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

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. FORALL x : (divides(x, i!1) AND divides(x, j!1)) IMPLIES (x < = max({k:posnat | divides(k, i!1) AND divides(k, j!1)}))
-5. (i!1 /= 0) OR (j!1 /= 0)

1. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), i!1) AND divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), j!1)