Theorem gcdcom ≪ | index | src | ≫ 

theorem gcdcom (a b: nat): $ gcd a b = gcd b a $;
StepHypRefExpression
1 id 
{d1 | A. x (x || d1 <-> x || a /\ x || b)} == {d2 | A. y (y || d2 <-> y || b /\ y || a)} ->
  {d1 | A. x (x || d1 <-> x || a /\ x || b)} == {d2 | A. y (y || d2 <-> y || b /\ y || a)}
2 1 theeqd 
{d1 | A. x (x || d1 <-> x || a /\ x || b)} == {d2 | A. y (y || d2 <-> y || b /\ y || a)} ->
  the {d1 | A. x (x || d1 <-> x || a /\ x || b)} = the {d2 | A. y (y || d2 <-> y || b /\ y || a)}
3 2 conv gcd 
{d1 | A. x (x || d1 <-> x || a /\ x || b)} == {d2 | A. y (y || d2 <-> y || b /\ y || a)} -> gcd a b = gcd b a
4 anr 
d1 = d2 /\ x = y -> x = y
5 anl 
d1 = d2 /\ x = y -> d1 = d2
6 4, 5 dvdeqd 
d1 = d2 /\ x = y -> (x || d1 <-> y || d2)
7 ancomb 
x || a /\ x || b <-> x || b /\ x || a
8 dvdeq1 
x = y -> (x || b <-> y || b)
9 dvdeq1 
x = y -> (x || a <-> y || a)
10 8, 9 aneqd 
x = y -> (x || b /\ x || a <-> y || b /\ y || a)
11 10 anwr 
d1 = d2 /\ x = y -> (x || b /\ x || a <-> y || b /\ y || a)
12 7, 11 syl5bb 
d1 = d2 /\ x = y -> (x || a /\ x || b <-> y || b /\ y || a)
13 6, 12 bieqd 
d1 = d2 /\ x = y -> (x || d1 <-> x || a /\ x || b <-> (y || d2 <-> y || b /\ y || a))
14 13 cbvald 
d1 = d2 -> (A. x (x || d1 <-> x || a /\ x || b) <-> A. y (y || d2 <-> y || b /\ y || a))
15 14 cbvab 
{d1 | A. x (x || d1 <-> x || a /\ x || b)} == {d2 | A. y (y || d2 <-> y || b /\ y || a)}
16 3, 15 ax_mp 
gcd a b = gcd b a

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