Theorem addcan1 ≪ | index | src | ≫ 

theorem addcan1 (a b c: nat): $ a + c = b + c <-> a = b $;
StepHypRefExpression
1 addeq2 
x = c -> a + x = a + c
2 addeq2 
x = c -> b + x = b + c
3 1, 2 eqeqd 
x = c -> (a + x = b + x <-> a + c = b + c)
4 3 bieq1d 
x = c -> (a + x = b + x <-> a = b <-> (a + c = b + c <-> a = b))
5 addeq2 
x = 0 -> a + x = a + 0
6 addeq2 
x = 0 -> b + x = b + 0
7 5, 6 eqeqd 
x = 0 -> (a + x = b + x <-> a + 0 = b + 0)
8 7 bieq1d 
x = 0 -> (a + x = b + x <-> a = b <-> (a + 0 = b + 0 <-> a = b))
9 addeq2 
x = y -> a + x = a + y
10 addeq2 
x = y -> b + x = b + y
11 9, 10 eqeqd 
x = y -> (a + x = b + x <-> a + y = b + y)
12 11 bieq1d 
x = y -> (a + x = b + x <-> a = b <-> (a + y = b + y <-> a = b))
13 addeq2 
x = suc y -> a + x = a + suc y
14 addeq2 
x = suc y -> b + x = b + suc y
15 13, 14 eqeqd 
x = suc y -> (a + x = b + x <-> a + suc y = b + suc y)
16 15 bieq1d 
x = suc y -> (a + x = b + x <-> a = b <-> (a + suc y = b + suc y <-> a = b))
17 eqeq 
a + 0 = a -> b + 0 = b -> (a + 0 = b + 0 <-> a = b)
18 add0 
a + 0 = a
19 17, 18 ax_mp 
b + 0 = b -> (a + 0 = b + 0 <-> a = b)
20 add0 
b + 0 = b
21 19, 20 ax_mp 
a + 0 = b + 0 <-> a = b
22 bitr 
(a + suc y = b + suc y <-> suc (a + y) = suc (b + y)) -> (suc (a + y) = suc (b + y) <-> a + y = b + y) -> (a + suc y = b + suc y <-> a + y = b + y)
23 eqeq 
a + suc y = suc (a + y) -> b + suc y = suc (b + y) -> (a + suc y = b + suc y <-> suc (a + y) = suc (b + y))
24 addS 
a + suc y = suc (a + y)
25 23, 24 ax_mp 
b + suc y = suc (b + y) -> (a + suc y = b + suc y <-> suc (a + y) = suc (b + y))
26 addS 
b + suc y = suc (b + y)
27 25, 26 ax_mp 
a + suc y = b + suc y <-> suc (a + y) = suc (b + y)
28 22, 27 ax_mp 
(suc (a + y) = suc (b + y) <-> a + y = b + y) -> (a + suc y = b + suc y <-> a + y = b + y)
29 peano2 
suc (a + y) = suc (b + y) <-> a + y = b + y
30 28, 29 ax_mp 
a + suc y = b + suc y <-> a + y = b + y
31 id 
(a + y = b + y <-> a = b) -> (a + y = b + y <-> a = b)
32 30, 31 syl5bb 
(a + y = b + y <-> a = b) -> (a + suc y = b + suc y <-> a = b)
33 4, 8, 12, 16, 21, 32 ind 
a + c = b + c <-> 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 (peano2, peano5, addeq, add0, addS)