FDL > PVS > Number Theory > gcd > gcd TCC1 > pf:gcd TCC1 > 1 (3 nodes)

Conclusion

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)

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

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