FDL > PVS > Number Theory > gcd > gcd def > pf:gcd def > 1 > 1 > 1 > 1 > 1 > 1 > 1 (2 nodes)

Conclusion

-1. FORALL kk:nzint : (((i!1 /= 0) OR (j!1 /= 0)) AND divides(kk, i!1) AND divides(kk, j!1)) IMPLIES (kk < = 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

Tactic
 INST "-1" "mm!1"
Premise 1.   (has proof of 1 step)

-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