FDL > PVS > Number Theory > gcd > gcd TCC1 > pf:gcd_TCC1 : proof (4 nodes)

Conclusion

1. FORALL i:int, j:{jj:int | (i = 0) = > (jj /= 0)} : nonempty?[posnat]({k:posnat | divides(k, i) AND divides(k, j)}) AND (EXISTS UB : FORALL y:({k:posnat | divides(k, i) AND divides(k, j)}) : y < = UB)