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

Conclusion

-1. divides(nn!1, i!1)
-2. divides(nn!1, j!1)
-3. FORALL mm : (divides(mm, i!1) AND divides(mm, j!1)) IMPLIES (mm < = nn!1)
-4. (i!1 /= 0) OR (j!1 /= 0)

1. max({k:posnat | divides(k, i!1) AND divides(k, j!1)}) = nn!1

Tactic
 LEMMA "max_def"
Premise 1.   (has proof of 8 steps)

-1. FORALL S:{A:(nonempty?[posnat]) | EXISTS UB : FORALL y:(A) : y < = UB} , a:posnat : (max(S) = a) IFF maximum?(a, S)
-2. divides(nn!1, i!1)
-3. divides(nn!1, j!1)
-4. FORALL mm : (divides(mm, i!1) AND divides(mm, j!1)) IMPLIES (mm < = nn!1)
-5. (i!1 /= 0) OR (j!1 /= 0)

1. max({k:posnat | divides(k, i!1) AND divides(k, j!1)}) = nn!1