FDL > PVS > Number Theory > gcd > gcd is max > pf:gcd is max > 1 > 1 > 1 > 2

Conclusion

-1. max({k:posnat | divides(k, i!1) AND divides(k, j!1)}) > 0
-2. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), i!1)
-3. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), j!1)
-4. (i!1 /= 0) OR (j!1 /= 0)
-5. divides(kk!1, i!1)
-6. divides(kk!1, j!1)

1. (kk!1 > = 0) AND (kk!1 > 0)
2. kk!1 < = max({k:posnat | divides(k, i!1) AND divides(k, j!1)})