FDL > PVS > Number Theory > gcd > gcd divides > pf:gcd divides > 1 > 1 > 2 (6 nodes)

Conclusion

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

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)
2. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), i!1) AND divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), j!1)

Tactic
 HIDE 2
Premise 1.   (has proof of 5 steps)

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

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)