MPE Home 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