Theorem expr ≪ | index | src | ≫ 

theorem expr (a: nat) {x y: nat}: $ E. x E. y a = x, y $;
StepHypRefExpression
1 id 
_1 = a -> _1 = a
2 1 eqeq1d 
_1 = a -> (_1 = x, y <-> a = x, y)
3 2 exeqd 
_1 = a -> (E. y _1 = x, y <-> E. y a = x, y)
4 3 exeqd 
_1 = a -> (E. x E. y _1 = x, y <-> E. x E. y a = x, y)
5 id 
_1 = 0 -> _1 = 0
6 5 eqeq1d 
_1 = 0 -> (_1 = x, y <-> 0 = x, y)
7 6 exeqd 
_1 = 0 -> (E. y _1 = x, y <-> E. y 0 = x, y)
8 7 exeqd 
_1 = 0 -> (E. x E. y _1 = x, y <-> E. x E. y 0 = x, y)
9 id 
_1 = a1 -> _1 = a1
10 9 eqeq1d 
_1 = a1 -> (_1 = x, y <-> a1 = x, y)
11 10 exeqd 
_1 = a1 -> (E. y _1 = x, y <-> E. y a1 = x, y)
12 11 exeqd 
_1 = a1 -> (E. x E. y _1 = x, y <-> E. x E. y a1 = x, y)
13 id 
_1 = suc a1 -> _1 = suc a1
14 13 eqeq1d 
_1 = suc a1 -> (_1 = x, y <-> suc a1 = x, y)
15 14 exeqd 
_1 = suc a1 -> (E. y _1 = x, y <-> E. y suc a1 = x, y)
16 15 exeqd 
_1 = suc a1 -> (E. x E. y _1 = x, y <-> E. x E. y suc a1 = x, y)
17 pr0 
0, 0 = 0
18 preq 
x = 0 -> y = 0 -> x, y = 0, 0
19 18 imp 
x = 0 /\ y = 0 -> x, y = 0, 0
20 19 eqcomd 
x = 0 /\ y = 0 -> 0, 0 = x, y
21 17, 20 syl5eqr 
x = 0 /\ y = 0 -> 0 = x, y
22 21 iexde 
x = 0 -> E. y 0 = x, y
23 22 iexie 
E. x E. y 0 = x, y
24 anl 
m = x /\ n = y -> m = x
25 anr 
m = x /\ n = y -> n = y
26 24, 25 preqd 
m = x /\ n = y -> m, n = x, y
27 26 eqeq2d 
m = x /\ n = y -> (suc a1 = m, n <-> suc a1 = x, y)
28 27 cbvexd 
m = x -> (E. n suc a1 = m, n <-> E. y suc a1 = x, y)
29 28 cbvex 
E. m E. n suc a1 = m, n <-> E. x E. y suc a1 = x, y
30 an3l 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> a1 = x, y
31 30 suceqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc a1 = suc (x, y)
32 addS 
(x + y) * suc (x + y) // 2 + suc y = suc ((x + y) * suc (x + y) // 2 + y)
33 32 conv pr 
(x + y) * suc (x + y) // 2 + suc y = suc (x, y)
34 mulcan2 
2 != 0 -> (2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * (suc y * suc (suc y) // 2) <-> (x + y) * suc (x + y) // 2 + suc y = suc y * suc (suc y) // 2)
35 d2ne0 
2 != 0
36 34, 35 ax_mp 
2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * (suc y * suc (suc y) // 2) <-> (x + y) * suc (x + y) // 2 + suc y = suc y * suc (suc y) // 2
37 muladd 
2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y
38 eqtr 
2 * (suc y * suc (suc y) // 2) = suc y * suc (suc y) -> suc y * suc (suc y) = suc (suc y) * suc y -> 2 * (suc y * suc (suc y) // 2) = suc (suc y) * suc y
39 muldiv3 
2 || suc y * suc (suc y) -> 2 * (suc y * suc (suc y) // 2) = suc y * suc (suc y)
40 prlem1 
2 || suc y * suc (suc y)
41 39, 40 ax_mp 
2 * (suc y * suc (suc y) // 2) = suc y * suc (suc y)
42 38, 41 ax_mp 
suc y * suc (suc y) = suc (suc y) * suc y -> 2 * (suc y * suc (suc y) // 2) = suc (suc y) * suc y
43 mulcom 
suc y * suc (suc y) = suc (suc y) * suc y
44 42, 43 ax_mp 
2 * (suc y * suc (suc y) // 2) = suc (suc y) * suc y
45 muldiv3 
2 || (x + y) * suc (x + y) -> 2 * ((x + y) * suc (x + y) // 2) = (x + y) * suc (x + y)
46 prlem1 
2 || (x + y) * suc (x + y)
47 45, 46 ax_mp 
2 * ((x + y) * suc (x + y) // 2) = (x + y) * suc (x + y)
48 add01 
0 + y = y
49 anr 
a1 = x, y /\ x = 0 -> x = 0
50 49 anwll 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x = 0
51 50 addeq1d 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x + y = 0 + y
52 48, 51 syl6eq 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> x + y = y
53 52 suceqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (x + y) = suc y
54 52, 53 muleqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) = y * suc y
55 47, 54 syl5eq 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) = y * suc y
56 55 addeq1d 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = y * suc y + 2 * suc y
57 addmul 
(y + 2) * suc y = y * suc y + 2 * suc y
58 muleq1 
y + 2 = suc (suc y) -> (y + 2) * suc y = suc (suc y) * suc y
59 eqtr 
y + 2 = suc (y + 1) -> suc (y + 1) = suc (suc y) -> y + 2 = suc (suc y)
60 addS 
y + suc 1 = suc (y + 1)
61 60 conv d2 
y + 2 = suc (y + 1)
62 59, 61 ax_mp 
suc (y + 1) = suc (suc y) -> y + 2 = suc (suc y)
63 suceq 
y + 1 = suc y -> suc (y + 1) = suc (suc y)
64 add12 
y + 1 = suc y
65 63, 64 ax_mp 
suc (y + 1) = suc (suc y)
66 62, 65 ax_mp 
y + 2 = suc (suc y)
67 58, 66 ax_mp 
(y + 2) * suc y = suc (suc y) * suc y
68 67 a1i 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (y + 2) * suc y = suc (suc y) * suc y
69 57, 68 syl5eqr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> y * suc y + 2 * suc y = suc (suc y) * suc y
70 56, 69 eqtrd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = suc (suc y) * suc y
71 44, 70 syl6eqr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2) + 2 * suc y = 2 * (suc y * suc (suc y) // 2)
72 37, 71 syl5eq 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> 2 * ((x + y) * suc (x + y) // 2 + suc y) = 2 * (suc y * suc (suc y) // 2)
73 36, 72 sylib 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) // 2 + suc y = suc y * suc (suc y) // 2
74 add0 
suc y * suc (suc y) // 2 + 0 = suc y * suc (suc y) // 2
75 add0 
suc y + 0 = suc y
76 anlr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m = suc y
77 anr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> n = 0
78 76, 77 addeqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m + n = suc y + 0
79 75, 78 syl6eq 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m + n = suc y
80 79 suceqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (m + n) = suc (suc y)
81 79, 80 muleqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) = suc y * suc (suc y)
82 81 diveq1d 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) // 2 = suc y * suc (suc y) // 2
83 82, 77 addeqd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (m + n) * suc (m + n) // 2 + n = suc y * suc (suc y) // 2 + 0
84 83 conv pr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m, n = suc y * suc (suc y) // 2 + 0
85 74, 84 syl6eq 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> m, n = suc y * suc (suc y) // 2
86 73, 85 eqtr4d 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> (x + y) * suc (x + y) // 2 + suc y = m, n
87 33, 86 syl5eqr 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc (x, y) = m, n
88 31, 87 eqtrd 
a1 = x, y /\ x = 0 /\ m = suc y /\ n = 0 -> suc a1 = m, n
89 88 iexde 
a1 = x, y /\ x = 0 /\ m = suc y -> E. n suc a1 = m, n
90 89 iexde 
a1 = x, y /\ x = 0 -> E. m E. n suc a1 = m, n
91 90 exp 
a1 = x, y -> x = 0 -> E. m E. n suc a1 = m, n
92 exsuc 
x != 0 <-> E. z x = suc z
93 92 conv ne 
~x = 0 <-> E. z x = suc z
94 suceq 
a1 = x, y -> suc a1 = suc (x, y)
95 94 anw3l 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc a1 = suc (x, y)
96 addSass 
suc z + y = z + suc y
97 addeq1 
x = suc z -> x + y = suc z + y
98 97 anwr 
a1 = x, y /\ x = suc z -> x + y = suc z + y
99 98 anwll 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = suc z + y
100 96, 99 syl6eq 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = z + suc y
101 anlr 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> m = z
102 anr 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> n = suc y
103 101, 102 addeqd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> m + n = z + suc y
104 100, 103 eqtr4d 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> x + y = m + n
105 104 suceqd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc (x + y) = suc (m + n)
106 104, 105 muleqd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) = (m + n) * suc (m + n)
107 106 diveq1d 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 = (m + n) * suc (m + n) // 2
108 102 eqcomd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc y = n
109 107, 108 addeqd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 + suc y = (m + n) * suc (m + n) // 2 + n
110 109 conv pr 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> (x + y) * suc (x + y) // 2 + suc y = m, n
111 33, 110 syl5eqr 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc (x, y) = m, n
112 95, 111 eqtrd 
a1 = x, y /\ x = suc z /\ m = z /\ n = suc y -> suc a1 = m, n
113 112 iexde 
a1 = x, y /\ x = suc z /\ m = z -> E. n suc a1 = m, n
114 113 iexde 
a1 = x, y /\ x = suc z -> E. m E. n suc a1 = m, n
115 114 eexda 
a1 = x, y -> E. z x = suc z -> E. m E. n suc a1 = m, n
116 93, 115 syl5bi 
a1 = x, y -> ~x = 0 -> E. m E. n suc a1 = m, n
117 91, 116 casesd 
a1 = x, y -> E. m E. n suc a1 = m, n
118 117 eex 
E. y a1 = x, y -> E. m E. n suc a1 = m, n
119 118 eex 
E. x E. y a1 = x, y -> E. m E. n suc a1 = m, n
120 29, 119 sylib 
E. x E. y a1 = x, y -> E. x E. y suc a1 = x, y
121 4, 8, 12, 16, 23, 120 ind 
E. x E. y a = x, y

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)