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

Theorem 2503lem2 17080
Description: Lemma for 2503prm 17082. 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 12493 . . . . . 6 2 ∈ ℕ0
3 5nn0 12496 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12696 . . . . 5 25 ∈ ℕ0
5 0nn0 12491 . . . . 5 0 ∈ ℕ0
64, 5deccl 12696 . . . 4 250 ∈ ℕ0
7 3nn 12295 . . . 4 3 ∈ ℕ
86, 7decnncl 12701 . . 3 2503 ∈ ℕ
91, 8eqeltri 2823 . 2 𝑁 ∈ ℕ
10 2nn 12289 . 2 2 ∈ ℕ
11 1nn0 12492 . . . . 5 1 ∈ ℕ0
1211, 2deccl 12696 . . . 4 12 ∈ ℕ0
1312, 3deccl 12696 . . 3 125 ∈ ℕ0
1413, 11deccl 12696 . 2 1251 ∈ ℕ0
15 0z 12573 . 2 0 ∈ ℤ
16 4nn0 12495 . . . . 5 4 ∈ ℕ0
1712, 16deccl 12696 . . . 4 124 ∈ ℕ0
18 8nn0 12499 . . . 4 8 ∈ ℕ0
1917, 18deccl 12696 . . 3 1248 ∈ ℕ0
20 1z 12596 . . 3 1 ∈ ℤ
21 3nn0 12494 . . . . 5 3 ∈ ℕ0
2221, 11deccl 12696 . . . 4 31 ∈ ℕ0
2322, 21deccl 12696 . . 3 313 ∈ ℕ0
24 6nn0 12497 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 12696 . . . . 5 62 ∈ ℕ0
2625, 16deccl 12696 . . . 4 624 ∈ ℕ0
27 9nn0 12500 . . . . . 6 9 ∈ ℕ0
282, 27deccl 12696 . . . . 5 29 ∈ ℕ0
2928nn0zi 12591 . . . 4 29 ∈ ℤ
30 7nn0 12498 . . . . . 6 7 ∈ ℕ0
312, 30deccl 12696 . . . . 5 27 ∈ ℕ0
3231, 5deccl 12696 . . . 4 270 ∈ ℕ0
3322, 2deccl 12696 . . . . 5 312 ∈ ℕ0
342, 21deccl 12696 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 12696 . . . . . 6 238 ∈ ℕ0
3635nn0zi 12591 . . . . 5 238 ∈ ℤ
3730, 30deccl 12696 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 12696 . . . . 5 772 ∈ ℕ0
3911, 3deccl 12696 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 12696 . . . . . 6 156 ∈ ℕ0
4121nn0zi 12591 . . . . . 6 3 ∈ ℤ
4227, 11deccl 12696 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 12696 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 12591 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 12696 . . . . . . . 8 19 ∈ ℕ0
46 4nn 12299 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 12701 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 12696 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 12696 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 12696 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 12591 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 12696 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 12696 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 12696 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 12696 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 12696 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 12696 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 12696 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 12696 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 12591 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 12696 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 12696 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 12696 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 12696 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 12696 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 17079 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 12366 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2726 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 12712 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2726 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2726 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 12488 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addridi 11405 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2726 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 12488 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addridi 11405 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 12291 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mullidi 11223 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 12340 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 7417 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 12358 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2754 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 12304 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mullidi 11223 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 7415 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 12363 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 12703 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 12734 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 11170 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 11408 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 7415 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 12307 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addlidi 11406 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2758 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 12734 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 12297 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mullidi 11223 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 7415 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 12361 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 12703 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2758 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 12734 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2726 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2726 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 7415 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2754 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 12796 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 12746 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 12382 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 12745 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 12380 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 12745 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2757 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 17012 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2726 . . . . . . . . . . 11 19 = 19
117 2t1e2 12379 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 7415 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2754 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 12316 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 12803 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 11227 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 12747 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2726 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 12696 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 12696 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2726 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2726 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2726 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2726 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 12341 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 12376 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 11410 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 12735 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addlidi 11406 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 12735 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 12488 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addridi 11405 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 12696 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 12696 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2726 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 12703 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2726 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 12364 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 12488 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addlidi 11406 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 12712 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 12768 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 11410 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 12736 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2726 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 12365 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2726 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 12712 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 7416 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 12781 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addlidi 11406 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 12741 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2754 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 12313 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 12765 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 11410 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2754 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 12733 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 12712 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 12733 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 12703 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 12301 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addlidi 11406 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2754 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 12338 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 7416 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 12784 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 12712 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2754 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 12782 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 11227 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 12374 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 12741 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 12733 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 12799 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addlidi 11406 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 12741 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 12733 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 12734 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 12488 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 11408 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 7415 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2758 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 12734 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 12703 . . . . . . . . . . . . 13 7 = 07
19321dec0h 12703 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2754 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 7416 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 12712 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2754 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 12383 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 7415 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 12769 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2754 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 12733 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 12797 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 12310 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 12757 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 11410 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 12742 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 12733 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 12734 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2726 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 12696 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 12696 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 12696 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2726 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2726 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 12703 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2726 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2754 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 12683 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 11410 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 12737 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 11410 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 12735 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2726 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 12735 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 12735 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 12488 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addridi 11405 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2754 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 12378 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 11393 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 7417 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2754 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 7415 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 12359 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2758 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 12733 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulridi 11222 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2754 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 12733 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 7415 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 11410 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 12733 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 12703 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 12703 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2754 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 7415 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2754 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 12732 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addridi 11405 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2758 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 12733 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 7415 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 11410 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2758 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 12733 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 12734 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2754 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mullidi 11223 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 7417 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2754 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 7415 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2758 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 12733 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 12789 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 12712 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 12733 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 7415 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 12755 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2754 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 12733 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 12734 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 12488 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulridi 11222 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 12747 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2757 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 17011 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2726 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 12712 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2726 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2754 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 7417 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addridi 11405 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2754 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 12734 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 7415 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2758 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 12734 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 12734 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 7415 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2758 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 12733 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 11407 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 7415 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2758 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 12733 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 12790 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 12746 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2757 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 17012 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2726 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 11227 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 7415 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2754 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 12747 . . . . . . . 8 (2 · 39) = 78
310 eqid 2726 . . . . . . . . . 10 2309 = 2309
311 eqid 2726 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 12741 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 12488 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addridi 11405 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 12384 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 12351 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 7417 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 12763 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2754 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 12783 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 11227 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 12741 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 12734 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 11408 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 7415 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2758 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 12734 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 12779 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 12742 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 12734 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 12735 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 7415 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2758 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 12733 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 12733 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 12733 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 12734 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 12488 . . . . . . . . . . 11 111 ∈ ℂ
339338mulridi 11222 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 12747 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2757 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 17011 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2726 . . . . . . . 8 78 = 78
344 4p1e5 12362 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 11227 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 12712 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 11227 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 12747 . . . . . . 7 (2 · 78) = 156
349 eqid 2726 . . . . . . . . 9 194 = 194
3502, 16deccl 12696 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2726 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 12712 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2726 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 12712 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 12735 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 12722 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 12770 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 12736 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2757 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2726 . . . . . . . . 9 91 = 91
361 eqid 2726 . . . . . . . . . . . 12 15 = 15
362204addlidi 11406 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2754 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 7417 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2754 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 12741 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 12733 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 7417 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 12372 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2754 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 12733 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 12734 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 12488 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 11408 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 7415 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2758 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 12734 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 7417 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2754 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 12733 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 12734 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 12696 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2726 . . . . . . . . . 10 77 = 77
38411, 30deccl 12696 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 12696 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2726 . . . . . . . . . . . 12 175 = 175
387384nn0cni 12488 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addlidi 11406 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 12712 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 12758 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 12736 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 7417 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2754 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulridi 11222 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 7415 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 12774 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2754 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 12733 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulridi 11222 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 7415 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 12369 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2758 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 12733 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mullidi 11223 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addlidi 11406 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 7417 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2754 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 12810 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 11410 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 12741 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 12733 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 12805 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 11227 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 12759 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 11410 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 12742 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 12733 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 12734 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mullidi 11223 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 7417 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 12370 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2754 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 12712 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 12733 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 12780 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 12746 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 12747 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2757 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 17013 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2726 . . . . . . 7 156 = 156
431117, 172oveq12i 7417 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2754 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 11227 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 12712 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 12734 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 12785 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 11227 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 12747 . . . . . 6 (2 · 156) = 312
439 eqid 2726 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 12712 . . . . . . . . 9 (77 + 1) = 78
441204addridi 11405 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2754 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 7417 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 12375 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2754 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 11410 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 12742 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 12734 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 11408 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 7415 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2758 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 12734 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 7415 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2754 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 12734 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 12712 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 7415 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 12775 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2754 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 12739 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 12488 . . . . . . . . 9 91 ∈ ℂ
462461mulridi 11222 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 12747 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2757 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 17011 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2726 . . . . . 6 312 = 312
467 eqid 2726 . . . . . . . . 9 31 = 31
468306oveq1i 7415 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2754 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2754 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 12747 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 7415 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 12488 . . . . . . . 8 62 ∈ ℂ
474473addridi 11405 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2754 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2754 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 12747 . . . . 5 (2 · 312) = 624
478 eqid 2726 . . . . . . 7 270 = 270
47930, 11deccl 12696 . . . . . . 7 71 ∈ ℕ0
480 eqid 2726 . . . . . . . . 9 71 = 71
481 7p2e9 12377 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 11410 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 12735 . . . . . . . 8 (27 + 71) = 98
484120addridi 11405 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2754 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 12696 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2726 . . . . . . . . . 10 238 = 238
488486nn0cni 12488 . . . . . . . . . . 11 119 ∈ ℂ
489488addlidi 11406 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 12741 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 7417 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2754 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 7415 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2758 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 12733 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 12772 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 11410 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 12742 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 12733 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 7416 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2754 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 12733 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 12733 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 12734 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 12488 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 11408 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 7415 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2758 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 12734 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 7417 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2754 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 12733 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 12746 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 7415 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 12696 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 12488 . . . . . . . . 9 714 ∈ ℂ
517516addridi 11405 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2754 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 12734 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 12696 . . . . . . 7 154 ∈ ℕ0
521 eqid 2726 . . . . . . . 8 154 = 154
5223, 16deccl 12696 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 12696 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 12696 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2726 . . . . . . . . . 10 540 = 540
526 eqid 2726 . . . . . . . . . . 11 54 = 54
52783addlidi 11406 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 12735 . . . . . . . . . 10 (1 + 54) = 55
52983addridi 11405 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 12735 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2726 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 12712 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 12795 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 12752 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 12735 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 12742 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 12733 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 11410 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 12741 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 12733 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 7416 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 12771 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 12742 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2754 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 12722 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 12733 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 12371 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 12741 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 12733 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 12734 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 12712 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 12746 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 12745 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 12747 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2757 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 17011 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2726 . . . . 5 624 = 624
558 eqid 2726 . . . . . . . 8 62 = 62
559437oveq1i 7415 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 12488 . . . . . . . . . 10 12 ∈ ℂ
561560addridi 11405 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2754 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 12747 . . . . . . 7 (2 · 62) = 124
564563oveq1i 7415 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 12488 . . . . . . 7 124 ∈ ℂ
566565addridi 11405 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2754 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 11227 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2754 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 12747 . . . 4 (2 · 624) = 1248
571 eqid 2726 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 12743 . . . . . . 7 (31 + 9) = 40
573169addridi 11405 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2754 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 12696 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2726 . . . . . . . . 9 29 = 29
577575nn0cni 12488 . . . . . . . . . 10 14 ∈ ℂ
578577addlidi 11406 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 7417 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2754 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 12742 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 12733 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 12741 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 12806 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 12741 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 12739 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 12734 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 11408 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 7415 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2758 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 12734 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 7417 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2754 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 12804 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 12756 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 12743 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 12733 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 12734 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 12696 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2726 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 11410 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 12742 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 12733 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 7415 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2758 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 12733 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 12746 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 11407 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 12745 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 12747 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 7415 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 12696 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 12696 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 12696 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 12488 . . . . . . . 8 7290 ∈ ℂ
616615addridi 11405 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2754 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 12488 . . . . . . . 8 270 ∈ ℂ
619618mul01i 11408 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2754 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 12747 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2757 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 17011 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 14169 . . . 4 (2↑3) = 8
625624oveq1i 7415 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2726 . . . 4 1248 = 1248
627 eqid 2726 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 12712 . . . 4 (124 + 1) = 125
629 8p3e11 12762 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 12742 . . 3 (1248 + 3) = 1251
6319nncni 12226 . . . . . . 7 𝑁 ∈ ℂ
632631mullidi 11223 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2754 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 12712 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 11227 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 12712 . . . . . 6 ((3 · 8) + 1) = 25
637161mullidi 11223 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 7415 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 12761 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2754 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 12739 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 12746 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2757 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 17010 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2726 . . . 4 1251 = 1251
646 eqid 2726 . . . . . 6 125 = 125
647 eqid 2726 . . . . . . 7 12 = 12
648117, 232oveq12i 7417 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2754 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 7415 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 12703 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2758 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 12734 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 12747 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 12741 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 12747 . . 3 (2 · 1251) = 2502
6576, 2deccl 12696 . . . . 5 2502 ∈ ℕ0
658657nn0cni 12488 . . . 4 2502 ∈ ℂ
659 eqid 2726 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 12712 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2757 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 11481 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2757 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 11407 . . . 4 (0 · 𝑁) = 0
665664oveq1i 7415 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2757 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2757 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 17011 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7405  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117  cmin 11448  cn 12216  2c2 12271  3c3 12272  4c4 12273  5c5 12274  6c6 12275  7c7 12276  8c8 12277  9c9 12278  cdc 12681   mod cmo 13840  cexp 14032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-rp 12981  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033
This theorem is referenced by:  2503prm  17082
  Copyright terms: Public domain W3C validator