Theorem eqgcd ≪ | index | src | ≫ 

theorem eqgcd (G: wff) (a b d: nat) {x: nat}:
  $ G -> (x || d <-> x || a /\ x || b) $ >
  $ G -> gcd a b = d $;
StepHypRefExpression
1 hyp h 
G -> (x || d <-> x || a /\ x || b)
2 1 iald 
G -> A. x (x || d <-> x || a /\ x || b)
3 2 anwl 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> A. x (x || d <-> x || a /\ x || b)
4 dvdeq1 
x = d2 -> (x || d <-> d2 || d)
5 dvdeq1 
x = d2 -> (x || a <-> d2 || a)
6 dvdeq1 
x = d2 -> (x || b <-> d2 || b)
7 5, 6 aneqd 
x = d2 -> (x || a /\ x || b <-> d2 || a /\ d2 || b)
8 4, 7 bieqd 
x = d2 -> (x || d <-> x || a /\ x || b <-> (d2 || d <-> d2 || a /\ d2 || b))
9 8 eale 
A. x (x || d <-> x || a /\ x || b) -> (d2 || d <-> d2 || a /\ d2 || b)
10 3, 9 rsyl 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> (d2 || d <-> d2 || a /\ d2 || b)
11 dvdid 
d2 || d2
12 dvdeq1 
y = d2 -> (y || d2 <-> d2 || d2)
13 dvdeq1 
y = d2 -> (y || a <-> d2 || a)
14 dvdeq1 
y = d2 -> (y || b <-> d2 || b)
15 13, 14 aneqd 
y = d2 -> (y || a /\ y || b <-> d2 || a /\ d2 || b)
16 12, 15 bieqd 
y = d2 -> (y || d2 <-> y || a /\ y || b <-> (d2 || d2 <-> d2 || a /\ d2 || b))
17 16 eale 
A. y (y || d2 <-> y || a /\ y || b) -> (d2 || d2 <-> d2 || a /\ d2 || b)
18 17 anwr 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> (d2 || d2 <-> d2 || a /\ d2 || b)
19 11, 18 mpbii 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> d2 || a /\ d2 || b
20 10, 19 mpbird 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> d2 || d
21 dvdeq1 
y = d -> (y || d2 <-> d || d2)
22 dvdeq1 
y = d -> (y || a <-> d || a)
23 dvdeq1 
y = d -> (y || b <-> d || b)
24 22, 23 aneqd 
y = d -> (y || a /\ y || b <-> d || a /\ d || b)
25 21, 24 bieqd 
y = d -> (y || d2 <-> y || a /\ y || b <-> (d || d2 <-> d || a /\ d || b))
26 25 eale 
A. y (y || d2 <-> y || a /\ y || b) -> (d || d2 <-> d || a /\ d || b)
27 26 anwr 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> (d || d2 <-> d || a /\ d || b)
28 dvdid 
d || d
29 dvdeq1 
x = d -> (x || d <-> d || d)
30 dvdeq1 
x = d -> (x || a <-> d || a)
31 dvdeq1 
x = d -> (x || b <-> d || b)
32 30, 31 aneqd 
x = d -> (x || a /\ x || b <-> d || a /\ d || b)
33 29, 32 bieqd 
x = d -> (x || d <-> x || a /\ x || b <-> (d || d <-> d || a /\ d || b))
34 33 eale 
A. x (x || d <-> x || a /\ x || b) -> (d || d <-> d || a /\ d || b)
35 3, 34 rsyl 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> (d || d <-> d || a /\ d || b)
36 28, 35 mpbii 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> d || a /\ d || b
37 27, 36 mpbird 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> d || d2
38 20, 37 dvdasymd 
G /\ A. y (y || d2 <-> y || a /\ y || b) -> d2 = d
39 anr 
G /\ d2 = d /\ y = x -> y = x
40 anlr 
G /\ d2 = d /\ y = x -> d2 = d
41 39, 40 dvdeqd 
G /\ d2 = d /\ y = x -> (y || d2 <-> x || d)
42 dvdeq1 
y = x -> (y || a <-> x || a)
43 dvdeq1 
y = x -> (y || b <-> x || b)
44 42, 43 aneqd 
y = x -> (y || a /\ y || b <-> x || a /\ x || b)
45 44 anwr 
G /\ d2 = d /\ y = x -> (y || a /\ y || b <-> x || a /\ x || b)
46 41, 45 bieqd 
G /\ d2 = d /\ y = x -> (y || d2 <-> y || a /\ y || b <-> (x || d <-> x || a /\ x || b))
47 46 cbvald 
G /\ d2 = d -> (A. y (y || d2 <-> y || a /\ y || b) <-> A. x (x || d <-> x || a /\ x || b))
48 2 anwl 
G /\ d2 = d -> A. x (x || d <-> x || a /\ x || b)
49 47, 48 mpbird 
G /\ d2 = d -> A. y (y || d2 <-> y || a /\ y || b)
50 38, 49 ibida 
G -> (A. y (y || d2 <-> y || a /\ y || b) <-> d2 = d)
51 50 eqtheabd 
G -> the {d2 | A. y (y || d2 <-> y || a /\ y || b)} = d
52 51 conv gcd 
G -> gcd a b = d

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), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)