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

Theorem 2503lem2 16076
Description: Lemma for 2503prm 16078. 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 11596 . . . . . 6 2 ∈ ℕ0
3 5nn0 11599 . . . . . 6 5 ∈ ℕ0
42, 3deccl 11794 . . . . 5 25 ∈ ℕ0
5 0nn0 11594 . . . . 5 0 ∈ ℕ0
64, 5deccl 11794 . . . 4 250 ∈ ℕ0
7 3nn 11392 . . . 4 3 ∈ ℕ
86, 7decnncl 11799 . . 3 2503 ∈ ℕ
91, 8eqeltri 2892 . 2 𝑁 ∈ ℕ
10 2nn 11386 . 2 2 ∈ ℕ
11 1nn0 11595 . . . . 5 1 ∈ ℕ0
1211, 2deccl 11794 . . . 4 12 ∈ ℕ0
1312, 3deccl 11794 . . 3 125 ∈ ℕ0
1413, 11deccl 11794 . 2 1251 ∈ ℕ0
15 0z 11674 . 2 0 ∈ ℤ
16 4nn0 11598 . . . . 5 4 ∈ ℕ0
1712, 16deccl 11794 . . . 4 124 ∈ ℕ0
18 8nn0 11602 . . . 4 8 ∈ ℕ0
1917, 18deccl 11794 . . 3 1248 ∈ ℕ0
20 1z 11693 . . 3 1 ∈ ℤ
21 3nn0 11597 . . . . 5 3 ∈ ℕ0
2221, 11deccl 11794 . . . 4 31 ∈ ℕ0
2322, 21deccl 11794 . . 3 313 ∈ ℕ0
24 6nn0 11600 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 11794 . . . . 5 62 ∈ ℕ0
2625, 16deccl 11794 . . . 4 624 ∈ ℕ0
27 9nn0 11603 . . . . . 6 9 ∈ ℕ0
282, 27deccl 11794 . . . . 5 29 ∈ ℕ0
2928nn0zi 11688 . . . 4 29 ∈ ℤ
30 7nn0 11601 . . . . . 6 7 ∈ ℕ0
312, 30deccl 11794 . . . . 5 27 ∈ ℕ0
3231, 5deccl 11794 . . . 4 270 ∈ ℕ0
3322, 2deccl 11794 . . . . 5 312 ∈ ℕ0
342, 21deccl 11794 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 11794 . . . . . 6 238 ∈ ℕ0
3635nn0zi 11688 . . . . 5 238 ∈ ℤ
3730, 30deccl 11794 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 11794 . . . . 5 772 ∈ ℕ0
3911, 3deccl 11794 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 11794 . . . . . 6 156 ∈ ℕ0
4121nn0zi 11688 . . . . . 6 3 ∈ ℤ
4227, 11deccl 11794 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 11794 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 11688 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 11794 . . . . . . . 8 19 ∈ ℕ0
46 4nn 11397 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 11799 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 11794 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 11794 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 11794 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 11688 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 11794 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 11794 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 11794 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 11794 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 11794 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 11794 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 11794 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 11794 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 11688 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 11794 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 11794 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 11794 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 11794 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 11794 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 16075 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 11469 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2817 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 11810 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2817 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2817 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 11591 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 10518 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2817 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 11591 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 10518 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 11388 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 10340 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 11444 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 6896 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 11462 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2839 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 11403 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 10340 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 6894 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 11466 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 11801 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2843 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 11832 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 10289 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 10521 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 6894 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 11407 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 10519 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2843 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 11832 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 11394 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 10340 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 6894 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 11464 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 11801 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2843 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 11832 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2817 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2817 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 6894 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2839 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 11894 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 11844 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 11485 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 24, 109, 110decmul1 11843 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 11483 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 16, 111, 112decmul1 11843 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2842 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 16011 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2817 . . . . . . . . . . 11 19 = 19
117 2t1e2 11482 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 6894 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2839 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 11419 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 11901 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 10344 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 11845 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2817 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 11794 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 11794 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2817 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2817 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2817 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2817 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 11445 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 11479 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 10523 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 11833 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 10519 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 11833 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 11591 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 10518 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 11794 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 11794 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2817 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 11801 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2817 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 11467 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 11591 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 10519 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 11810 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 11866 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 10523 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 11834 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2817 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 11468 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2817 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 11810 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 6895 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 11879 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 10519 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 11839 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2839 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 6894 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 11415 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 11863 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 10523 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2839 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 11831 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 11810 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 11831 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 11801 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 11399 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 10519 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2839 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 11442 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 6895 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 11882 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 11810 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2839 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 11880 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 10344 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 11477 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 11839 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 11831 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 11897 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 10519 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 11839 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 11831 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 11832 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 11591 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 10521 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 6894 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2843 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 11832 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 11801 . . . . . . . . . . . . 13 7 = 07
19321dec0h 11801 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2839 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 6895 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 11810 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2839 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 11486 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 6894 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 11867 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2839 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 11831 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 11895 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 11411 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 11855 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 10523 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 11840 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 11831 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 11832 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2817 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 11794 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 11794 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 11794 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2817 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2817 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 11801 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2817 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 6894 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2839 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 11781 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 10523 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 11835 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 10523 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 11833 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2817 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 11833 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 11833 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 11591 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 10518 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2839 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 11481 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 10506 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 6896 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2839 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 6894 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 11463 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2843 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 11831 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 10339 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 6894 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2839 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 11831 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 6894 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 10523 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2843 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 11831 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 11801 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 11801 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2839 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 6894 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2839 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 11830 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 6894 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 10518 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2843 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 11831 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 6894 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 10523 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2843 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 11831 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 11832 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2839 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 10340 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 6896 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2839 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 6894 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2843 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 11831 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 11887 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 11810 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 11831 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 6894 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 11853 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2839 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 11831 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 11832 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 11591 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 10339 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 11845 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2842 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 16010 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2817 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 11810 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2817 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2839 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 6896 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 10518 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2839 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 11832 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 6894 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2843 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 11832 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 11832 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 6894 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2843 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 11831 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 10520 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 6894 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2843 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 11831 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 11888 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 11844 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2842 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 16011 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2817 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 10344 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 6894 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2839 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 11845 . . . . . . . 8 (2 · 39) = 78
310 eqid 2817 . . . . . . . . . 10 2309 = 2309
311 eqid 2817 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 11839 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 11591 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 10518 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 11487 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 11455 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 6896 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 11861 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2839 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 11881 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 10344 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 11839 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 11832 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 10521 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 6894 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2843 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 11832 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 11877 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 11840 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 11832 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 11833 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 6894 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2843 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 11831 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 11831 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 11831 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 11832 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 11591 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 10339 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 11845 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2842 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 16010 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2817 . . . . . . . 8 78 = 78
344 4p1e5 11465 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 10344 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 11810 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 10344 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 11845 . . . . . . 7 (2 · 78) = 156
349 eqid 2817 . . . . . . . . 9 194 = 194
3502, 16deccl 11794 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2817 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 11810 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2817 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 11810 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 11833 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 11820 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 11868 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 11834 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2842 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2817 . . . . . . . . 9 91 = 91
361 eqid 2817 . . . . . . . . . . . 12 15 = 15
362204addid2i 10519 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2839 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 6896 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2839 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 11839 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 11831 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 6896 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 11475 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2839 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 11831 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 11832 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 11591 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 10521 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 6894 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2843 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 11832 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 6896 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2839 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 11831 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 11832 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 11794 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2817 . . . . . . . . . 10 77 = 77
38411, 30deccl 11794 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 11794 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2817 . . . . . . . . . . . 12 175 = 175
387384nn0cni 11591 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 10519 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 11810 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 11856 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 11834 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 6896 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2839 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 10339 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 6894 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 11872 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2839 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 11831 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 10339 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 6894 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 11472 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2843 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 11831 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 10340 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 10519 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 6896 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2839 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 11908 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 10523 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 11839 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 11831 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 11903 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 10344 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 11857 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 10523 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 11840 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 11831 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 11832 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 10340 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 6896 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 11473 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2839 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 11810 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 11831 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 11878 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 11844 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 11845 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2842 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 16012 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2817 . . . . . . 7 156 = 156
431117, 172oveq12i 6896 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2839 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 10344 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 11810 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 11832 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 11883 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 10344 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 11845 . . . . . 6 (2 · 156) = 312
439 eqid 2817 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 11810 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 10518 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2839 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 6896 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 11478 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2839 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 10523 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 11840 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 11832 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 10521 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 6894 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2843 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 11832 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 6894 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2839 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 11832 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 11810 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 6894 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 11873 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2839 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 11837 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 11591 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 10339 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 11845 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2842 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 16010 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2817 . . . . . 6 312 = 312
467 eqid 2817 . . . . . . . . 9 31 = 31
468306oveq1i 6894 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2839 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2839 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 11845 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 6894 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 11591 . . . . . . . 8 62 ∈ ℂ
474473addid1i 10518 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2839 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2839 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 11845 . . . . 5 (2 · 312) = 624
478 eqid 2817 . . . . . . 7 270 = 270
47930, 11deccl 11794 . . . . . . 7 71 ∈ ℕ0
480 eqid 2817 . . . . . . . . 9 71 = 71
481 7p2e9 11480 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 10523 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 11833 . . . . . . . 8 (27 + 71) = 98
484120addid1i 10518 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2839 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 11794 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2817 . . . . . . . . . 10 238 = 238
488486nn0cni 11591 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 10519 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 11839 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 6896 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2839 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 6894 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2843 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 11831 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 11870 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 10523 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 11840 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 11831 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 6895 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2839 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 11831 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 11831 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 11832 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 11591 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 10521 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 6894 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2843 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 11832 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 6896 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2839 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 11831 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 11844 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 6894 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 11794 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 11591 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 10518 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2839 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 11832 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 11794 . . . . . . 7 154 ∈ ℕ0
521 eqid 2817 . . . . . . . 8 154 = 154
5223, 16deccl 11794 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 11794 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 11794 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2817 . . . . . . . . . 10 540 = 540
526 eqid 2817 . . . . . . . . . . 11 54 = 54
52783addid2i 10519 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 11833 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 10518 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 11833 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2817 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 11810 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 11893 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 11850 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 11833 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 11840 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 11831 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 10523 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 11839 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 11831 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 6895 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 11869 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 11840 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2839 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 11820 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 11831 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 11474 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 11839 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 11831 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 11832 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 11810 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 11844 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 16, 552, 112decmul1 11843 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 11845 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2842 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 16010 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2817 . . . . 5 624 = 624
558 eqid 2817 . . . . . . . 8 62 = 62
559437oveq1i 6894 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 11591 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 10518 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2839 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 11845 . . . . . . 7 (2 · 62) = 124
564563oveq1i 6894 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 11591 . . . . . . 7 124 ∈ ℂ
566565addid1i 10518 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2839 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 10344 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2839 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 11845 . . . 4 (2 · 624) = 1248
571 eqid 2817 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 11841 . . . . . . 7 (31 + 9) = 40
573169addid1i 10518 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2839 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 11794 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2817 . . . . . . . . 9 29 = 29
577575nn0cni 11591 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 10519 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 6896 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2839 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 11840 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 11831 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 11839 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 11904 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 11839 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 11837 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 11832 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 10521 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 6894 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2843 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 11832 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 6896 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2839 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 11902 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 11854 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 11841 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 11831 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 11832 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 11794 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2817 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 10523 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 11840 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 11831 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 6894 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2843 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 11831 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 11844 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 10520 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 5, 607, 608decmul1 11843 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 11845 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 6894 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 11794 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 11794 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 11794 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 11591 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 10518 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2839 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 11591 . . . . . . . 8 270 ∈ ℂ
619618mul01i 10521 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2839 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 11845 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2842 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 16010 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 13206 . . . 4 (2↑3) = 8
625624oveq1i 6894 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2817 . . . 4 1248 = 1248
627 eqid 2817 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 11810 . . . 4 (124 + 1) = 125
629 8p3e11 11860 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 11840 . . 3 (1248 + 3) = 1251
6319nncni 11326 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 10340 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2839 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 11810 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 10344 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 11810 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 10340 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 6894 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 11859 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2839 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 11837 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 11844 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2842 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 16009 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2817 . . . 4 1251 = 1251
646 eqid 2817 . . . . . 6 125 = 125
647 eqid 2817 . . . . . . 7 12 = 12
648117, 232oveq12i 6896 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2839 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 6894 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 11801 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2843 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 11832 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 11845 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 11839 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 11845 . . 3 (2 · 1251) = 2502
6576, 2deccl 11794 . . . . 5 2502 ∈ ℕ0
658657nn0cni 11591 . . . 4 2502 ∈ ℂ
659 eqid 2817 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 11810 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2842 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 10593 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2842 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 10520 . . . 4 (0 · 𝑁) = 0
665664oveq1i 6894 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2842 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2842 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 16010 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  (class class class)co 6884  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236  cmin 10561  cn 11315  2c2 11368  3c3 11369  4c4 11370  5c5 11371  6c6 11372  7c7 11373  8c8 11374  9c9 11375  cdc 11779   mod cmo 12912  cexp 13103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-2nd 7409  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-sup 8597  df-inf 8598  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-rp 12067  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104
This theorem is referenced by:  2503prm  16078
  Copyright terms: Public domain W3C validator