FDL > PVS > Number Theory > gcd > gcd def > pf:gcd_def : proof (20 nodes)

Conclusion

1. FORALL i:int, j:int, nn:posnat : ((i /= 0) OR (j /= 0)) IMPLIES ((gcd(i, j) = nn) IFF ((divides(nn, i) AND divides(nn, j)) AND (FORALL mm : (divides(mm, i) AND divides(mm, j)) IMPLIES (mm < = nn))))