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

Conclusion

-1. (i!1 /= 0) OR (j!1 /= 0)

1. (gcd(i!1, j!1) = nn!1) IFF ((divides(nn!1, i!1) AND divides(nn!1, j!1)) AND (FORALL mm : (divides(mm, i!1) AND divides(mm, j!1)) IMPLIES (mm < = nn!1)))

Tactic
 SPLIT +
Premise 1.   (has proof of 7 steps)

-1. (i!1 /= 0) OR (j!1 /= 0)

1. (gcd(i!1, j!1) = nn!1) IMPLIES ((divides(nn!1, i!1) AND divides(nn!1, j!1)) AND (FORALL mm : (divides(mm, i!1) AND divides(mm, j!1)) IMPLIES (mm < = nn!1)))
Premise 2.   (has proof of 11 steps)

-1. (i!1 /= 0) OR (j!1 /= 0)

1. ((divides(nn!1, i!1) AND divides(nn!1, j!1)) AND (FORALL mm : (divides(mm, i!1) AND divides(mm, j!1)) IMPLIES (mm < = nn!1))) IMPLIES (gcd(i!1, j!1) = nn!1)