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

Theorem 2503lem2 16243
Description: Lemma for 2503prm 16245. 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 11661 . . . . . 6 2 ∈ ℕ0
3 5nn0 11664 . . . . . 6 5 ∈ ℕ0
42, 3deccl 11860 . . . . 5 25 ∈ ℕ0
5 0nn0 11659 . . . . 5 0 ∈ ℕ0
64, 5deccl 11860 . . . 4 250 ∈ ℕ0
7 3nn 11454 . . . 4 3 ∈ ℕ
86, 7decnncl 11866 . . 3 2503 ∈ ℕ
91, 8eqeltri 2855 . 2 𝑁 ∈ ℕ
10 2nn 11448 . 2 2 ∈ ℕ
11 1nn0 11660 . . . . 5 1 ∈ ℕ0
1211, 2deccl 11860 . . . 4 12 ∈ ℕ0
1312, 3deccl 11860 . . 3 125 ∈ ℕ0
1413, 11deccl 11860 . 2 1251 ∈ ℕ0
15 0z 11739 . 2 0 ∈ ℤ
16 4nn0 11663 . . . . 5 4 ∈ ℕ0
1712, 16deccl 11860 . . . 4 124 ∈ ℕ0
18 8nn0 11667 . . . 4 8 ∈ ℕ0
1917, 18deccl 11860 . . 3 1248 ∈ ℕ0
20 1z 11759 . . 3 1 ∈ ℤ
21 3nn0 11662 . . . . 5 3 ∈ ℕ0
2221, 11deccl 11860 . . . 4 31 ∈ ℕ0
2322, 21deccl 11860 . . 3 313 ∈ ℕ0
24 6nn0 11665 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 11860 . . . . 5 62 ∈ ℕ0
2625, 16deccl 11860 . . . 4 624 ∈ ℕ0
27 9nn0 11668 . . . . . 6 9 ∈ ℕ0
282, 27deccl 11860 . . . . 5 29 ∈ ℕ0
2928nn0zi 11754 . . . 4 29 ∈ ℤ
30 7nn0 11666 . . . . . 6 7 ∈ ℕ0
312, 30deccl 11860 . . . . 5 27 ∈ ℕ0
3231, 5deccl 11860 . . . 4 270 ∈ ℕ0
3322, 2deccl 11860 . . . . 5 312 ∈ ℕ0
342, 21deccl 11860 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 11860 . . . . . 6 238 ∈ ℕ0
3635nn0zi 11754 . . . . 5 238 ∈ ℤ
3730, 30deccl 11860 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 11860 . . . . 5 772 ∈ ℕ0
3911, 3deccl 11860 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 11860 . . . . . 6 156 ∈ ℕ0
4121nn0zi 11754 . . . . . 6 3 ∈ ℤ
4227, 11deccl 11860 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 11860 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 11754 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 11860 . . . . . . . 8 19 ∈ ℕ0
46 4nn 11459 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 11866 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 11860 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 11860 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 11860 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 11754 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 11860 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 11860 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 11860 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 11860 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 11860 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 11860 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 11860 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 11860 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 11754 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 11860 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 11860 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 11860 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 11860 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 11860 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 16242 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 11532 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2778 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 11877 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2778 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2778 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 11655 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 10563 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2778 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 11655 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 10563 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 11450 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 10382 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 11506 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 6934 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 11524 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2802 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 11465 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 10382 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 6932 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 11529 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 11868 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2806 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 11899 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 10330 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 10566 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 6932 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 11469 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 10564 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2806 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 11899 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 11456 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 10382 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 6932 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 11527 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 11868 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2806 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 11899 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2778 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2778 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 6932 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2802 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 11962 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 11912 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 11548 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 11910 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 11546 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 11910 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2805 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 16178 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2778 . . . . . . . . . . 11 19 = 19
117 2t1e2 11545 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 6932 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2802 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 11481 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 11969 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 10386 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 11913 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2778 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 11860 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 11860 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2778 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2778 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2778 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2778 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 11507 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 11542 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 10568 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 11900 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 10564 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 11900 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 11655 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 10563 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 11860 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 11860 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2778 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 11868 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2778 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 11530 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 11655 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 10564 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 11877 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 11934 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 10568 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 11901 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2778 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 11531 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2778 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 11877 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 6933 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 11947 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 10564 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 11906 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2802 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 11477 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 11931 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 10568 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2802 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 11898 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 11877 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 11898 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 11868 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 11461 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 10564 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2802 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 11504 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 6933 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 11950 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 11877 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2802 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 11948 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 10386 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 11540 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 11906 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 11898 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 11965 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 10564 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 11906 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 11898 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 11899 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 11655 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 10566 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 6932 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2806 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 11899 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 11868 . . . . . . . . . . . . 13 7 = 07
19321dec0h 11868 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2802 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 6933 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 11877 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2802 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 11549 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 6932 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 11935 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2802 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 11898 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 11963 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 11473 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 11923 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 10568 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 11907 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 11898 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 11899 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2778 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 11860 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 11860 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 11860 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2778 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2778 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 11868 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2778 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2802 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 11847 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 10568 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 11902 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 10568 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 11900 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2778 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 11900 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 11900 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 11655 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 10563 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2802 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 11544 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 10551 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 6934 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2802 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 6932 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 11525 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2806 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 11898 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 10381 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2802 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 11898 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 6932 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 10568 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2806 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 11898 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 11868 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 11868 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2802 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 6932 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2802 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 11897 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 10563 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2806 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 11898 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 6932 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 10568 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2806 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 11898 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 11899 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2802 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 10382 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 6934 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2802 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 6932 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2806 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 11898 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 11955 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 11877 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 11898 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 6932 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 11921 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2802 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 11898 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 11899 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 11655 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 10381 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 11913 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2805 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 16177 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2778 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 11877 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2778 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2802 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 6934 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 10563 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2802 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 11899 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 6932 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2806 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 11899 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 11899 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 6932 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2806 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 11898 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 10565 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 6932 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2806 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 11898 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 11956 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 11912 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2805 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 16178 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2778 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 10386 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 6932 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2802 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 11913 . . . . . . . 8 (2 · 39) = 78
310 eqid 2778 . . . . . . . . . 10 2309 = 2309
311 eqid 2778 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 11906 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 11655 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 10563 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 11550 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 11517 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 6934 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 11929 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2802 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 11949 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 10386 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 11906 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 11899 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 10566 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 6932 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2806 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 11899 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 11945 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 11907 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 11899 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 11900 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 6932 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2806 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 11898 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 11898 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 11898 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 11899 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 11655 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 10381 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 11913 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2805 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 16177 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2778 . . . . . . . 8 78 = 78
344 4p1e5 11528 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 10386 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 11877 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 10386 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 11913 . . . . . . 7 (2 · 78) = 156
349 eqid 2778 . . . . . . . . 9 194 = 194
3502, 16deccl 11860 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2778 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 11877 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2778 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 11877 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 11900 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 11887 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 11936 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 11901 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2805 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2778 . . . . . . . . 9 91 = 91
361 eqid 2778 . . . . . . . . . . . 12 15 = 15
362204addid2i 10564 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2802 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 6934 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2802 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 11906 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 11898 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 6934 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 11538 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2802 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 11898 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 11899 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 11655 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 10566 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 6932 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2806 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 11899 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 6934 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2802 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 11898 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 11899 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 11860 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2778 . . . . . . . . . 10 77 = 77
38411, 30deccl 11860 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 11860 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2778 . . . . . . . . . . . 12 175 = 175
387384nn0cni 11655 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 10564 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 11877 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 11924 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 11901 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 6934 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2802 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 10381 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 6932 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 11940 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2802 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 11898 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 10381 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 6932 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 11535 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2806 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 11898 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 10382 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 10564 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 6934 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2802 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 11976 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 10568 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 11906 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 11898 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 11971 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 10386 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 11925 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 10568 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 11907 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 11898 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 11899 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 10382 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 6934 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 11536 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2802 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 11877 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 11898 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 11946 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 11912 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 11913 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2805 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 16179 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2778 . . . . . . 7 156 = 156
431117, 172oveq12i 6934 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2802 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 10386 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 11877 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 11899 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 11951 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 10386 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 11913 . . . . . 6 (2 · 156) = 312
439 eqid 2778 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 11877 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 10563 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2802 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 6934 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 11541 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2802 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 10568 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 11907 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 11899 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 10566 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 6932 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2806 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 11899 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 6932 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2802 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 11899 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 11877 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 6932 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 11941 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2802 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 11904 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 11655 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 10381 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 11913 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2805 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 16177 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2778 . . . . . 6 312 = 312
467 eqid 2778 . . . . . . . . 9 31 = 31
468306oveq1i 6932 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2802 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2802 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 11913 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 6932 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 11655 . . . . . . . 8 62 ∈ ℂ
474473addid1i 10563 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2802 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2802 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 11913 . . . . 5 (2 · 312) = 624
478 eqid 2778 . . . . . . 7 270 = 270
47930, 11deccl 11860 . . . . . . 7 71 ∈ ℕ0
480 eqid 2778 . . . . . . . . 9 71 = 71
481 7p2e9 11543 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 10568 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 11900 . . . . . . . 8 (27 + 71) = 98
484120addid1i 10563 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2802 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 11860 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2778 . . . . . . . . . 10 238 = 238
488486nn0cni 11655 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 10564 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 11906 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 6934 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2802 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 6932 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2806 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 11898 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 11938 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 10568 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 11907 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 11898 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 6933 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2802 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 11898 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 11898 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 11899 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 11655 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 10566 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 6932 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2806 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 11899 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 6934 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2802 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 11898 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 11912 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 6932 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 11860 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 11655 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 10563 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2802 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 11899 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 11860 . . . . . . 7 154 ∈ ℕ0
521 eqid 2778 . . . . . . . 8 154 = 154
5223, 16deccl 11860 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 11860 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 11860 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2778 . . . . . . . . . 10 540 = 540
526 eqid 2778 . . . . . . . . . . 11 54 = 54
52783addid2i 10564 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 11900 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 10563 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 11900 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2778 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 11877 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 11961 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 11918 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 11900 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 11907 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 11898 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 10568 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 11906 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 11898 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 6933 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 11937 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 11907 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2802 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 11887 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 11898 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 11537 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 11906 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 11898 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 11899 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 11877 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 11912 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 11910 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 11913 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2805 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 16177 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2778 . . . . 5 624 = 624
558 eqid 2778 . . . . . . . 8 62 = 62
559437oveq1i 6932 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 11655 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 10563 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2802 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 11913 . . . . . . 7 (2 · 62) = 124
564563oveq1i 6932 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 11655 . . . . . . 7 124 ∈ ℂ
566565addid1i 10563 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2802 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 10386 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2802 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 11913 . . . 4 (2 · 624) = 1248
571 eqid 2778 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 11908 . . . . . . 7 (31 + 9) = 40
573169addid1i 10563 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2802 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 11860 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2778 . . . . . . . . 9 29 = 29
577575nn0cni 11655 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 10564 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 6934 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2802 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 11907 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 11898 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 11906 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 11972 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 11906 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 11904 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 11899 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 10566 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 6932 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2806 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 11899 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 6934 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2802 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 11970 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 11922 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 11908 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 11898 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 11899 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 11860 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2778 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 10568 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 11907 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 11898 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 6932 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2806 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 11898 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 11912 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 10565 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 11910 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 11913 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 6932 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 11860 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 11860 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 11860 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 11655 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 10563 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2802 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 11655 . . . . . . . 8 270 ∈ ℂ
619618mul01i 10566 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2802 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 11913 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2805 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 16177 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 13282 . . . 4 (2↑3) = 8
625624oveq1i 6932 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2778 . . . 4 1248 = 1248
627 eqid 2778 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 11877 . . . 4 (124 + 1) = 125
629 8p3e11 11928 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 11907 . . 3 (1248 + 3) = 1251
6319nncni 11385 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 10382 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2802 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 11877 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 10386 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 11877 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 10382 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 6932 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 11927 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2802 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 11904 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 11912 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2805 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 16176 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2778 . . . 4 1251 = 1251
646 eqid 2778 . . . . . 6 125 = 125
647 eqid 2778 . . . . . . 7 12 = 12
648117, 232oveq12i 6934 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2802 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 6932 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 11868 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2806 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 11899 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 11913 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 11906 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 11913 . . 3 (2 · 1251) = 2502
6576, 2deccl 11860 . . . . 5 2502 ∈ ℕ0
658657nn0cni 11655 . . . 4 2502 ∈ ℂ
659 eqid 2778 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 11877 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2805 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 10640 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2805 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 10565 . . . 4 (0 · 𝑁) = 0
665664oveq1i 6932 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2805 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2805 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 16177 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1601  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  cmin 10606  cn 11374  2c2 11430  3c3 11431  4c4 11432  5c5 11433  6c6 11434  7c7 11435  8c8 11436  9c9 11437  cdc 11845   mod cmo 12987  cexp 13178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-sup 8636  df-inf 8637  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-rp 12138  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179
This theorem is referenced by:  2503prm  16245
  Copyright terms: Public domain W3C validator