Theorem prth ≪ | index | src | ≫ 

theorem prth (a b c d: nat): $ a, c = b, d <-> a = b /\ c = d $;
StepHypRefExpression
1 addcan1 
a + c = b + c <-> a = b
2 prlem2 
a, c <= b, d -> a + c <= b + d
3 eqle 
a, c = b, d -> a, c <= b, d
4 2, 3 syl 
a, c = b, d -> a + c <= b + d
5 prlem2 
b, d <= a, c -> b + d <= a + c
6 eqler 
a, c = b, d -> b, d <= a, c
7 5, 6 syl 
a, c = b, d -> b + d <= a + c
8 4, 7 leasymd 
a, c = b, d -> a + c = b + d
9 addcan2 
b + c = b + d <-> c = d
10 addcan2 
(b + d) * suc (b + d) // 2 + c = (b + d) * suc (b + d) // 2 + d <-> c = d
11 id 
a + c = b + d -> a + c = b + d
12 suceq 
a + c = b + d -> suc (a + c) = suc (b + d)
13 11, 12 muleqd 
a + c = b + d -> (a + c) * suc (a + c) = (b + d) * suc (b + d)
14 13 diveq1d 
a + c = b + d -> (a + c) * suc (a + c) // 2 = (b + d) * suc (b + d) // 2
15 14 addeq1d 
a + c = b + d -> (a + c) * suc (a + c) // 2 + c = (b + d) * suc (b + d) // 2 + c
16 15 eqeq1d 
a + c = b + d -> ((a + c) * suc (a + c) // 2 + c = (b + d) * suc (b + d) // 2 + d <-> (b + d) * suc (b + d) // 2 + c = (b + d) * suc (b + d) // 2 + d)
17 8, 16 rsyl 
a, c = b, d -> ((a + c) * suc (a + c) // 2 + c = (b + d) * suc (b + d) // 2 + d <-> (b + d) * suc (b + d) // 2 + c = (b + d) * suc (b + d) // 2 + d)
18 id 
a, c = b, d -> a, c = b, d
19 18 conv pr 
a, c = b, d -> (a + c) * suc (a + c) // 2 + c = (b + d) * suc (b + d) // 2 + d
20 17, 19 mpbid 
a, c = b, d -> (b + d) * suc (b + d) // 2 + c = (b + d) * suc (b + d) // 2 + d
21 10, 20 sylib 
a, c = b, d -> c = d
22 9, 21 sylibr 
a, c = b, d -> b + c = b + d
23 8, 22 eqtr4d 
a, c = b, d -> a + c = b + c
24 1, 23 sylib 
a, c = b, d -> a = b
25 24, 21 iand 
a, c = b, d -> a = b /\ c = d
26 anl 
a = b /\ c = d -> a = b
27 anr 
a = b /\ c = d -> c = d
28 26, 27 preqd 
a = b /\ c = d -> a, c = b, d
29 25, 28 ibii 
a, c = b, d <-> a = b /\ c = 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, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)