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

Theorem 2503lem2 17116
Description: Lemma for 2503prm 17118. 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 12529 . . . . . 6 2 ∈ ℕ0
3 5nn0 12532 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12732 . . . . 5 25 ∈ ℕ0
5 0nn0 12527 . . . . 5 0 ∈ ℕ0
64, 5deccl 12732 . . . 4 250 ∈ ℕ0
7 3nn 12331 . . . 4 3 ∈ ℕ
86, 7decnncl 12737 . . 3 2503 ∈ ℕ
91, 8eqeltri 2825 . 2 𝑁 ∈ ℕ
10 2nn 12325 . 2 2 ∈ ℕ
11 1nn0 12528 . . . . 5 1 ∈ ℕ0
1211, 2deccl 12732 . . . 4 12 ∈ ℕ0
1312, 3deccl 12732 . . 3 125 ∈ ℕ0
1413, 11deccl 12732 . 2 1251 ∈ ℕ0
15 0z 12609 . 2 0 ∈ ℤ
16 4nn0 12531 . . . . 5 4 ∈ ℕ0
1712, 16deccl 12732 . . . 4 124 ∈ ℕ0
18 8nn0 12535 . . . 4 8 ∈ ℕ0
1917, 18deccl 12732 . . 3 1248 ∈ ℕ0
20 1z 12632 . . 3 1 ∈ ℤ
21 3nn0 12530 . . . . 5 3 ∈ ℕ0
2221, 11deccl 12732 . . . 4 31 ∈ ℕ0
2322, 21deccl 12732 . . 3 313 ∈ ℕ0
24 6nn0 12533 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 12732 . . . . 5 62 ∈ ℕ0
2625, 16deccl 12732 . . . 4 624 ∈ ℕ0
27 9nn0 12536 . . . . . 6 9 ∈ ℕ0
282, 27deccl 12732 . . . . 5 29 ∈ ℕ0
2928nn0zi 12627 . . . 4 29 ∈ ℤ
30 7nn0 12534 . . . . . 6 7 ∈ ℕ0
312, 30deccl 12732 . . . . 5 27 ∈ ℕ0
3231, 5deccl 12732 . . . 4 270 ∈ ℕ0
3322, 2deccl 12732 . . . . 5 312 ∈ ℕ0
342, 21deccl 12732 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 12732 . . . . . 6 238 ∈ ℕ0
3635nn0zi 12627 . . . . 5 238 ∈ ℤ
3730, 30deccl 12732 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 12732 . . . . 5 772 ∈ ℕ0
3911, 3deccl 12732 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 12732 . . . . . 6 156 ∈ ℕ0
4121nn0zi 12627 . . . . . 6 3 ∈ ℤ
4227, 11deccl 12732 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 12732 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 12627 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 12732 . . . . . . . 8 19 ∈ ℕ0
46 4nn 12335 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 12737 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 12732 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 12732 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 12732 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 12627 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 12732 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 12732 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 12732 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 12732 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 12732 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 12732 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 12732 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 12732 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 12627 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 12732 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 12732 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 12732 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 12732 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 12732 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 17115 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 12402 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2728 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 12748 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2728 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2728 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 12524 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addridi 11441 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2728 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 12524 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addridi 11441 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 12327 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mullidi 11259 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 12376 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 7438 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 12394 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2756 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 12340 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mullidi 11259 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 7436 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 12399 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 12739 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2760 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 12770 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 11206 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 11444 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 7436 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 12343 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addlidi 11442 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2760 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 12770 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 12333 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mullidi 11259 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 7436 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 12397 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 12739 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2760 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 12770 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2728 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2728 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 7436 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2756 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 12832 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 12782 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 12418 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 12781 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 12416 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 12781 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2759 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 17048 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2728 . . . . . . . . . . 11 19 = 19
117 2t1e2 12415 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 7436 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2756 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 12352 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 12839 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 11263 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 12783 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2728 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 12732 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 12732 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2728 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2728 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2728 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2728 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 12377 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 12412 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 11446 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 12771 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addlidi 11442 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 12771 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 12524 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addridi 11441 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 12732 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 12732 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2728 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 12739 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2728 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 12400 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 12524 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addlidi 11442 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 12748 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 12804 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 11446 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 12772 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2728 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 12401 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2728 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 12748 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 7437 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 12817 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addlidi 11442 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 12777 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2756 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 7436 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 12349 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 12801 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 11446 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2756 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 12769 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 12748 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 12769 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 12739 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 12337 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addlidi 11442 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2756 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 12374 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 7437 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 12820 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 12748 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2756 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 12818 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 11263 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 12410 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 12777 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 12769 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 12835 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addlidi 11442 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 12777 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 12769 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 12770 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 12524 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 11444 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 7436 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2760 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 12770 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 12739 . . . . . . . . . . . . 13 7 = 07
19321dec0h 12739 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2756 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 7437 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 12748 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2756 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 12419 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 7436 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 12805 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2756 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 12769 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 12833 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 12346 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 12793 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 11446 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 12778 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 12769 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 12770 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2728 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 12732 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 12732 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 12732 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2728 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2728 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 12739 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2728 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 7436 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2756 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 12719 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 11446 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 12773 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 11446 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 12771 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2728 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 12771 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 12771 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 12524 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addridi 11441 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2756 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 12414 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 11429 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 7438 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2756 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 7436 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 12395 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2760 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 12769 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulridi 11258 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 7436 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2756 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 12769 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 7436 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 11446 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2760 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 12769 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 12739 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 12739 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2756 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 7436 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2756 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 12768 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 7436 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addridi 11441 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2760 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 12769 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 7436 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 11446 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2760 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 12769 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 12770 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2756 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mullidi 11259 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 7438 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2756 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 7436 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2760 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 12769 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 12825 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 12748 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 12769 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 7436 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 12791 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2756 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 12769 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 12770 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 12524 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulridi 11258 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 12783 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2759 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 17047 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2728 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 12748 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2728 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2756 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 7438 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addridi 11441 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2756 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 12770 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 7436 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2760 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 12770 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 12770 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 7436 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2760 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 12769 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 11443 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 7436 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2760 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 12769 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 12826 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 12782 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2759 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 17048 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2728 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 11263 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 7436 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2756 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 12783 . . . . . . . 8 (2 · 39) = 78
310 eqid 2728 . . . . . . . . . 10 2309 = 2309
311 eqid 2728 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 12777 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 12524 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addridi 11441 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 12420 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 12387 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 7438 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 12799 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2756 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 12819 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 11263 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 12777 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 12770 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 11444 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 7436 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2760 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 12770 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 12815 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 12778 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 12770 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 12771 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 7436 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2760 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 12769 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 12769 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 12769 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 12770 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 12524 . . . . . . . . . . 11 111 ∈ ℂ
339338mulridi 11258 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 12783 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2759 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 17047 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2728 . . . . . . . 8 78 = 78
344 4p1e5 12398 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 11263 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 12748 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 11263 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 12783 . . . . . . 7 (2 · 78) = 156
349 eqid 2728 . . . . . . . . 9 194 = 194
3502, 16deccl 12732 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2728 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 12748 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2728 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 12748 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 12771 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 12758 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 12806 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 12772 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2759 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2728 . . . . . . . . 9 91 = 91
361 eqid 2728 . . . . . . . . . . . 12 15 = 15
362204addlidi 11442 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2756 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 7438 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2756 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 12777 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 12769 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 7438 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 12408 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2756 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 12769 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 12770 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 12524 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 11444 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 7436 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2760 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 12770 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 7438 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2756 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 12769 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 12770 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 12732 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2728 . . . . . . . . . 10 77 = 77
38411, 30deccl 12732 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 12732 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2728 . . . . . . . . . . . 12 175 = 175
387384nn0cni 12524 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addlidi 11442 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 12748 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 12794 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 12772 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 7438 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2756 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulridi 11258 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 7436 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 12810 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2756 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 12769 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulridi 11258 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 7436 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 12405 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2760 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 12769 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mullidi 11259 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addlidi 11442 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 7438 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2756 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 12846 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 11446 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 12777 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 12769 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 12841 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 11263 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 12795 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 11446 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 12778 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 12769 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 12770 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mullidi 11259 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 7438 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 12406 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2756 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 12748 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 12769 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 12816 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 12782 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 12783 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2759 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 17049 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2728 . . . . . . 7 156 = 156
431117, 172oveq12i 7438 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2756 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 11263 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 12748 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 12770 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 12821 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 11263 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 12783 . . . . . 6 (2 · 156) = 312
439 eqid 2728 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 12748 . . . . . . . . 9 (77 + 1) = 78
441204addridi 11441 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2756 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 7438 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 12411 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2756 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 11446 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 12778 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 12770 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 11444 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 7436 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2760 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 12770 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 7436 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2756 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 12770 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 12748 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 7436 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 12811 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2756 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 12775 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 12524 . . . . . . . . 9 91 ∈ ℂ
462461mulridi 11258 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 12783 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2759 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 17047 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2728 . . . . . 6 312 = 312
467 eqid 2728 . . . . . . . . 9 31 = 31
468306oveq1i 7436 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2756 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2756 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 12783 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 7436 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 12524 . . . . . . . 8 62 ∈ ℂ
474473addridi 11441 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2756 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2756 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 12783 . . . . 5 (2 · 312) = 624
478 eqid 2728 . . . . . . 7 270 = 270
47930, 11deccl 12732 . . . . . . 7 71 ∈ ℕ0
480 eqid 2728 . . . . . . . . 9 71 = 71
481 7p2e9 12413 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 11446 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 12771 . . . . . . . 8 (27 + 71) = 98
484120addridi 11441 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2756 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 12732 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2728 . . . . . . . . . 10 238 = 238
488486nn0cni 12524 . . . . . . . . . . 11 119 ∈ ℂ
489488addlidi 11442 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 12777 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 7438 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2756 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 7436 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2760 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 12769 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 12808 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 11446 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 12778 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 12769 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 7437 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2756 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 12769 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 12769 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 12770 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 12524 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 11444 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 7436 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2760 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 12770 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 7438 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2756 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 12769 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 12782 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 7436 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 12732 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 12524 . . . . . . . . 9 714 ∈ ℂ
517516addridi 11441 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2756 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 12770 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 12732 . . . . . . 7 154 ∈ ℕ0
521 eqid 2728 . . . . . . . 8 154 = 154
5223, 16deccl 12732 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 12732 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 12732 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2728 . . . . . . . . . 10 540 = 540
526 eqid 2728 . . . . . . . . . . 11 54 = 54
52783addlidi 11442 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 12771 . . . . . . . . . 10 (1 + 54) = 55
52983addridi 11441 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 12771 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2728 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 12748 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 12831 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 12788 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 12771 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 12778 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 12769 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 11446 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 12777 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 12769 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 7437 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 12807 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 12778 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2756 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 12758 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 12769 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 12407 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 12777 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 12769 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 12770 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 12748 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 12782 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 12781 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 12783 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2759 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 17047 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2728 . . . . 5 624 = 624
558 eqid 2728 . . . . . . . 8 62 = 62
559437oveq1i 7436 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 12524 . . . . . . . . . 10 12 ∈ ℂ
561560addridi 11441 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2756 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 12783 . . . . . . 7 (2 · 62) = 124
564563oveq1i 7436 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 12524 . . . . . . 7 124 ∈ ℂ
566565addridi 11441 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2756 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 11263 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2756 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 12783 . . . 4 (2 · 624) = 1248
571 eqid 2728 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 12779 . . . . . . 7 (31 + 9) = 40
573169addridi 11441 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2756 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 12732 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2728 . . . . . . . . 9 29 = 29
577575nn0cni 12524 . . . . . . . . . 10 14 ∈ ℂ
578577addlidi 11442 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 7438 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2756 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 12778 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 12769 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 12777 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 12842 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 12777 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 12775 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 12770 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 11444 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 7436 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2760 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 12770 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 7438 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2756 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 12840 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 12792 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 12779 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 12769 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 12770 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 12732 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2728 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 11446 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 12778 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 12769 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 7436 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2760 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 12769 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 12782 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 11443 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 12781 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 12783 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 7436 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 12732 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 12732 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 12732 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 12524 . . . . . . . 8 7290 ∈ ℂ
616615addridi 11441 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2756 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 12524 . . . . . . . 8 270 ∈ ℂ
619618mul01i 11444 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2756 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 12783 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2759 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 17047 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 14205 . . . 4 (2↑3) = 8
625624oveq1i 7436 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2728 . . . 4 1248 = 1248
627 eqid 2728 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 12748 . . . 4 (124 + 1) = 125
629 8p3e11 12798 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 12778 . . 3 (1248 + 3) = 1251
6319nncni 12262 . . . . . . 7 𝑁 ∈ ℂ
632631mullidi 11259 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2756 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 12748 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 11263 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 12748 . . . . . 6 ((3 · 8) + 1) = 25
637161mullidi 11259 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 7436 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 12797 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2756 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 12775 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 12782 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2759 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 17046 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2728 . . . 4 1251 = 1251
646 eqid 2728 . . . . . 6 125 = 125
647 eqid 2728 . . . . . . 7 12 = 12
648117, 232oveq12i 7438 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2756 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 7436 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 12739 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2760 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 12770 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 12783 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 12777 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 12783 . . 3 (2 · 1251) = 2502
6576, 2deccl 12732 . . . . 5 2502 ∈ ℕ0
658657nn0cni 12524 . . . 4 2502 ∈ ℂ
659 eqid 2728 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 12748 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2759 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 11517 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2759 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 11443 . . . 4 (0 · 𝑁) = 0
665664oveq1i 7436 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2759 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2759 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 17047 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7426  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cmin 11484  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  cdc 12717   mod cmo 13876  cexp 14068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-sup 9475  df-inf 9476  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069
This theorem is referenced by:  2503prm  17118
  Copyright terms: Public domain W3C validator