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

Theorem 2503lem2 15769
Description: Lemma for 2503prm 15771. 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 11253 . . . . . 6 2 ∈ ℕ0
3 5nn0 11256 . . . . . 6 5 ∈ ℕ0
42, 3deccl 11456 . . . . 5 25 ∈ ℕ0
5 0nn0 11251 . . . . 5 0 ∈ ℕ0
64, 5deccl 11456 . . . 4 250 ∈ ℕ0
7 3nn 11130 . . . 4 3 ∈ ℕ
86, 7decnncl 11462 . . 3 2503 ∈ ℕ
91, 8eqeltri 2694 . 2 𝑁 ∈ ℕ
10 2nn 11129 . 2 2 ∈ ℕ
11 1nn0 11252 . . . . 5 1 ∈ ℕ0
1211, 2deccl 11456 . . . 4 12 ∈ ℕ0
1312, 3deccl 11456 . . 3 125 ∈ ℕ0
1413, 11deccl 11456 . 2 1251 ∈ ℕ0
15 0z 11332 . 2 0 ∈ ℤ
16 4nn0 11255 . . . . 5 4 ∈ ℕ0
1712, 16deccl 11456 . . . 4 124 ∈ ℕ0
18 8nn0 11259 . . . 4 8 ∈ ℕ0
1917, 18deccl 11456 . . 3 1248 ∈ ℕ0
20 1z 11351 . . 3 1 ∈ ℤ
21 3nn0 11254 . . . . 5 3 ∈ ℕ0
2221, 11deccl 11456 . . . 4 31 ∈ ℕ0
2322, 21deccl 11456 . . 3 313 ∈ ℕ0
24 6nn0 11257 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 11456 . . . . 5 62 ∈ ℕ0
2625, 16deccl 11456 . . . 4 624 ∈ ℕ0
27 9nn0 11260 . . . . . 6 9 ∈ ℕ0
282, 27deccl 11456 . . . . 5 29 ∈ ℕ0
2928nn0zi 11346 . . . 4 29 ∈ ℤ
30 7nn0 11258 . . . . . 6 7 ∈ ℕ0
312, 30deccl 11456 . . . . 5 27 ∈ ℕ0
3231, 5deccl 11456 . . . 4 270 ∈ ℕ0
3322, 2deccl 11456 . . . . 5 312 ∈ ℕ0
342, 21deccl 11456 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 11456 . . . . . 6 238 ∈ ℕ0
3635nn0zi 11346 . . . . 5 238 ∈ ℤ
3730, 30deccl 11456 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 11456 . . . . 5 772 ∈ ℕ0
3911, 3deccl 11456 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 11456 . . . . . 6 156 ∈ ℕ0
4121nn0zi 11346 . . . . . 6 3 ∈ ℤ
4227, 11deccl 11456 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 11456 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 11346 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 11456 . . . . . . . 8 19 ∈ ℕ0
46 4nn 11131 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 11462 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 11456 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 11456 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 11456 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 11346 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 11456 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 11456 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 11456 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 11456 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 11456 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 11456 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 11456 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 11456 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 11346 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 11456 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 11456 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 11456 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 11456 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 11456 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 15768 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 11102 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2621 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 11479 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2621 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2621 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 11248 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 10167 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2621 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 11248 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 10167 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 11035 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 9987 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 11077 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 6616 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 11095 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2643 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 11044 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 9987 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 6614 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 11099 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 11466 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2647 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 11512 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 9938 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 10170 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 6614 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 11046 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 10168 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2647 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 11512 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 11039 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 9987 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 6614 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 11097 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 11466 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2647 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 11512 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2621 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2621 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 6614 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2643 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 11598 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 11531 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 11123 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 24, 109, 110decmul1 11529 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 11121 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 16, 111, 112decmul1 11529 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2646 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 15698 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2621 . . . . . . . . . . 11 19 = 19
117 2t1e2 11120 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 6614 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2643 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 11052 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 11607 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 9991 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 11533 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2621 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 11456 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 11456 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2621 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2621 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2621 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2621 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 11078 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 11114 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 10172 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 11514 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 10168 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 11514 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 11248 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 10167 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 11456 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 11456 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2621 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 11466 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2621 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 11100 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 11248 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 10168 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 11479 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 11563 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 10172 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 11516 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2621 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 11101 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2621 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 11479 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 6615 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 11578 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 10168 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 11523 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2643 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 11050 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 11560 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 10172 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2643 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 11510 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 11479 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 11510 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 11466 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 11042 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 10168 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2643 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 11076 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 6615 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 11583 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 11479 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2643 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 11579 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 9991 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 11111 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 11523 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 11510 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 11601 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 10168 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 11523 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 11510 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 11512 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 11248 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 10170 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 6614 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2647 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 11512 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 11466 . . . . . . . . . . . . 13 7 = 07
19321dec0h 11466 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2643 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 6615 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 11479 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2643 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 11124 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 6614 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 11565 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2643 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 11510 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 11599 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 11048 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 11549 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 10172 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 11524 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 11510 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 11512 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2621 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 11456 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 11456 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 11456 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2621 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2621 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 11466 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2621 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2643 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 11440 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 10172 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 11519 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 10172 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 11514 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2621 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 11514 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 11514 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 11248 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 10167 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2643 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 11119 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 10155 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 6616 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2643 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 6614 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 11096 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2647 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 11510 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 9986 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2643 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 11510 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 6614 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 10172 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2647 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 11510 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 11466 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 11466 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2643 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 6614 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2643 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 11508 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 10167 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2647 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 11510 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 6614 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 10172 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2647 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 11510 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 11512 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2643 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 9987 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 6616 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2643 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 6614 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2647 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 11510 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 11590 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 11479 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 11510 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 6614 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 11546 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2643 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 11510 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 11512 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 11248 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 9986 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 11533 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2646 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 15697 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2621 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 11479 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2621 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2643 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 6616 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 10167 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2643 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 11512 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 6614 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2647 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 11512 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 11512 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 6614 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2647 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 11510 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 10169 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 6614 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2647 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 11510 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 11592 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 11531 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2646 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 15698 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2621 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 9991 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 6614 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2643 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 11533 . . . . . . . 8 (2 · 39) = 78
310 eqid 2621 . . . . . . . . . 10 2309 = 2309
311 eqid 2621 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 11523 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 11248 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 10167 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 11125 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 11088 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 6616 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 11558 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2643 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 11581 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 9991 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 11523 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 11512 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 10170 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 6614 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2647 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 11512 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 11576 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 11524 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 11512 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 11514 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 6614 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2647 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 11510 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 11510 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 11510 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 11512 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 11248 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 9986 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 11533 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2646 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 15697 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2621 . . . . . . . 8 78 = 78
344 4p1e5 11098 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 9991 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 11479 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 9991 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 11533 . . . . . . 7 (2 · 78) = 156
349 eqid 2621 . . . . . . . . 9 194 = 194
3502, 16deccl 11456 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2621 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 11479 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2621 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 11479 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 11514 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 11494 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 11566 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 11516 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2646 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2621 . . . . . . . . 9 91 = 91
361 eqid 2621 . . . . . . . . . . . 12 15 = 15
362204addid2i 10168 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2643 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 6616 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2643 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 11523 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 11510 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 6616 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 11109 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2643 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 11510 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 11512 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 11248 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 10170 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 6614 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2647 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 11512 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 6616 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2643 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 11510 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 11512 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 11456 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2621 . . . . . . . . . 10 77 = 77
38411, 30deccl 11456 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 11456 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2621 . . . . . . . . . . . 12 175 = 175
387384nn0cni 11248 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 10168 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 11479 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 11551 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 11516 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 6616 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2643 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 9986 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 6614 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 11570 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2643 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 11510 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 9986 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 6614 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 11106 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2647 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 11510 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 9987 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 10168 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 6616 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2643 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 11614 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 10172 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 11523 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 11510 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 11609 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 9991 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 11552 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 10172 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 11524 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 11510 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 11512 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 9987 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 6616 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 11107 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2643 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 11479 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 11510 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 11577 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 11531 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 11533 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2646 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 15699 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2621 . . . . . . 7 156 = 156
431117, 172oveq12i 6616 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2643 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 9991 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 11479 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 11512 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 11585 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 9991 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 11533 . . . . . 6 (2 · 156) = 312
439 eqid 2621 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 11479 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 10167 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2643 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 6616 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 11113 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2643 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 10172 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 11524 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 11512 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 10170 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 6614 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2647 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 11512 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 6614 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2643 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 11512 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 11479 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 6614 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 11571 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2643 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 11521 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 11248 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 9986 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 11533 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2646 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 15697 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2621 . . . . . 6 312 = 312
467 eqid 2621 . . . . . . . . 9 31 = 31
468306oveq1i 6614 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2643 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2643 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 11533 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 6614 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 11248 . . . . . . . 8 62 ∈ ℂ
474473addid1i 10167 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2643 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2643 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 11533 . . . . 5 (2 · 312) = 624
478 eqid 2621 . . . . . . 7 270 = 270
47930, 11deccl 11456 . . . . . . 7 71 ∈ ℕ0
480 eqid 2621 . . . . . . . . 9 71 = 71
481 7p2e9 11116 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 10172 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 11514 . . . . . . . 8 (27 + 71) = 98
484120addid1i 10167 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2643 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 11456 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2621 . . . . . . . . . 10 238 = 238
488486nn0cni 11248 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 10168 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 11523 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 6616 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2643 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 6614 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2647 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 11510 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 11568 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 10172 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 11524 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 11510 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 6615 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2643 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 11510 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 11510 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 11512 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 11248 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 10170 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 6614 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2647 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 11512 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 6616 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2643 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 11510 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 11531 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 6614 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 11456 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 11248 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 10167 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2643 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 11512 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 11456 . . . . . . 7 154 ∈ ℕ0
521 eqid 2621 . . . . . . . 8 154 = 154
5223, 16deccl 11456 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 11456 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 11456 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2621 . . . . . . . . . 10 540 = 540
526 eqid 2621 . . . . . . . . . . 11 54 = 54
52783addid2i 10168 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 11514 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 10167 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 11514 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2621 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 11479 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 11597 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 11540 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 11514 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 11524 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 11510 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 10172 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 11523 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 11510 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 6615 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 11567 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 11524 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2643 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 11494 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 11510 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 11108 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 11523 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 11510 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 11512 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 11479 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 11531 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 16, 552, 112decmul1 11529 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 11533 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2646 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 15697 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2621 . . . . 5 624 = 624
558 eqid 2621 . . . . . . . 8 62 = 62
559437oveq1i 6614 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 11248 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 10167 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2643 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 11533 . . . . . . 7 (2 · 62) = 124
564563oveq1i 6614 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 11248 . . . . . . 7 124 ∈ ℂ
566565addid1i 10167 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2643 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 9991 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2643 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 11533 . . . 4 (2 · 624) = 1248
571 eqid 2621 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 11525 . . . . . . 7 (31 + 9) = 40
573169addid1i 10167 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2643 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 11456 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2621 . . . . . . . . 9 29 = 29
577575nn0cni 11248 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 10168 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 6616 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2643 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 11524 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 11510 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 11523 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 11610 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 11523 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 11521 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 11512 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 10170 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 6614 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2647 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 11512 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 6616 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2643 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 11608 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 11547 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 11525 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 11510 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 11512 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 11456 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2621 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 10172 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 11524 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 11510 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 6614 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2647 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 11510 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 11531 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 10169 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 5, 607, 608decmul1 11529 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 11533 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 6614 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 11456 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 11456 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 11456 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 11248 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 10167 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2643 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 11248 . . . . . . . 8 270 ∈ ℂ
619618mul01i 10170 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2643 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 11533 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2646 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 15697 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 12903 . . . 4 (2↑3) = 8
625624oveq1i 6614 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2621 . . . 4 1248 = 1248
627 eqid 2621 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 11479 . . . 4 (124 + 1) = 125
629 8p3e11 11556 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 11524 . . 3 (1248 + 3) = 1251
6319nncni 10974 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 9987 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2643 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 11479 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 9991 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 11479 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 9987 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 6614 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 11554 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2643 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 11521 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 11531 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2646 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 15696 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2621 . . . 4 1251 = 1251
646 eqid 2621 . . . . . 6 125 = 125
647 eqid 2621 . . . . . . 7 12 = 12
648117, 232oveq12i 6616 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2643 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 6614 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 11466 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2647 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 11512 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 11533 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 11523 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 11533 . . 3 (2 · 1251) = 2502
6576, 2deccl 11456 . . . . 5 2502 ∈ ℕ0
658657nn0cni 11248 . . . 4 2502 ∈ ℂ
659 eqid 2621 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 11479 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2646 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 10242 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2646 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 10169 . . . 4 (0 · 𝑁) = 0
665664oveq1i 6614 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2646 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2646 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 15697 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6604  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  cmin 10210  cn 10964  2c2 11014  3c3 11015  4c4 11016  5c5 11017  6c6 11018  7c7 11019  8c8 11020  9c9 11021  cdc 11437   mod cmo 12608  cexp 12800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-sup 8292  df-inf 8293  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-rp 11777  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801
This theorem is referenced by:  2503prm  15771
  Copyright terms: Public domain W3C validator