FDL > PVS > Number Theory > gcd > gcd is max > pf:gcd is max > 1 > 1 > 2 (5 nodes)

Conclusion

-1. (i!1 /= 0) OR (j!1 /= 0)
-2. divides(kk!1, i!1)
-3. divides(kk!1, j!1)

1. nonempty?[posnat]({k:posnat | divides(k, i!1) AND divides(k, j!1)}) AND (EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB)
2. kk!1 < = max({k:posnat | divides(k, i!1) AND divides(k, j!1)})

Tactic
 REWRITE "gcd_noem"
Premise 1.   (has proof of 4 steps)

-1. (i!1 /= 0) OR (j!1 /= 0)
-2. divides(kk!1, i!1)
-3. divides(kk!1, j!1)

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