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

Theorem 2503lem2 16047
 Description: Lemma for 2503prm 16049. 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 11501 . . . . . 6 2 ∈ ℕ0
3 5nn0 11504 . . . . . 6 5 ∈ ℕ0
42, 3deccl 11704 . . . . 5 25 ∈ ℕ0
5 0nn0 11499 . . . . 5 0 ∈ ℕ0
64, 5deccl 11704 . . . 4 250 ∈ ℕ0
7 3nn 11378 . . . 4 3 ∈ ℕ
86, 7decnncl 11710 . . 3 2503 ∈ ℕ
91, 8eqeltri 2835 . 2 𝑁 ∈ ℕ
10 2nn 11377 . 2 2 ∈ ℕ
11 1nn0 11500 . . . . 5 1 ∈ ℕ0
1211, 2deccl 11704 . . . 4 12 ∈ ℕ0
1312, 3deccl 11704 . . 3 125 ∈ ℕ0
1413, 11deccl 11704 . 2 1251 ∈ ℕ0
15 0z 11580 . 2 0 ∈ ℤ
16 4nn0 11503 . . . . 5 4 ∈ ℕ0
1712, 16deccl 11704 . . . 4 124 ∈ ℕ0
18 8nn0 11507 . . . 4 8 ∈ ℕ0
1917, 18deccl 11704 . . 3 1248 ∈ ℕ0
20 1z 11599 . . 3 1 ∈ ℤ
21 3nn0 11502 . . . . 5 3 ∈ ℕ0
2221, 11deccl 11704 . . . 4 31 ∈ ℕ0
2322, 21deccl 11704 . . 3 313 ∈ ℕ0
24 6nn0 11505 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 11704 . . . . 5 62 ∈ ℕ0
2625, 16deccl 11704 . . . 4 624 ∈ ℕ0
27 9nn0 11508 . . . . . 6 9 ∈ ℕ0
282, 27deccl 11704 . . . . 5 29 ∈ ℕ0
2928nn0zi 11594 . . . 4 29 ∈ ℤ
30 7nn0 11506 . . . . . 6 7 ∈ ℕ0
312, 30deccl 11704 . . . . 5 27 ∈ ℕ0
3231, 5deccl 11704 . . . 4 270 ∈ ℕ0
3322, 2deccl 11704 . . . . 5 312 ∈ ℕ0
342, 21deccl 11704 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 11704 . . . . . 6 238 ∈ ℕ0
3635nn0zi 11594 . . . . 5 238 ∈ ℤ
3730, 30deccl 11704 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 11704 . . . . 5 772 ∈ ℕ0
3911, 3deccl 11704 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 11704 . . . . . 6 156 ∈ ℕ0
4121nn0zi 11594 . . . . . 6 3 ∈ ℤ
4227, 11deccl 11704 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 11704 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 11594 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 11704 . . . . . . . 8 19 ∈ ℕ0
46 4nn 11379 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 11710 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 11704 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 11704 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 11704 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 11594 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 11704 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 11704 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 11704 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 11704 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 11704 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 11704 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 11704 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 11704 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 11594 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 11704 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 11704 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 11704 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 11704 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 11704 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 16046 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 11350 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2760 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 11727 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2760 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2760 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 11496 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 10415 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2760 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 11496 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 10415 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 11283 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 10235 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 11325 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 6825 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 11343 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2782 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 11292 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 10235 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 6823 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 11347 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 11714 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2786 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 11760 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 10186 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 10418 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 6823 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 11294 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 10416 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2786 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 11760 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 11287 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 10235 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 6823 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 11345 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 11714 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2786 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 11760 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2760 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2760 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 6823 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2782 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 11846 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 11779 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 11371 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 24, 109, 110decmul1 11777 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 11369 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 16, 111, 112decmul1 11777 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2785 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 15976 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2760 . . . . . . . . . . 11 19 = 19
117 2t1e2 11368 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 6823 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2782 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 11300 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 11855 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 10239 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 11781 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2760 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 11704 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 11704 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2760 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2760 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2760 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2760 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 11326 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 11362 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 10420 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 11762 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 10416 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 11762 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 11496 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 10415 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 11704 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 11704 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2760 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 11714 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2760 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 11348 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 11496 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 10416 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 11727 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 11811 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 10420 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 11764 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2760 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 11349 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2760 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 11727 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 6824 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 11826 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 10416 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 11771 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2782 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 11298 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 11808 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 10420 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2782 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 11758 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 11727 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 11758 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 11714 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 11290 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 10416 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2782 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 11324 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 6824 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 11831 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 11727 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2782 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 11827 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 10239 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 11359 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 11771 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 11758 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 11849 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 10416 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 11771 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 11758 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 11760 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 11496 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 10418 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 6823 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2786 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 11760 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 11714 . . . . . . . . . . . . 13 7 = 07
19321dec0h 11714 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2782 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 6824 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 11727 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2782 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 11372 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 6823 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 11813 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2782 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 11758 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 11847 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 11296 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 11797 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 10420 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 11772 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 11758 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 11760 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2760 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 11704 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 11704 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 11704 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2760 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2760 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 11714 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2760 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2782 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 11688 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 10420 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 11767 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 10420 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 11762 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2760 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 11762 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 11762 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 11496 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 10415 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2782 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 11367 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 10403 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 6825 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2782 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 6823 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 11344 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2786 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 11758 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 10234 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2782 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 11758 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 6823 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 10420 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2786 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 11758 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 11714 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 11714 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2782 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 6823 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2782 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 11756 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 10415 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2786 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 11758 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 6823 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 10420 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2786 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 11758 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 11760 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2782 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 10235 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 6825 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2782 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 6823 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2786 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 11758 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 11838 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 11727 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 11758 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 6823 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 11794 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2782 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 11758 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 11760 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 11496 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 10234 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 11781 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2785 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 15975 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2760 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 11727 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2760 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2782 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 6825 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 10415 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2782 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 11760 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 6823 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2786 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 11760 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 11760 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 6823 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2786 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 11758 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 10417 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 6823 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2786 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 11758 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 11840 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 11779 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2785 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 15976 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2760 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 10239 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 6823 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2782 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 11781 . . . . . . . 8 (2 · 39) = 78
310 eqid 2760 . . . . . . . . . 10 2309 = 2309
311 eqid 2760 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 11771 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 11496 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 10415 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 11373 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 11336 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 6825 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 11806 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2782 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 11829 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 10239 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 11771 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 11760 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 10418 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 6823 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2786 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 11760 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 11824 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 11772 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 11760 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 11762 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 6823 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2786 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 11758 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 11758 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 11758 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 11760 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 11496 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 10234 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 11781 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2785 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 15975 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2760 . . . . . . . 8 78 = 78
344 4p1e5 11346 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 10239 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 11727 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 10239 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 11781 . . . . . . 7 (2 · 78) = 156
349 eqid 2760 . . . . . . . . 9 194 = 194
3502, 16deccl 11704 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2760 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 11727 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2760 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 11727 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 11762 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 11742 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 11814 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 11764 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2785 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2760 . . . . . . . . 9 91 = 91
361 eqid 2760 . . . . . . . . . . . 12 15 = 15
362204addid2i 10416 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2782 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 6825 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2782 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 11771 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 11758 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 6825 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 11357 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2782 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 11758 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 11760 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 11496 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 10418 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 6823 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2786 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 11760 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 6825 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2782 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 11758 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 11760 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 11704 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2760 . . . . . . . . . 10 77 = 77
38411, 30deccl 11704 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 11704 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2760 . . . . . . . . . . . 12 175 = 175
387384nn0cni 11496 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 10416 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 11727 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 11799 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 11764 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 6825 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2782 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 10234 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 6823 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 11818 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2782 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 11758 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 10234 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 6823 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 11354 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2786 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 11758 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 10235 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 10416 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 6825 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2782 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 11862 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 10420 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 11771 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 11758 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 11857 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 10239 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 11800 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 10420 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 11772 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 11758 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 11760 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 10235 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 6825 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 11355 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2782 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 11727 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 11758 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 11825 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 11779 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 11781 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2785 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 15977 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2760 . . . . . . 7 156 = 156
431117, 172oveq12i 6825 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2782 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 10239 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 11727 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 11760 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 11833 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 10239 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 11781 . . . . . 6 (2 · 156) = 312
439 eqid 2760 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 11727 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 10415 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2782 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 6825 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 11361 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2782 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 10420 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 11772 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 11760 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 10418 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 6823 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2786 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 11760 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 6823 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2782 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 11760 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 11727 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 6823 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 11819 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2782 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 11769 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 11496 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 10234 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 11781 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2785 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 15975 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2760 . . . . . 6 312 = 312
467 eqid 2760 . . . . . . . . 9 31 = 31
468306oveq1i 6823 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2782 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2782 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 11781 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 6823 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 11496 . . . . . . . 8 62 ∈ ℂ
474473addid1i 10415 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2782 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2782 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 11781 . . . . 5 (2 · 312) = 624
478 eqid 2760 . . . . . . 7 270 = 270
47930, 11deccl 11704 . . . . . . 7 71 ∈ ℕ0
480 eqid 2760 . . . . . . . . 9 71 = 71
481 7p2e9 11364 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 10420 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 11762 . . . . . . . 8 (27 + 71) = 98
484120addid1i 10415 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2782 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 11704 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2760 . . . . . . . . . 10 238 = 238
488486nn0cni 11496 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 10416 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 11771 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 6825 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2782 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 6823 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2786 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 11758 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 11816 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 10420 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 11772 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 11758 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 6824 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2782 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 11758 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 11758 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 11760 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 11496 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 10418 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 6823 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2786 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 11760 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 6825 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2782 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 11758 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 11779 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 6823 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 11704 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 11496 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 10415 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2782 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 11760 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 11704 . . . . . . 7 154 ∈ ℕ0
521 eqid 2760 . . . . . . . 8 154 = 154
5223, 16deccl 11704 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 11704 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 11704 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2760 . . . . . . . . . 10 540 = 540
526 eqid 2760 . . . . . . . . . . 11 54 = 54
52783addid2i 10416 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 11762 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 10415 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 11762 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2760 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 11727 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 11845 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 11788 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 11762 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 11772 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 11758 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 10420 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 11771 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 11758 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 6824 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 11815 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 11772 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2782 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 11742 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 11758 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 11356 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 11771 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 11758 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 11760 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 11727 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 11779 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 16, 552, 112decmul1 11777 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 11781 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2785 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 15975 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2760 . . . . 5 624 = 624
558 eqid 2760 . . . . . . . 8 62 = 62
559437oveq1i 6823 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 11496 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 10415 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2782 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 11781 . . . . . . 7 (2 · 62) = 124
564563oveq1i 6823 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 11496 . . . . . . 7 124 ∈ ℂ
566565addid1i 10415 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2782 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 10239 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2782 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 11781 . . . 4 (2 · 624) = 1248
571 eqid 2760 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 11773 . . . . . . 7 (31 + 9) = 40
573169addid1i 10415 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2782 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 11704 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2760 . . . . . . . . 9 29 = 29
577575nn0cni 11496 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 10416 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 6825 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2782 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 11772 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 11758 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 11771 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 11858 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 11771 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 11769 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 11760 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 10418 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 6823 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2786 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 11760 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 6825 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2782 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 11856 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 11795 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 11773 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 11758 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 11760 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 11704 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2760 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 10420 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 11772 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 11758 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 6823 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2786 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 11758 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 11779 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 10417 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 5, 607, 608decmul1 11777 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 11781 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 6823 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 11704 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 11704 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 11704 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 11496 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 10415 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2782 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 11496 . . . . . . . 8 270 ∈ ℂ
619618mul01i 10418 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2782 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 11781 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2785 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 15975 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 13157 . . . 4 (2↑3) = 8
625624oveq1i 6823 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2760 . . . 4 1248 = 1248
627 eqid 2760 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 11727 . . . 4 (124 + 1) = 125
629 8p3e11 11804 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 11772 . . 3 (1248 + 3) = 1251
6319nncni 11222 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 10235 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2782 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 11727 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 10239 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 11727 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 10235 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 6823 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 11802 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2782 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 11769 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 11779 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2785 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 15974 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2760 . . . 4 1251 = 1251
646 eqid 2760 . . . . . 6 125 = 125
647 eqid 2760 . . . . . . 7 12 = 12
648117, 232oveq12i 6825 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2782 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 6823 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 11714 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2786 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 11760 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 11781 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 11771 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 11781 . . 3 (2 · 1251) = 2502
6576, 2deccl 11704 . . . . 5 2502 ∈ ℕ0
658657nn0cni 11496 . . . 4 2502 ∈ ℂ
659 eqid 2760 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 11727 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2785 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 10490 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2785 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 10417 . . . 4 (0 · 𝑁) = 0
665664oveq1i 6823 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2785 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2785 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 15975 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1632  (class class class)co 6813  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133   − cmin 10458  ℕcn 11212  2c2 11262  3c3 11263  4c4 11264  5c5 11265  6c6 11266  7c7 11267  8c8 11268  9c9 11269  ;cdc 11685   mod cmo 12862  ↑cexp 13054 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055 This theorem is referenced by:  2503prm  16049
 Copyright terms: Public domain W3C validator