FDL > PVS > Number Theory > gcd > gcd divides > pf:gcd divides > 1 > 1 > 2 > 1 (5 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)

Tactic
 PROP
Premise 1.   (has proof of 1 step)

1. i!1 = 0
2. nonempty?[posnat]({k:posnat | divides(k, i!1) AND divides(k, j!1)})
Premise 2.   (has proof of 1 step)

1. j!1 = 0
2. nonempty?[posnat]({k:posnat | divides(k, i!1) AND divides(k, j!1)})
Premise 3.   (has proof of 1 step)

1. i!1 = 0
2. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB
Premise 4.   (has proof of 1 step)

1. j!1 = 0
2. EXISTS UB : FORALL y:({k:posnat | divides(k, i!1) AND divides(k, j!1)}) : y < = UB