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

Conclusion

-1. (((i!1 /= 0) OR (j!1 /= 0)) AND divides(mm!1, i!1) AND divides(mm!1, j!1)) IMPLIES (mm!1 < = gcd(i!1, j!1))
-2. gcd(i!1, j!1) = nn!1
-3. divides(mm!1, i!1)
-4. divides(mm!1, j!1)
-5. (i!1 /= 0) OR (j!1 /= 0)

1. mm!1 < = nn!1