MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2503lem2 Structured version   Visualization version   GIF version

Theorem 2503lem2 17133
Description: Lemma for 2503prm 17135. Calculate a power mod. We calculate 2↑19 = 2↑18 · 2≡1832 · 2 = 𝑁 + 1161, 2↑38 = (2↑19)↑2≡1161↑2 = 538𝑁 + 1307, 2↑39 = 2↑38 · 2≡1307 · 2 = 𝑁 + 111, 2↑78 = (2↑39)↑2≡111↑2 = 5𝑁 − 194, 2↑156 = (2↑78)↑2≡194↑2 = 15𝑁 + 91, 2↑312 = (2↑156)↑2≡91↑2 = 3𝑁 + 772, 2↑624 = (2↑312)↑2≡772↑2 = 238𝑁 + 270, 2↑1248 = (2↑624)↑2≡270↑2 = 29𝑁 + 313, 2↑1251 = 2↑1248 · 8≡313 · 8 = 𝑁 + 1 and finally 2↑(𝑁 − 1) = (2↑1251)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
2503prm.1 𝑁 = 2503
Assertion
Ref Expression
2503lem2 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)

Proof of Theorem 2503lem2
StepHypRef Expression
1 2503prm.1 . . 3 𝑁 = 2503
2 2nn0 12533 . . . . . 6 2 ∈ ℕ0
3 5nn0 12536 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12736 . . . . 5 25 ∈ ℕ0
5 0nn0 12531 . . . . 5 0 ∈ ℕ0
64, 5deccl 12736 . . . 4 250 ∈ ℕ0
7 3nn 12335 . . . 4 3 ∈ ℕ
86, 7decnncl 12741 . . 3 2503 ∈ ℕ
91, 8eqeltri 2822 . 2 𝑁 ∈ ℕ
10 2nn 12329 . 2 2 ∈ ℕ
11 1nn0 12532 . . . . 5 1 ∈ ℕ0
1211, 2deccl 12736 . . . 4 12 ∈ ℕ0
1312, 3deccl 12736 . . 3 125 ∈ ℕ0
1413, 11deccl 12736 . 2 1251 ∈ ℕ0
15 0z 12613 . 2 0 ∈ ℤ
16 4nn0 12535 . . . . 5 4 ∈ ℕ0
1712, 16deccl 12736 . . . 4 124 ∈ ℕ0
18 8nn0 12539 . . . 4 8 ∈ ℕ0
1917, 18deccl 12736 . . 3 1248 ∈ ℕ0
20 1z 12636 . . 3 1 ∈ ℤ
21 3nn0 12534 . . . . 5 3 ∈ ℕ0
2221, 11deccl 12736 . . . 4 31 ∈ ℕ0
2322, 21deccl 12736 . . 3 313 ∈ ℕ0
24 6nn0 12537 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 12736 . . . . 5 62 ∈ ℕ0
2625, 16deccl 12736 . . . 4 624 ∈ ℕ0
27 9nn0 12540 . . . . . 6 9 ∈ ℕ0
282, 27deccl 12736 . . . . 5 29 ∈ ℕ0
2928nn0zi 12631 . . . 4 29 ∈ ℤ
30 7nn0 12538 . . . . . 6 7 ∈ ℕ0
312, 30deccl 12736 . . . . 5 27 ∈ ℕ0
3231, 5deccl 12736 . . . 4 270 ∈ ℕ0
3322, 2deccl 12736 . . . . 5 312 ∈ ℕ0
342, 21deccl 12736 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 12736 . . . . . 6 238 ∈ ℕ0
3635nn0zi 12631 . . . . 5 238 ∈ ℤ
3730, 30deccl 12736 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 12736 . . . . 5 772 ∈ ℕ0
3911, 3deccl 12736 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 12736 . . . . . 6 156 ∈ ℕ0
4121nn0zi 12631 . . . . . 6 3 ∈ ℤ
4227, 11deccl 12736 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 12736 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 12631 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 12736 . . . . . . . 8 19 ∈ ℕ0
46 4nn 12339 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 12741 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 12736 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 12736 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 12736 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 12631 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 12736 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 12736 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 12736 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 12736 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 12736 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 12736 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 12736 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 12736 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 12631 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 12736 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 12736 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 12736 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 12736 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 12736 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 17132 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 12406 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2726 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 12752 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2726 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2726 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 12528 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addridi 11440 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2726 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 12528 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addridi 11440 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 12331 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mullidi 11258 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 12380 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 7426 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 12398 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2754 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 12344 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mullidi 11258 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 7424 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 12403 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 12743 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 12774 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 11205 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 11443 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 7424 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 12347 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addlidi 11441 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2758 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 12774 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 12337 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mullidi 11258 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 7424 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 12401 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 12743 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2758 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 12774 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2726 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2726 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 7424 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2754 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 12836 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 12786 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 12422 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 12785 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 12420 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 12785 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2757 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 17065 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2726 . . . . . . . . . . 11 19 = 19
117 2t1e2 12419 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 7424 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2754 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 12356 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 12843 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 11262 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 12787 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2726 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 12736 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 12736 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2726 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2726 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2726 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2726 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 12381 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 12416 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 11445 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 12775 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addlidi 11441 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 12775 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 12528 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addridi 11440 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 12736 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 12736 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2726 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 12743 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2726 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 12404 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 12528 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addlidi 11441 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 12752 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 12808 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 11445 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 12776 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2726 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 12405 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2726 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 12752 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 7425 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 12821 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addlidi 11441 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 12781 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2754 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 7424 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 12353 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 12805 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 11445 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2754 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 12773 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 12752 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 12773 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 12743 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 12341 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addlidi 11441 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2754 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 12378 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 7425 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 12824 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 12752 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2754 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 12822 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 11262 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 12414 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 12781 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 12773 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 12839 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addlidi 11441 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 12781 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 12773 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 12774 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 12528 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 11443 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 7424 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2758 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 12774 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 12743 . . . . . . . . . . . . 13 7 = 07
19321dec0h 12743 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2754 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 7425 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 12752 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2754 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 12423 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 7424 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 12809 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2754 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 12773 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 12837 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 12350 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 12797 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 11445 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 12782 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 12773 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 12774 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2726 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 12736 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 12736 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 12736 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2726 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2726 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 12743 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2726 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 7424 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2754 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 12723 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 11445 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 12777 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 11445 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 12775 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2726 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 12775 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 12775 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 12528 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addridi 11440 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2754 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 12418 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 11428 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 7426 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2754 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 7424 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 12399 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2758 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 12773 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulridi 11257 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 7424 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2754 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 12773 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 7424 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 11445 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 12773 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 12743 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 12743 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2754 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 7424 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2754 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 12772 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 7424 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addridi 11440 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2758 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 12773 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 7424 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 11445 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 12773 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 12774 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2754 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mullidi 11258 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 7426 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2754 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 7424 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2758 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 12773 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 12829 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 12752 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 12773 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 7424 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 12795 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2754 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 12773 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 12774 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 12528 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulridi 11257 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 12787 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2757 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 17064 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2726 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 12752 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2726 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2754 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 7426 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addridi 11440 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2754 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 12774 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 7424 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2758 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 12774 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 12774 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 7424 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2758 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 12773 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 11442 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 7424 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2758 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 12773 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 12830 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 12786 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2757 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 17065 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2726 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 11262 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 7424 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2754 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 12787 . . . . . . . 8 (2 · 39) = 78
310 eqid 2726 . . . . . . . . . 10 2309 = 2309
311 eqid 2726 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 12781 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 12528 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addridi 11440 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 12424 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 12391 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 7426 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 12803 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2754 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 12823 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 11262 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 12781 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 12774 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 11443 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 7424 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2758 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 12774 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 12819 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 12782 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 12774 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 12775 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 7424 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2758 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 12773 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 12773 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 12773 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 12774 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 12528 . . . . . . . . . . 11 111 ∈ ℂ
339338mulridi 11257 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 12787 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2757 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 17064 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2726 . . . . . . . 8 78 = 78
344 4p1e5 12402 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 11262 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 12752 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 11262 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 12787 . . . . . . 7 (2 · 78) = 156
349 eqid 2726 . . . . . . . . 9 194 = 194
3502, 16deccl 12736 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2726 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 12752 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2726 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 12752 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 12775 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 12762 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 12810 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 12776 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2757 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2726 . . . . . . . . 9 91 = 91
361 eqid 2726 . . . . . . . . . . . 12 15 = 15
362204addlidi 11441 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2754 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 7426 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2754 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 12781 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 12773 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 7426 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 12412 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2754 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 12773 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 12774 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 12528 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 11443 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 7424 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2758 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 12774 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 7426 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2754 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 12773 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 12774 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 12736 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2726 . . . . . . . . . 10 77 = 77
38411, 30deccl 12736 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 12736 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2726 . . . . . . . . . . . 12 175 = 175
387384nn0cni 12528 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addlidi 11441 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 12752 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 12798 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 12776 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 7426 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2754 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulridi 11257 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 7424 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 12814 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2754 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 12773 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulridi 11257 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 7424 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 12409 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2758 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 12773 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mullidi 11258 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addlidi 11441 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 7426 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2754 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 12850 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 11445 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 12781 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 12773 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 12845 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 11262 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 12799 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 11445 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 12782 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 12773 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 12774 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mullidi 11258 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 7426 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 12410 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2754 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 12752 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 12773 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 12820 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 12786 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 12787 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2757 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 17066 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2726 . . . . . . 7 156 = 156
431117, 172oveq12i 7426 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2754 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 11262 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 12752 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 12774 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 12825 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 11262 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 12787 . . . . . 6 (2 · 156) = 312
439 eqid 2726 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 12752 . . . . . . . . 9 (77 + 1) = 78
441204addridi 11440 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2754 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 7426 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 12415 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2754 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 11445 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 12782 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 12774 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 11443 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 7424 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2758 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 12774 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 7424 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2754 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 12774 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 12752 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 7424 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 12815 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2754 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 12779 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 12528 . . . . . . . . 9 91 ∈ ℂ
462461mulridi 11257 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 12787 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2757 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 17064 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2726 . . . . . 6 312 = 312
467 eqid 2726 . . . . . . . . 9 31 = 31
468306oveq1i 7424 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2754 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2754 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 12787 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 7424 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 12528 . . . . . . . 8 62 ∈ ℂ
474473addridi 11440 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2754 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2754 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 12787 . . . . 5 (2 · 312) = 624
478 eqid 2726 . . . . . . 7 270 = 270
47930, 11deccl 12736 . . . . . . 7 71 ∈ ℕ0
480 eqid 2726 . . . . . . . . 9 71 = 71
481 7p2e9 12417 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 11445 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 12775 . . . . . . . 8 (27 + 71) = 98
484120addridi 11440 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2754 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 12736 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2726 . . . . . . . . . 10 238 = 238
488486nn0cni 12528 . . . . . . . . . . 11 119 ∈ ℂ
489488addlidi 11441 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 12781 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 7426 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2754 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 7424 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2758 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 12773 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 12812 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 11445 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 12782 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 12773 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 7425 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2754 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 12773 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 12773 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 12774 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 12528 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 11443 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 7424 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2758 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 12774 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 7426 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2754 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 12773 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 12786 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 7424 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 12736 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 12528 . . . . . . . . 9 714 ∈ ℂ
517516addridi 11440 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2754 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 12774 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 12736 . . . . . . 7 154 ∈ ℕ0
521 eqid 2726 . . . . . . . 8 154 = 154
5223, 16deccl 12736 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 12736 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 12736 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2726 . . . . . . . . . 10 540 = 540
526 eqid 2726 . . . . . . . . . . 11 54 = 54
52783addlidi 11441 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 12775 . . . . . . . . . 10 (1 + 54) = 55
52983addridi 11440 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 12775 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2726 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 12752 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 12835 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 12792 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 12775 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 12782 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 12773 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 11445 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 12781 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 12773 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 7425 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 12811 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 12782 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2754 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 12762 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 12773 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 12411 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 12781 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 12773 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 12774 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 12752 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 12786 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 12785 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 12787 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2757 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 17064 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2726 . . . . 5 624 = 624
558 eqid 2726 . . . . . . . 8 62 = 62
559437oveq1i 7424 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 12528 . . . . . . . . . 10 12 ∈ ℂ
561560addridi 11440 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2754 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 12787 . . . . . . 7 (2 · 62) = 124
564563oveq1i 7424 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 12528 . . . . . . 7 124 ∈ ℂ
566565addridi 11440 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2754 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 11262 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2754 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 12787 . . . 4 (2 · 624) = 1248
571 eqid 2726 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 12783 . . . . . . 7 (31 + 9) = 40
573169addridi 11440 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2754 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 12736 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2726 . . . . . . . . 9 29 = 29
577575nn0cni 12528 . . . . . . . . . 10 14 ∈ ℂ
578577addlidi 11441 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 7426 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2754 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 12782 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 12773 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 12781 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 12846 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 12781 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 12779 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 12774 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 11443 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 7424 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2758 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 12774 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 7426 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2754 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 12844 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 12796 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 12783 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 12773 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 12774 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 12736 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2726 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 11445 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 12782 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 12773 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 7424 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2758 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 12773 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 12786 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 11442 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 12785 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 12787 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 7424 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 12736 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 12736 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 12736 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 12528 . . . . . . . 8 7290 ∈ ℂ
616615addridi 11440 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2754 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 12528 . . . . . . . 8 270 ∈ ℂ
619618mul01i 11443 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2754 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 12787 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2757 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 17064 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 14210 . . . 4 (2↑3) = 8
625624oveq1i 7424 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2726 . . . 4 1248 = 1248
627 eqid 2726 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 12752 . . . 4 (124 + 1) = 125
629 8p3e11 12802 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 12782 . . 3 (1248 + 3) = 1251
6319nncni 12266 . . . . . . 7 𝑁 ∈ ℂ
632631mullidi 11258 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2754 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 12752 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 11262 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 12752 . . . . . 6 ((3 · 8) + 1) = 25
637161mullidi 11258 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 7424 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 12801 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2754 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 12779 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 12786 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2757 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 17063 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2726 . . . 4 1251 = 1251
646 eqid 2726 . . . . . 6 125 = 125
647 eqid 2726 . . . . . . 7 12 = 12
648117, 232oveq12i 7426 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2754 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 7424 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 12743 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2758 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 12774 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 12787 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 12781 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 12787 . . 3 (2 · 1251) = 2502
6576, 2deccl 12736 . . . . 5 2502 ∈ ℕ0
658657nn0cni 12528 . . . 4 2502 ∈ ℂ
659 eqid 2726 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 12752 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2757 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 11516 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2757 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 11442 . . . 4 (0 · 𝑁) = 0
665664oveq1i 7424 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2757 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2757 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 17064 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  (class class class)co 7414  0cc0 11147  1c1 11148   + caddc 11150   · cmul 11152  cmin 11483  cn 12256  2c2 12311  3c3 12312  4c4 12313  5c5 12314  6c6 12315  7c7 12316  8c8 12317  9c9 12318  cdc 12721   mod cmo 13881  cexp 14073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736  ax-cnex 11203  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223  ax-pre-mulgt0 11224  ax-pre-sup 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366  df-rab 3421  df-v 3465  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-iun 4996  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6303  df-ord 6369  df-on 6370  df-lim 6371  df-suc 6372  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7867  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-sup 9476  df-inf 9477  df-pnf 11289  df-mnf 11290  df-xr 11291  df-ltxr 11292  df-le 11293  df-sub 11485  df-neg 11486  df-div 11911  df-nn 12257  df-2 12319  df-3 12320  df-4 12321  df-5 12322  df-6 12323  df-7 12324  df-8 12325  df-9 12326  df-n0 12517  df-z 12603  df-dec 12722  df-uz 12867  df-rp 13021  df-fl 13804  df-mod 13882  df-seq 14014  df-exp 14074
This theorem is referenced by:  2503prm  17135
  Copyright terms: Public domain W3C validator