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

Conclusion

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

1. divides(gcd(i!1, j!1), i!1) AND divides(gcd(i!1, j!1), j!1)

Tactic
 EXPAND "gcd"
Premise 1.   (has proof of 8 steps)

-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)