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

Theorem 2503lem2 16970
Description: Lemma for 2503prm 16972. 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 12389 . . . . . 6 2 ∈ ℕ0
3 5nn0 12392 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12592 . . . . 5 25 ∈ ℕ0
5 0nn0 12387 . . . . 5 0 ∈ ℕ0
64, 5deccl 12592 . . . 4 250 ∈ ℕ0
7 3nn 12191 . . . 4 3 ∈ ℕ
86, 7decnncl 12597 . . 3 2503 ∈ ℕ
91, 8eqeltri 2835 . 2 𝑁 ∈ ℕ
10 2nn 12185 . 2 2 ∈ ℕ
11 1nn0 12388 . . . . 5 1 ∈ ℕ0
1211, 2deccl 12592 . . . 4 12 ∈ ℕ0
1312, 3deccl 12592 . . 3 125 ∈ ℕ0
1413, 11deccl 12592 . 2 1251 ∈ ℕ0
15 0z 12469 . 2 0 ∈ ℤ
16 4nn0 12391 . . . . 5 4 ∈ ℕ0
1712, 16deccl 12592 . . . 4 124 ∈ ℕ0
18 8nn0 12395 . . . 4 8 ∈ ℕ0
1917, 18deccl 12592 . . 3 1248 ∈ ℕ0
20 1z 12492 . . 3 1 ∈ ℤ
21 3nn0 12390 . . . . 5 3 ∈ ℕ0
2221, 11deccl 12592 . . . 4 31 ∈ ℕ0
2322, 21deccl 12592 . . 3 313 ∈ ℕ0
24 6nn0 12393 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 12592 . . . . 5 62 ∈ ℕ0
2625, 16deccl 12592 . . . 4 624 ∈ ℕ0
27 9nn0 12396 . . . . . 6 9 ∈ ℕ0
282, 27deccl 12592 . . . . 5 29 ∈ ℕ0
2928nn0zi 12487 . . . 4 29 ∈ ℤ
30 7nn0 12394 . . . . . 6 7 ∈ ℕ0
312, 30deccl 12592 . . . . 5 27 ∈ ℕ0
3231, 5deccl 12592 . . . 4 270 ∈ ℕ0
3322, 2deccl 12592 . . . . 5 312 ∈ ℕ0
342, 21deccl 12592 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 12592 . . . . . 6 238 ∈ ℕ0
3635nn0zi 12487 . . . . 5 238 ∈ ℤ
3730, 30deccl 12592 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 12592 . . . . 5 772 ∈ ℕ0
3911, 3deccl 12592 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 12592 . . . . . 6 156 ∈ ℕ0
4121nn0zi 12487 . . . . . 6 3 ∈ ℤ
4227, 11deccl 12592 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 12592 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 12487 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 12592 . . . . . . . 8 19 ∈ ℕ0
46 4nn 12195 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 12597 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 12592 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 12592 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 12592 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 12487 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 12592 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 12592 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 12592 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 12592 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 12592 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 12592 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 12592 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 12592 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 12487 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 12592 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 12592 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 12592 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 12592 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 12592 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 16969 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 12262 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2738 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 12608 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2738 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2738 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 12384 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 11301 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2738 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 12384 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 11301 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 12187 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 11119 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 12236 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 7364 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 12254 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2766 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 12200 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 11119 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 7362 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 12259 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 12599 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2770 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 12630 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 11068 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 11304 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 7362 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 12203 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 11302 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2770 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 12630 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 12193 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 11119 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 7362 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 12257 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 12599 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2770 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 12630 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2738 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2738 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 7362 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2766 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 12692 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 12642 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 12278 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 12641 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 12276 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 12641 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2769 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 16902 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2738 . . . . . . . . . . 11 19 = 19
117 2t1e2 12275 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 7362 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2766 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 12212 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 12699 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 11123 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 12643 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2738 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 12592 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 12592 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2738 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2738 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2738 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2738 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 12237 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 12272 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 11306 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 12631 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 11302 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 12631 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 12384 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 11301 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 12592 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 12592 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2738 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 12599 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2738 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 12260 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 12384 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 11302 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 12608 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 12664 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 11306 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 12632 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2738 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 12261 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2738 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 12608 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 7363 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 12677 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 11302 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 12637 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2766 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 7362 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 12209 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 12661 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 11306 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2766 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 12629 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 12608 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 12629 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 12599 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 12197 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 11302 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2766 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 12234 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 7363 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 12680 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 12608 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2766 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 12678 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 11123 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 12270 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 12637 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 12629 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 12695 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 11302 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 12637 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 12629 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 12630 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 12384 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 11304 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 7362 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2770 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 12630 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 12599 . . . . . . . . . . . . 13 7 = 07
19321dec0h 12599 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2766 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 7363 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 12608 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2766 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 12279 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 7362 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 12665 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2766 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 12629 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 12693 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 12206 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 12653 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 11306 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 12638 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 12629 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 12630 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2738 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 12592 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 12592 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 12592 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2738 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2738 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 12599 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2738 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 7362 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2766 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 12579 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 11306 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 12633 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 11306 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 12631 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2738 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 12631 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 12631 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 12384 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 11301 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2766 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 12274 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 11289 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 7364 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2766 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 7362 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 12255 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2770 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 12629 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 11118 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 7362 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2766 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 12629 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 7362 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 11306 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2770 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 12629 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 12599 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 12599 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2766 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 7362 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2766 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 12628 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 7362 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 11301 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2770 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 12629 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 7362 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 11306 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2770 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 12629 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 12630 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2766 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 11119 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 7364 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2766 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 7362 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2770 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 12629 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 12685 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 12608 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 12629 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 7362 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 12651 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2766 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 12629 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 12630 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 12384 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 11118 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 12643 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2769 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 16901 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2738 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 12608 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2738 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2766 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 7364 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 11301 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2766 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 12630 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 7362 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2770 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 12630 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 12630 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 7362 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2770 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 12629 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 11303 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 7362 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2770 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 12629 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 12686 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 12642 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2769 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 16902 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2738 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 11123 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 7362 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2766 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 12643 . . . . . . . 8 (2 · 39) = 78
310 eqid 2738 . . . . . . . . . 10 2309 = 2309
311 eqid 2738 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 12637 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 12384 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 11301 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 12280 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 12247 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 7364 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 12659 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2766 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 12679 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 11123 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 12637 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 12630 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 11304 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 7362 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2770 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 12630 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 12675 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 12638 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 12630 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 12631 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 7362 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2770 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 12629 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 12629 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 12629 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 12630 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 12384 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 11118 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 12643 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2769 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 16901 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2738 . . . . . . . 8 78 = 78
344 4p1e5 12258 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 11123 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 12608 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 11123 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 12643 . . . . . . 7 (2 · 78) = 156
349 eqid 2738 . . . . . . . . 9 194 = 194
3502, 16deccl 12592 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2738 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 12608 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2738 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 12608 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 12631 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 12618 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 12666 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 12632 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2769 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2738 . . . . . . . . 9 91 = 91
361 eqid 2738 . . . . . . . . . . . 12 15 = 15
362204addid2i 11302 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2766 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 7364 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2766 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 12637 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 12629 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 7364 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 12268 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2766 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 12629 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 12630 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 12384 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 11304 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 7362 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2770 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 12630 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 7364 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2766 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 12629 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 12630 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 12592 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2738 . . . . . . . . . 10 77 = 77
38411, 30deccl 12592 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 12592 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2738 . . . . . . . . . . . 12 175 = 175
387384nn0cni 12384 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 11302 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 12608 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 12654 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 12632 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 7364 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2766 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 11118 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 7362 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 12670 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2766 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 12629 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 11118 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 7362 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 12265 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2770 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 12629 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 11119 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 11302 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 7364 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2766 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 12706 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 11306 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 12637 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 12629 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 12701 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 11123 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 12655 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 11306 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 12638 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 12629 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 12630 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 11119 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 7364 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 12266 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2766 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 12608 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 12629 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 12676 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 12642 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 12643 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2769 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 16903 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2738 . . . . . . 7 156 = 156
431117, 172oveq12i 7364 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2766 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 11123 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 12608 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 12630 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 12681 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 11123 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 12643 . . . . . 6 (2 · 156) = 312
439 eqid 2738 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 12608 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 11301 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2766 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 7364 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 12271 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2766 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 11306 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 12638 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 12630 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 11304 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 7362 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2770 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 12630 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 7362 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2766 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 12630 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 12608 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 7362 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 12671 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2766 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 12635 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 12384 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 11118 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 12643 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2769 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 16901 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2738 . . . . . 6 312 = 312
467 eqid 2738 . . . . . . . . 9 31 = 31
468306oveq1i 7362 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2766 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2766 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 12643 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 7362 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 12384 . . . . . . . 8 62 ∈ ℂ
474473addid1i 11301 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2766 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2766 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 12643 . . . . 5 (2 · 312) = 624
478 eqid 2738 . . . . . . 7 270 = 270
47930, 11deccl 12592 . . . . . . 7 71 ∈ ℕ0
480 eqid 2738 . . . . . . . . 9 71 = 71
481 7p2e9 12273 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 11306 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 12631 . . . . . . . 8 (27 + 71) = 98
484120addid1i 11301 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2766 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 12592 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2738 . . . . . . . . . 10 238 = 238
488486nn0cni 12384 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 11302 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 12637 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 7364 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2766 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 7362 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2770 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 12629 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 12668 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 11306 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 12638 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 12629 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 7363 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2766 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 12629 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 12629 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 12630 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 12384 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 11304 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 7362 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2770 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 12630 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 7364 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2766 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 12629 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 12642 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 7362 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 12592 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 12384 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 11301 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2766 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 12630 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 12592 . . . . . . 7 154 ∈ ℕ0
521 eqid 2738 . . . . . . . 8 154 = 154
5223, 16deccl 12592 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 12592 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 12592 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2738 . . . . . . . . . 10 540 = 540
526 eqid 2738 . . . . . . . . . . 11 54 = 54
52783addid2i 11302 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 12631 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 11301 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 12631 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2738 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 12608 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 12691 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 12648 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 12631 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 12638 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 12629 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 11306 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 12637 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 12629 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 7363 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 12667 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 12638 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2766 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 12618 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 12629 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 12267 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 12637 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 12629 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 12630 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 12608 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 12642 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 12641 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 12643 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2769 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 16901 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2738 . . . . 5 624 = 624
558 eqid 2738 . . . . . . . 8 62 = 62
559437oveq1i 7362 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 12384 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 11301 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2766 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 12643 . . . . . . 7 (2 · 62) = 124
564563oveq1i 7362 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 12384 . . . . . . 7 124 ∈ ℂ
566565addid1i 11301 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2766 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 11123 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2766 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 12643 . . . 4 (2 · 624) = 1248
571 eqid 2738 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 12639 . . . . . . 7 (31 + 9) = 40
573169addid1i 11301 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2766 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 12592 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2738 . . . . . . . . 9 29 = 29
577575nn0cni 12384 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 11302 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 7364 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2766 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 12638 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 12629 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 12637 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 12702 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 12637 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 12635 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 12630 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 11304 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 7362 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2770 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 12630 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 7364 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2766 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 12700 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 12652 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 12639 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 12629 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 12630 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 12592 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2738 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 11306 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 12638 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 12629 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 7362 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2770 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 12629 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 12642 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 11303 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 12641 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 12643 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 7362 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 12592 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 12592 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 12592 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 12384 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 11301 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2766 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 12384 . . . . . . . 8 270 ∈ ℂ
619618mul01i 11304 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2766 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 12643 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2769 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 16901 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 14057 . . . 4 (2↑3) = 8
625624oveq1i 7362 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2738 . . . 4 1248 = 1248
627 eqid 2738 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 12608 . . . 4 (124 + 1) = 125
629 8p3e11 12658 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 12638 . . 3 (1248 + 3) = 1251
6319nncni 12122 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 11119 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2766 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 12608 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 11123 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 12608 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 11119 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 7362 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 12657 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2766 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 12635 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 12642 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2769 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 16900 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2738 . . . 4 1251 = 1251
646 eqid 2738 . . . . . 6 125 = 125
647 eqid 2738 . . . . . . 7 12 = 12
648117, 232oveq12i 7364 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2766 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 7362 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 12599 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2770 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 12630 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 12643 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 12637 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 12643 . . 3 (2 · 1251) = 2502
6576, 2deccl 12592 . . . . 5 2502 ∈ ℕ0
658657nn0cni 12384 . . . 4 2502 ∈ ℂ
659 eqid 2738 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 12608 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2769 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 11377 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2769 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 11303 . . . 4 (0 · 𝑁) = 0
665664oveq1i 7362 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2769 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2769 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 16901 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7352  0cc0 11010  1c1 11011   + caddc 11013   · cmul 11015  cmin 11344  cn 12112  2c2 12167  3c3 12168  4c4 12169  5c5 12170  6c6 12171  7c7 12172  8c8 12173  9c9 12174  cdc 12577   mod cmo 13729  cexp 13922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7665  ax-cnex 11066  ax-resscn 11067  ax-1cn 11068  ax-icn 11069  ax-addcl 11070  ax-addrcl 11071  ax-mulcl 11072  ax-mulrcl 11073  ax-mulcom 11074  ax-addass 11075  ax-mulass 11076  ax-distr 11077  ax-i2m1 11078  ax-1ne0 11079  ax-1rid 11080  ax-rnegex 11081  ax-rrecex 11082  ax-cnre 11083  ax-pre-lttri 11084  ax-pre-lttrn 11085  ax-pre-ltadd 11086  ax-pre-mulgt0 11087  ax-pre-sup 11088
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-lim 6321  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7308  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7796  df-2nd 7915  df-frecs 8205  df-wrecs 8236  df-recs 8310  df-rdg 8349  df-er 8607  df-en 8843  df-dom 8844  df-sdom 8845  df-sup 9337  df-inf 9338  df-pnf 11150  df-mnf 11151  df-xr 11152  df-ltxr 11153  df-le 11154  df-sub 11346  df-neg 11347  df-div 11772  df-nn 12113  df-2 12175  df-3 12176  df-4 12177  df-5 12178  df-6 12179  df-7 12180  df-8 12181  df-9 12182  df-n0 12373  df-z 12459  df-dec 12578  df-uz 12723  df-rp 12871  df-fl 13652  df-mod 13730  df-seq 13862  df-exp 13923
This theorem is referenced by:  2503prm  16972
  Copyright terms: Public domain W3C validator