Theorem dvdcop | index | src |

theorem dvdcop (G: wff) (a b d: nat):
  $ G -> coprime a b $ >
  $ G -> d || a $ >
  $ G -> d || b $ >
  $ G -> d = 1 $;
StepHypRefExpression
1 dvd12
d || 1 <-> d = 1
2 hyp h1
G -> coprime a b
3 2 conv coprime
G -> gcd a b = 1
4 3 dvdeq2d
G -> (d || gcd a b <-> d || 1)
5 dvdgcd
d || gcd a b <-> d || a /\ d || b
6 hyp h2
G -> d || a
7 hyp h3
G -> d || b
8 6, 7 iand
G -> d || a /\ d || b
9 5, 8 sylibr
G -> d || gcd a b
10 4, 9 mpbid
G -> d || 1
11 1, 10 sylib
G -> d = 1

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)