FDL > PVS > Number Theory > gcd > gcd divides > pf:gcd divides > 1 > 1 > 2 > 1 > 4

Conclusion

1. j!1 = 0
2. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB