Theorem leasymd ≪ | index | src | ≫ 

theorem leasymd (G: wff) (a b: nat):
  $ G -> a <= b $ >
  $ G -> b <= a $ >
  $ G -> a = b $;
StepHypRefExpression
1 hyp h1 
G -> a <= b
2 add0 
a + 0 = a
3 addeq2 
x = 0 -> a + x = a + 0
4 3 anwr 
G /\ a + x = b /\ x = 0 -> a + x = a + 0
5 anlr 
G /\ a + x = b /\ x = 0 -> a + x = b
6 4, 5 eqtr3d 
G /\ a + x = b /\ x = 0 -> a + 0 = b
7 2, 6 syl5eqr 
G /\ a + x = b /\ x = 0 -> a = b
8 exsuc 
x != 0 <-> E. y x = suc y
9 8 conv ne 
~x = 0 <-> E. y x = suc y
10 hyp h2 
G -> b <= a
11 10 anwl 
G /\ a + x = b -> b <= a
12 11 anwl 
G /\ a + x = b /\ x = suc y -> b <= a
13 absurd 
~suc (y + z) = 0 -> suc (y + z) = 0 -> a = b
14 peano1 
suc (y + z) != 0
15 14 conv ne 
~suc (y + z) = 0
16 15 a1i 
G /\ a + x = b /\ x = suc y /\ b + z = a -> ~suc (y + z) = 0
17 addS1 
suc y + z = suc (y + z)
18 anlr 
G /\ a + x = b /\ x = suc y /\ b + z = a -> x = suc y
19 18 addeq1d 
G /\ a + x = b /\ x = suc y /\ b + z = a -> x + z = suc y + z
20 addcan2 
a + (x + z) = a + 0 <-> x + z = 0
21 eqcom 
a + x + z = a + (x + z) -> a + (x + z) = a + x + z
22 addass 
a + x + z = a + (x + z)
23 21, 22 ax_mp 
a + (x + z) = a + x + z
24 anlr 
G /\ a + x = b /\ x = suc y -> a + x = b
25 24 anwl 
G /\ a + x = b /\ x = suc y /\ b + z = a -> a + x = b
26 25 addeq1d 
G /\ a + x = b /\ x = suc y /\ b + z = a -> a + x + z = b + z
27 anr 
G /\ a + x = b /\ x = suc y /\ b + z = a -> b + z = a
28 26, 27 eqtrd 
G /\ a + x = b /\ x = suc y /\ b + z = a -> a + x + z = a
29 23, 2, 28 eqtr4g 
G /\ a + x = b /\ x = suc y /\ b + z = a -> a + (x + z) = a + 0
30 20, 29 sylib 
G /\ a + x = b /\ x = suc y /\ b + z = a -> x + z = 0
31 19, 30 eqtr3d 
G /\ a + x = b /\ x = suc y /\ b + z = a -> suc y + z = 0
32 17, 31 syl5eqr 
G /\ a + x = b /\ x = suc y /\ b + z = a -> suc (y + z) = 0
33 13, 16, 32 sylc 
G /\ a + x = b /\ x = suc y /\ b + z = a -> a = b
34 33 eexda 
G /\ a + x = b /\ x = suc y -> E. z b + z = a -> a = b
35 34 conv le 
G /\ a + x = b /\ x = suc y -> b <= a -> a = b
36 12, 35 mpd 
G /\ a + x = b /\ x = suc y -> a = b
37 36 eexda 
G /\ a + x = b -> E. y x = suc y -> a = b
38 9, 37 syl5bi 
G /\ a + x = b -> ~x = 0 -> a = b
39 38 imp 
G /\ a + x = b /\ ~x = 0 -> a = b
40 7, 39 casesda 
G /\ a + x = b -> a = b
41 40 eexda 
G -> E. x a + x = b -> a = b
42 41 conv le 
G -> a <= b -> a = b
43 1, 42 mpd 
G -> a = b

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_peano (peano1, peano2, peano5, addeq, add0, addS)