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