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

Conclusion

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

1. 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
 TYPEPRED "max({k: posnat | divides(k, i!1) AND divides(k, j!1)})"
Premise 1.   (has proof of 1 step)

-1. max({k:posnat | divides(k, i!1) AND divides(k, j!1)}) > 0
-2. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), i!1)
-3. divides(max({k:posnat | divides(k, i!1) AND divides(k, j!1)}), j!1)
-4. FORALL x : (divides(x, i!1) AND divides(x, j!1)) IMPLIES (x < = max({k:posnat | divides(k, i!1) AND divides(k, j!1)}))
-5. (i!1 /= 0) OR (j!1 /= 0)

1. 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)
Premise 2.   (has proof of 6 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)
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)