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

Theorem 2503lem2 16463
Description: Lemma for 2503prm 16465. 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 11906 . . . . . 6 2 ∈ ℕ0
3 5nn0 11909 . . . . . 6 5 ∈ ℕ0
42, 3deccl 12105 . . . . 5 25 ∈ ℕ0
5 0nn0 11904 . . . . 5 0 ∈ ℕ0
64, 5deccl 12105 . . . 4 250 ∈ ℕ0
7 3nn 11708 . . . 4 3 ∈ ℕ
86, 7decnncl 12110 . . 3 2503 ∈ ℕ
91, 8eqeltri 2913 . 2 𝑁 ∈ ℕ
10 2nn 11702 . 2 2 ∈ ℕ
11 1nn0 11905 . . . . 5 1 ∈ ℕ0
1211, 2deccl 12105 . . . 4 12 ∈ ℕ0
1312, 3deccl 12105 . . 3 125 ∈ ℕ0
1413, 11deccl 12105 . 2 1251 ∈ ℕ0
15 0z 11984 . 2 0 ∈ ℤ
16 4nn0 11908 . . . . 5 4 ∈ ℕ0
1712, 16deccl 12105 . . . 4 124 ∈ ℕ0
18 8nn0 11912 . . . 4 8 ∈ ℕ0
1917, 18deccl 12105 . . 3 1248 ∈ ℕ0
20 1z 12004 . . 3 1 ∈ ℤ
21 3nn0 11907 . . . . 5 3 ∈ ℕ0
2221, 11deccl 12105 . . . 4 31 ∈ ℕ0
2322, 21deccl 12105 . . 3 313 ∈ ℕ0
24 6nn0 11910 . . . . . 6 6 ∈ ℕ0
2524, 2deccl 12105 . . . . 5 62 ∈ ℕ0
2625, 16deccl 12105 . . . 4 624 ∈ ℕ0
27 9nn0 11913 . . . . . 6 9 ∈ ℕ0
282, 27deccl 12105 . . . . 5 29 ∈ ℕ0
2928nn0zi 11999 . . . 4 29 ∈ ℤ
30 7nn0 11911 . . . . . 6 7 ∈ ℕ0
312, 30deccl 12105 . . . . 5 27 ∈ ℕ0
3231, 5deccl 12105 . . . 4 270 ∈ ℕ0
3322, 2deccl 12105 . . . . 5 312 ∈ ℕ0
342, 21deccl 12105 . . . . . . 7 23 ∈ ℕ0
3534, 18deccl 12105 . . . . . 6 238 ∈ ℕ0
3635nn0zi 11999 . . . . 5 238 ∈ ℤ
3730, 30deccl 12105 . . . . . 6 77 ∈ ℕ0
3837, 2deccl 12105 . . . . 5 772 ∈ ℕ0
3911, 3deccl 12105 . . . . . . 7 15 ∈ ℕ0
4039, 24deccl 12105 . . . . . 6 156 ∈ ℕ0
4121nn0zi 11999 . . . . . 6 3 ∈ ℤ
4227, 11deccl 12105 . . . . . 6 91 ∈ ℕ0
4330, 18deccl 12105 . . . . . . 7 78 ∈ ℕ0
4439nn0zi 11999 . . . . . . 7 15 ∈ ℤ
4511, 27deccl 12105 . . . . . . . 8 19 ∈ ℕ0
46 4nn 11712 . . . . . . . 8 4 ∈ ℕ
4745, 46decnncl 12110 . . . . . . 7 194 ∈ ℕ
4834, 5deccl 12105 . . . . . . . 8 230 ∈ ℕ0
4948, 27deccl 12105 . . . . . . 7 2309 ∈ ℕ0
5021, 27deccl 12105 . . . . . . . 8 39 ∈ ℕ0
5116nn0zi 11999 . . . . . . . 8 4 ∈ ℤ
5211, 11deccl 12105 . . . . . . . . 9 11 ∈ ℕ0
5352, 11deccl 12105 . . . . . . . 8 111 ∈ ℕ0
5421, 18deccl 12105 . . . . . . . . 9 38 ∈ ℕ0
5511, 21deccl 12105 . . . . . . . . . . 11 13 ∈ ℕ0
5655, 5deccl 12105 . . . . . . . . . 10 130 ∈ ℕ0
5756, 30deccl 12105 . . . . . . . . 9 1307 ∈ ℕ0
583, 21deccl 12105 . . . . . . . . . . . 12 53 ∈ ℕ0
5958, 18deccl 12105 . . . . . . . . . . 11 538 ∈ ℕ0
6059nn0zi 11999 . . . . . . . . . 10 538 ∈ ℤ
6152, 24deccl 12105 . . . . . . . . . . 11 116 ∈ ℕ0
6261, 11deccl 12105 . . . . . . . . . 10 1161 ∈ ℕ0
6311, 18deccl 12105 . . . . . . . . . . 11 18 ∈ ℕ0
6463, 21deccl 12105 . . . . . . . . . . . 12 183 ∈ ℕ0
6564, 2deccl 12105 . . . . . . . . . . 11 1832 ∈ ℕ0
6612503lem1 16462 . . . . . . . . . . 11 ((2↑18) mod 𝑁) = (1832 mod 𝑁)
67 8p1e9 11779 . . . . . . . . . . . 12 (8 + 1) = 9
68 eqid 2825 . . . . . . . . . . . 12 18 = 18
6911, 18, 67, 68decsuc 12121 . . . . . . . . . . 11 (18 + 1) = 19
70 eqid 2825 . . . . . . . . . . . . 13 1161 = 1161
71 eqid 2825 . . . . . . . . . . . . . 14 250 = 250
7261nn0cni 11901 . . . . . . . . . . . . . . 15 116 ∈ ℂ
7372addid1i 10819 . . . . . . . . . . . . . 14 (116 + 0) = 116
74 eqid 2825 . . . . . . . . . . . . . . 15 25 = 25
7552nn0cni 11901 . . . . . . . . . . . . . . . 16 11 ∈ ℂ
7675addid1i 10819 . . . . . . . . . . . . . . 15 (11 + 0) = 11
77 2cn 11704 . . . . . . . . . . . . . . . . . 18 2 ∈ ℂ
7877mulid2i 10638 . . . . . . . . . . . . . . . . 17 (1 · 2) = 2
79 1p0e1 11753 . . . . . . . . . . . . . . . . 17 (1 + 0) = 1
8078, 79oveq12i 7163 . . . . . . . . . . . . . . . 16 ((1 · 2) + (1 + 0)) = (2 + 1)
81 2p1e3 11771 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
8280, 81eqtri 2848 . . . . . . . . . . . . . . 15 ((1 · 2) + (1 + 0)) = 3
83 5cn 11717 . . . . . . . . . . . . . . . . . 18 5 ∈ ℂ
8483mulid2i 10638 . . . . . . . . . . . . . . . . 17 (1 · 5) = 5
8584oveq1i 7161 . . . . . . . . . . . . . . . 16 ((1 · 5) + 1) = (5 + 1)
86 5p1e6 11776 . . . . . . . . . . . . . . . 16 (5 + 1) = 6
8724dec0h 12112 . . . . . . . . . . . . . . . 16 6 = 06
8885, 86, 873eqtri 2852 . . . . . . . . . . . . . . 15 ((1 · 5) + 1) = 06
892, 3, 11, 11, 74, 76, 11, 24, 5, 82, 88decma2c 12143 . . . . . . . . . . . . . 14 ((1 · 25) + (11 + 0)) = 36
90 ax-1cn 10587 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
9190mul01i 10822 . . . . . . . . . . . . . . . 16 (1 · 0) = 0
9291oveq1i 7161 . . . . . . . . . . . . . . 15 ((1 · 0) + 6) = (0 + 6)
93 6cn 11720 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
9493addid2i 10820 . . . . . . . . . . . . . . 15 (0 + 6) = 6
9592, 94, 873eqtri 2852 . . . . . . . . . . . . . 14 ((1 · 0) + 6) = 06
964, 5, 52, 24, 71, 73, 11, 24, 5, 89, 95decma2c 12143 . . . . . . . . . . . . 13 ((1 · 250) + (116 + 0)) = 366
97 3cn 11710 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
9897mulid2i 10638 . . . . . . . . . . . . . . 15 (1 · 3) = 3
9998oveq1i 7161 . . . . . . . . . . . . . 14 ((1 · 3) + 1) = (3 + 1)
100 3p1e4 11774 . . . . . . . . . . . . . 14 (3 + 1) = 4
10116dec0h 12112 . . . . . . . . . . . . . 14 4 = 04
10299, 100, 1013eqtri 2852 . . . . . . . . . . . . 13 ((1 · 3) + 1) = 04
1036, 21, 61, 11, 1, 70, 11, 16, 5, 96, 102decma2c 12143 . . . . . . . . . . . 12 ((1 · 𝑁) + 1161) = 3664
104 eqid 2825 . . . . . . . . . . . . 13 1832 = 1832
105 eqid 2825 . . . . . . . . . . . . . 14 183 = 183
10678oveq1i 7161 . . . . . . . . . . . . . . . 16 ((1 · 2) + 1) = (2 + 1)
107106, 81eqtri 2848 . . . . . . . . . . . . . . 15 ((1 · 2) + 1) = 3
108 8t2e16 12205 . . . . . . . . . . . . . . 15 (8 · 2) = 16
1092, 11, 18, 68, 24, 11, 107, 108decmul1c 12155 . . . . . . . . . . . . . 14 (18 · 2) = 36
110 3t2e6 11795 . . . . . . . . . . . . . 14 (3 · 2) = 6
1112, 63, 21, 105, 109, 110decmul1 12154 . . . . . . . . . . . . 13 (183 · 2) = 366
112 2t2e4 11793 . . . . . . . . . . . . 13 (2 · 2) = 4
1132, 64, 2, 104, 111, 112decmul1 12154 . . . . . . . . . . . 12 (1832 · 2) = 3664
114103, 113eqtr4i 2851 . . . . . . . . . . 11 ((1 · 𝑁) + 1161) = (1832 · 2)
1159, 10, 63, 20, 65, 62, 66, 69, 114modxp1i 16398 . . . . . . . . . 10 ((2↑19) mod 𝑁) = (1161 mod 𝑁)
116 eqid 2825 . . . . . . . . . . 11 19 = 19
117 2t1e2 11792 . . . . . . . . . . . . 13 (2 · 1) = 2
118117oveq1i 7161 . . . . . . . . . . . 12 ((2 · 1) + 1) = (2 + 1)
119118, 81eqtri 2848 . . . . . . . . . . 11 ((2 · 1) + 1) = 3
120 9cn 11729 . . . . . . . . . . . 12 9 ∈ ℂ
121 9t2e18 12212 . . . . . . . . . . . 12 (9 · 2) = 18
122120, 77, 121mulcomli 10642 . . . . . . . . . . 11 (2 · 9) = 18
1232, 11, 27, 116, 18, 11, 119, 122decmul2c 12156 . . . . . . . . . 10 (2 · 19) = 38
124 eqid 2825 . . . . . . . . . . . 12 1307 = 1307
12511, 24deccl 12105 . . . . . . . . . . . . 13 16 ∈ ℕ0
126125, 2deccl 12105 . . . . . . . . . . . 12 162 ∈ ℕ0
127 eqid 2825 . . . . . . . . . . . . . 14 130 = 130
128 eqid 2825 . . . . . . . . . . . . . 14 162 = 162
129 eqid 2825 . . . . . . . . . . . . . . 15 13 = 13
130 eqid 2825 . . . . . . . . . . . . . . 15 16 = 16
131 1p1e2 11754 . . . . . . . . . . . . . . 15 (1 + 1) = 2
132 6p3e9 11789 . . . . . . . . . . . . . . . 16 (6 + 3) = 9
13393, 97, 132addcomli 10824 . . . . . . . . . . . . . . 15 (3 + 6) = 9
13411, 21, 11, 24, 129, 130, 131, 133decadd 12144 . . . . . . . . . . . . . 14 (13 + 16) = 29
13577addid2i 10820 . . . . . . . . . . . . . 14 (0 + 2) = 2
13655, 5, 125, 2, 127, 128, 134, 135decadd 12144 . . . . . . . . . . . . 13 (130 + 162) = 292
13728nn0cni 11901 . . . . . . . . . . . . . . 15 29 ∈ ℂ
138137addid1i 10819 . . . . . . . . . . . . . 14 (29 + 0) = 29
1392, 24deccl 12105 . . . . . . . . . . . . . . 15 26 ∈ ℕ0
140139, 27deccl 12105 . . . . . . . . . . . . . 14 269 ∈ ℕ0
141 eqid 2825 . . . . . . . . . . . . . . 15 538 = 538
1422dec0h 12112 . . . . . . . . . . . . . . . 16 2 = 02
143 eqid 2825 . . . . . . . . . . . . . . . 16 269 = 269
144 6p1e7 11777 . . . . . . . . . . . . . . . . 17 (6 + 1) = 7
145139nn0cni 11901 . . . . . . . . . . . . . . . . . 18 26 ∈ ℂ
146145addid2i 10820 . . . . . . . . . . . . . . . . 17 (0 + 26) = 26
1472, 24, 144, 146decsuc 12121 . . . . . . . . . . . . . . . 16 ((0 + 26) + 1) = 27
148 9p2e11 12177 . . . . . . . . . . . . . . . . 17 (9 + 2) = 11
149120, 77, 148addcomli 10824 . . . . . . . . . . . . . . . 16 (2 + 9) = 11
1505, 2, 139, 27, 142, 143, 147, 11, 149decaddc 12145 . . . . . . . . . . . . . . 15 (2 + 269) = 271
151 eqid 2825 . . . . . . . . . . . . . . . 16 53 = 53
152 7p1e8 11778 . . . . . . . . . . . . . . . . 17 (7 + 1) = 8
153 eqid 2825 . . . . . . . . . . . . . . . . 17 27 = 27
1542, 30, 152, 153decsuc 12121 . . . . . . . . . . . . . . . 16 (27 + 1) = 28
15581oveq2i 7162 . . . . . . . . . . . . . . . . 17 ((5 · 2) + (2 + 1)) = ((5 · 2) + 3)
156 5t2e10 12190 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
15797addid2i 10820 . . . . . . . . . . . . . . . . . 18 (0 + 3) = 3
15811, 5, 21, 156, 157decaddi 12150 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 3) = 13
159155, 158eqtri 2848 . . . . . . . . . . . . . . . 16 ((5 · 2) + (2 + 1)) = 13
160110oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((3 · 2) + 8) = (6 + 8)
161 8cn 11726 . . . . . . . . . . . . . . . . . 18 8 ∈ ℂ
162 8p6e14 12174 . . . . . . . . . . . . . . . . . 18 (8 + 6) = 14
163161, 93, 162addcomli 10824 . . . . . . . . . . . . . . . . 17 (6 + 8) = 14
164160, 163eqtri 2848 . . . . . . . . . . . . . . . 16 ((3 · 2) + 8) = 14
1653, 21, 2, 18, 151, 154, 2, 16, 11, 159, 164decmac 12142 . . . . . . . . . . . . . . 15 ((53 · 2) + (27 + 1)) = 134
16611, 24, 144, 108decsuc 12121 . . . . . . . . . . . . . . 15 ((8 · 2) + 1) = 17
16758, 18, 31, 11, 141, 150, 2, 30, 11, 165, 166decmac 12142 . . . . . . . . . . . . . 14 ((538 · 2) + (2 + 269)) = 1347
16827dec0h 12112 . . . . . . . . . . . . . . 15 9 = 09
169 4cn 11714 . . . . . . . . . . . . . . . . . 18 4 ∈ ℂ
170169addid2i 10820 . . . . . . . . . . . . . . . . 17 (0 + 4) = 4
171170, 101eqtri 2848 . . . . . . . . . . . . . . . 16 (0 + 4) = 04
172 0p1e1 11751 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
173172oveq2i 7162 . . . . . . . . . . . . . . . . 17 ((5 · 5) + (0 + 1)) = ((5 · 5) + 1)
174 5t5e25 12193 . . . . . . . . . . . . . . . . . 18 (5 · 5) = 25
1752, 3, 86, 174decsuc 12121 . . . . . . . . . . . . . . . . 17 ((5 · 5) + 1) = 26
176173, 175eqtri 2848 . . . . . . . . . . . . . . . 16 ((5 · 5) + (0 + 1)) = 26
177 5t3e15 12191 . . . . . . . . . . . . . . . . . 18 (5 · 3) = 15
17883, 97, 177mulcomli 10642 . . . . . . . . . . . . . . . . 17 (3 · 5) = 15
179 5p4e9 11787 . . . . . . . . . . . . . . . . 17 (5 + 4) = 9
18011, 3, 16, 178, 179decaddi 12150 . . . . . . . . . . . . . . . 16 ((3 · 5) + 4) = 19
1813, 21, 5, 16, 151, 171, 3, 27, 11, 176, 180decmac 12142 . . . . . . . . . . . . . . 15 ((53 · 5) + (0 + 4)) = 269
182 8t5e40 12208 . . . . . . . . . . . . . . . 16 (8 · 5) = 40
183120addid2i 10820 . . . . . . . . . . . . . . . 16 (0 + 9) = 9
18416, 5, 27, 182, 183decaddi 12150 . . . . . . . . . . . . . . 15 ((8 · 5) + 9) = 49
18558, 18, 5, 27, 141, 168, 3, 27, 16, 181, 184decmac 12142 . . . . . . . . . . . . . 14 ((538 · 5) + 9) = 2699
1862, 3, 2, 27, 74, 138, 59, 27, 140, 167, 185decma2c 12143 . . . . . . . . . . . . 13 ((538 · 25) + (29 + 0)) = 13479
18759nn0cni 11901 . . . . . . . . . . . . . . . 16 538 ∈ ℂ
188187mul01i 10822 . . . . . . . . . . . . . . 15 (538 · 0) = 0
189188oveq1i 7161 . . . . . . . . . . . . . 14 ((538 · 0) + 2) = (0 + 2)
190189, 135, 1423eqtri 2852 . . . . . . . . . . . . 13 ((538 · 0) + 2) = 02
1914, 5, 28, 2, 71, 136, 59, 2, 5, 186, 190decma2c 12143 . . . . . . . . . . . 12 ((538 · 250) + (130 + 162)) = 134792
19230dec0h 12112 . . . . . . . . . . . . 13 7 = 07
19321dec0h 12112 . . . . . . . . . . . . . . 15 3 = 03
194157, 193eqtri 2848 . . . . . . . . . . . . . 14 (0 + 3) = 03
195172oveq2i 7162 . . . . . . . . . . . . . . 15 ((5 · 3) + (0 + 1)) = ((5 · 3) + 1)
19611, 3, 86, 177decsuc 12121 . . . . . . . . . . . . . . 15 ((5 · 3) + 1) = 16
197195, 196eqtri 2848 . . . . . . . . . . . . . 14 ((5 · 3) + (0 + 1)) = 16
198 3t3e9 11796 . . . . . . . . . . . . . . . 16 (3 · 3) = 9
199198oveq1i 7161 . . . . . . . . . . . . . . 15 ((3 · 3) + 3) = (9 + 3)
200 9p3e12 12178 . . . . . . . . . . . . . . 15 (9 + 3) = 12
201199, 200eqtri 2848 . . . . . . . . . . . . . 14 ((3 · 3) + 3) = 12
2023, 21, 5, 21, 151, 194, 21, 2, 11, 197, 201decmac 12142 . . . . . . . . . . . . 13 ((53 · 3) + (0 + 3)) = 162
203 8t3e24 12206 . . . . . . . . . . . . . 14 (8 · 3) = 24
204 7cn 11723 . . . . . . . . . . . . . . 15 7 ∈ ℂ
205 7p4e11 12166 . . . . . . . . . . . . . . 15 (7 + 4) = 11
206204, 169, 205addcomli 10824 . . . . . . . . . . . . . 14 (4 + 7) = 11
2072, 16, 30, 203, 81, 11, 206decaddci 12151 . . . . . . . . . . . . 13 ((8 · 3) + 7) = 31
20858, 18, 5, 30, 141, 192, 21, 11, 21, 202, 207decmac 12142 . . . . . . . . . . . 12 ((538 · 3) + 7) = 1621
2096, 21, 56, 30, 1, 124, 59, 11, 126, 191, 208decma2c 12143 . . . . . . . . . . 11 ((538 · 𝑁) + 1307) = 1347921
210 eqid 2825 . . . . . . . . . . . . 13 116 = 116
21124, 27deccl 12105 . . . . . . . . . . . . . 14 69 ∈ ℕ0
212211, 30deccl 12105 . . . . . . . . . . . . 13 697 ∈ ℕ0
21330, 5deccl 12105 . . . . . . . . . . . . . 14 70 ∈ ℕ0
214 eqid 2825 . . . . . . . . . . . . . 14 11 = 11
215 eqid 2825 . . . . . . . . . . . . . . 15 697 = 697
21611dec0h 12112 . . . . . . . . . . . . . . . 16 1 = 01
217 eqid 2825 . . . . . . . . . . . . . . . 16 69 = 69
21894oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((0 + 6) + 1) = (6 + 1)
219218, 144eqtri 2848 . . . . . . . . . . . . . . . 16 ((0 + 6) + 1) = 7
220 9p1e10 12092 . . . . . . . . . . . . . . . . 17 (9 + 1) = 10
221120, 90, 220addcomli 10824 . . . . . . . . . . . . . . . 16 (1 + 9) = 10
2225, 11, 24, 27, 216, 217, 219, 221decaddc2 12146 . . . . . . . . . . . . . . 15 (1 + 69) = 70
223204, 90, 152addcomli 10824 . . . . . . . . . . . . . . 15 (1 + 7) = 8
22411, 11, 211, 30, 214, 215, 222, 223decadd 12144 . . . . . . . . . . . . . 14 (11 + 697) = 708
225 eqid 2825 . . . . . . . . . . . . . . . 16 70 = 70
2265, 30, 11, 11, 192, 214, 172, 152decadd 12144 . . . . . . . . . . . . . . . 16 (7 + 11) = 18
22730, 5, 52, 24, 225, 210, 226, 94decadd 12144 . . . . . . . . . . . . . . 15 (70 + 116) = 186
22863nn0cni 11901 . . . . . . . . . . . . . . . . 17 18 ∈ ℂ
229228addid1i 10819 . . . . . . . . . . . . . . . 16 (18 + 0) = 18
230131, 142eqtri 2848 . . . . . . . . . . . . . . . . 17 (1 + 1) = 02
231 1t1e1 11791 . . . . . . . . . . . . . . . . . . 19 (1 · 1) = 1
232 00id 10807 . . . . . . . . . . . . . . . . . . 19 (0 + 0) = 0
233231, 232oveq12i 7163 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + (0 + 0)) = (1 + 0)
234233, 79eqtri 2848 . . . . . . . . . . . . . . . . 17 ((1 · 1) + (0 + 0)) = 1
235231oveq1i 7161 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 2) = (1 + 2)
236 1p2e3 11772 . . . . . . . . . . . . . . . . . 18 (1 + 2) = 3
237235, 236, 1933eqtri 2852 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 2) = 03
23811, 11, 5, 2, 214, 230, 11, 21, 5, 234, 237decmac 12142 . . . . . . . . . . . . . . . 16 ((11 · 1) + (1 + 1)) = 13
23993mulid1i 10637 . . . . . . . . . . . . . . . . . 18 (6 · 1) = 6
240239oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 8) = (6 + 8)
241240, 163eqtri 2848 . . . . . . . . . . . . . . . 16 ((6 · 1) + 8) = 14
24252, 24, 11, 18, 210, 229, 11, 16, 11, 238, 241decmac 12142 . . . . . . . . . . . . . . 15 ((116 · 1) + (18 + 0)) = 134
243231oveq1i 7161 . . . . . . . . . . . . . . . 16 ((1 · 1) + 6) = (1 + 6)
24493, 90, 144addcomli 10824 . . . . . . . . . . . . . . . 16 (1 + 6) = 7
245243, 244, 1923eqtri 2852 . . . . . . . . . . . . . . 15 ((1 · 1) + 6) = 07
24661, 11, 63, 24, 70, 227, 11, 30, 5, 242, 245decmac 12142 . . . . . . . . . . . . . 14 ((1161 · 1) + (70 + 116)) = 1347
24718dec0h 12112 . . . . . . . . . . . . . . 15 8 = 08
2485dec0h 12112 . . . . . . . . . . . . . . . . 17 0 = 00
249232, 248eqtri 2848 . . . . . . . . . . . . . . . 16 (0 + 0) = 00
250231oveq1i 7161 . . . . . . . . . . . . . . . . . 18 ((1 · 1) + 0) = (1 + 0)
251250, 79eqtri 2848 . . . . . . . . . . . . . . . . 17 ((1 · 1) + 0) = 1
25211, 11, 5, 5, 214, 249, 11, 251, 251decma 12141 . . . . . . . . . . . . . . . 16 ((11 · 1) + (0 + 0)) = 11
253239oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((6 · 1) + 0) = (6 + 0)
25493addid1i 10819 . . . . . . . . . . . . . . . . 17 (6 + 0) = 6
255253, 254, 873eqtri 2852 . . . . . . . . . . . . . . . 16 ((6 · 1) + 0) = 06
25652, 24, 5, 5, 210, 249, 11, 24, 5, 252, 255decmac 12142 . . . . . . . . . . . . . . 15 ((116 · 1) + (0 + 0)) = 116
257231oveq1i 7161 . . . . . . . . . . . . . . . 16 ((1 · 1) + 8) = (1 + 8)
258161, 90, 67addcomli 10824 . . . . . . . . . . . . . . . 16 (1 + 8) = 9
259257, 258, 1683eqtri 2852 . . . . . . . . . . . . . . 15 ((1 · 1) + 8) = 09
26061, 11, 5, 18, 70, 247, 11, 27, 5, 256, 259decmac 12142 . . . . . . . . . . . . . 14 ((1161 · 1) + 8) = 1169
26111, 11, 213, 18, 214, 224, 62, 27, 61, 246, 260decma2c 12143 . . . . . . . . . . . . 13 ((1161 · 11) + (11 + 697)) = 13479
262172, 216eqtri 2848 . . . . . . . . . . . . . . 15 (0 + 1) = 01
26393mulid2i 10638 . . . . . . . . . . . . . . . . . 18 (1 · 6) = 6
264263, 232oveq12i 7163 . . . . . . . . . . . . . . . . 17 ((1 · 6) + (0 + 0)) = (6 + 0)
265264, 254eqtri 2848 . . . . . . . . . . . . . . . 16 ((1 · 6) + (0 + 0)) = 6
266263oveq1i 7161 . . . . . . . . . . . . . . . . 17 ((1 · 6) + 3) = (6 + 3)
267266, 132, 1683eqtri 2852 . . . . . . . . . . . . . . . 16 ((1 · 6) + 3) = 09
26811, 11, 5, 21, 214, 194, 24, 27, 5, 265, 267decmac 12142 . . . . . . . . . . . . . . 15 ((11 · 6) + (0 + 3)) = 69
269 6t6e36 12198 . . . . . . . . . . . . . . . 16 (6 · 6) = 36
27021, 24, 144, 269decsuc 12121 . . . . . . . . . . . . . . 15 ((6 · 6) + 1) = 37
27152, 24, 5, 11, 210, 262, 24, 30, 21, 268, 270decmac 12142 . . . . . . . . . . . . . 14 ((116 · 6) + (0 + 1)) = 697
272263oveq1i 7161 . . . . . . . . . . . . . . 15 ((1 · 6) + 6) = (6 + 6)
273 6p6e12 12164 . . . . . . . . . . . . . . 15 (6 + 6) = 12
274272, 273eqtri 2848 . . . . . . . . . . . . . 14 ((1 · 6) + 6) = 12
27561, 11, 5, 24, 70, 87, 24, 2, 11, 271, 274decmac 12142 . . . . . . . . . . . . 13 ((1161 · 6) + 6) = 6972
27652, 24, 52, 24, 210, 210, 62, 2, 212, 261, 275decma2c 12143 . . . . . . . . . . . 12 ((1161 · 116) + 116) = 134792
27762nn0cni 11901 . . . . . . . . . . . . 13 1161 ∈ ℂ
278277mulid1i 10637 . . . . . . . . . . . 12 (1161 · 1) = 1161
27962, 61, 11, 70, 11, 61, 276, 278decmul2c 12156 . . . . . . . . . . 11 (1161 · 1161) = 1347921
280209, 279eqtr4i 2851 . . . . . . . . . 10 ((538 · 𝑁) + 1307) = (1161 · 1161)
2819, 10, 45, 60, 62, 57, 115, 123, 280mod2xi 16397 . . . . . . . . 9 ((2↑38) mod 𝑁) = (1307 mod 𝑁)
282 eqid 2825 . . . . . . . . . 10 38 = 38
28321, 18, 67, 282decsuc 12121 . . . . . . . . 9 (38 + 1) = 39
284 eqid 2825 . . . . . . . . . . 11 111 = 111
28579, 216eqtri 2848 . . . . . . . . . . . . 13 (1 + 0) = 01
28678, 232oveq12i 7163 . . . . . . . . . . . . . 14 ((1 · 2) + (0 + 0)) = (2 + 0)
28777addid1i 10819 . . . . . . . . . . . . . 14 (2 + 0) = 2
288286, 287eqtri 2848 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 0)) = 2
2892, 3, 5, 11, 74, 285, 11, 24, 5, 288, 88decma2c 12143 . . . . . . . . . . . 12 ((1 · 25) + (1 + 0)) = 26
29091oveq1i 7161 . . . . . . . . . . . . 13 ((1 · 0) + 1) = (0 + 1)
291290, 172, 2163eqtri 2852 . . . . . . . . . . . 12 ((1 · 0) + 1) = 01
2924, 5, 11, 11, 71, 76, 11, 11, 5, 289, 291decma2c 12143 . . . . . . . . . . 11 ((1 · 250) + (11 + 0)) = 261
2936, 21, 52, 11, 1, 284, 11, 16, 5, 292, 102decma2c 12143 . . . . . . . . . 10 ((1 · 𝑁) + 111) = 2614
294110oveq1i 7161 . . . . . . . . . . . . . 14 ((3 · 2) + 0) = (6 + 0)
295294, 254, 873eqtri 2852 . . . . . . . . . . . . 13 ((3 · 2) + 0) = 06
29611, 21, 5, 5, 129, 249, 2, 24, 5, 288, 295decmac 12142 . . . . . . . . . . . 12 ((13 · 2) + (0 + 0)) = 26
29777mul02i 10821 . . . . . . . . . . . . . 14 (0 · 2) = 0
298297oveq1i 7161 . . . . . . . . . . . . 13 ((0 · 2) + 1) = (0 + 1)
299298, 172, 2163eqtri 2852 . . . . . . . . . . . 12 ((0 · 2) + 1) = 01
30055, 5, 5, 11, 127, 216, 2, 11, 5, 296, 299decmac 12142 . . . . . . . . . . 11 ((130 · 2) + 1) = 261
301 7t2e14 12199 . . . . . . . . . . 11 (7 · 2) = 14
3022, 56, 30, 124, 16, 11, 300, 301decmul1c 12155 . . . . . . . . . 10 (1307 · 2) = 2614
303293, 302eqtr4i 2851 . . . . . . . . 9 ((1 · 𝑁) + 111) = (1307 · 2)
3049, 10, 54, 20, 57, 53, 281, 283, 303modxp1i 16398 . . . . . . . 8 ((2↑39) mod 𝑁) = (111 mod 𝑁)
305 eqid 2825 . . . . . . . . 9 39 = 39
30697, 77, 110mulcomli 10642 . . . . . . . . . . 11 (2 · 3) = 6
307306oveq1i 7161 . . . . . . . . . 10 ((2 · 3) + 1) = (6 + 1)
308307, 144eqtri 2848 . . . . . . . . 9 ((2 · 3) + 1) = 7
3092, 21, 27, 305, 18, 11, 308, 122decmul2c 12156 . . . . . . . 8 (2 · 39) = 78
310 eqid 2825 . . . . . . . . . 10 2309 = 2309
311 eqid 2825 . . . . . . . . . . . 12 230 = 230
31234, 5, 2, 311, 135decaddi 12150 . . . . . . . . . . 11 (230 + 2) = 232
31334nn0cni 11901 . . . . . . . . . . . . 13 23 ∈ ℂ
314313addid1i 10819 . . . . . . . . . . . 12 (23 + 0) = 23
315 4t2e8 11797 . . . . . . . . . . . . . 14 (4 · 2) = 8
316 2p2e4 11764 . . . . . . . . . . . . . 14 (2 + 2) = 4
317315, 316oveq12i 7163 . . . . . . . . . . . . 13 ((4 · 2) + (2 + 2)) = (8 + 4)
318 8p4e12 12172 . . . . . . . . . . . . 13 (8 + 4) = 12
319317, 318eqtri 2848 . . . . . . . . . . . 12 ((4 · 2) + (2 + 2)) = 12
320 5t4e20 12192 . . . . . . . . . . . . . 14 (5 · 4) = 20
32183, 169, 320mulcomli 10642 . . . . . . . . . . . . 13 (4 · 5) = 20
3222, 5, 21, 321, 157decaddi 12150 . . . . . . . . . . . 12 ((4 · 5) + 3) = 23
3232, 3, 2, 21, 74, 314, 16, 21, 2, 319, 322decma2c 12143 . . . . . . . . . . 11 ((4 · 25) + (23 + 0)) = 123
324169mul01i 10822 . . . . . . . . . . . . 13 (4 · 0) = 0
325324oveq1i 7161 . . . . . . . . . . . 12 ((4 · 0) + 2) = (0 + 2)
326325, 135, 1423eqtri 2852 . . . . . . . . . . 11 ((4 · 0) + 2) = 02
3274, 5, 34, 2, 71, 312, 16, 2, 5, 323, 326decma2c 12143 . . . . . . . . . 10 ((4 · 250) + (230 + 2)) = 1232
328 4t3e12 12188 . . . . . . . . . . 11 (4 · 3) = 12
32911, 2, 27, 328, 131, 11, 149decaddci 12151 . . . . . . . . . 10 ((4 · 3) + 9) = 21
3306, 21, 48, 27, 1, 310, 16, 11, 2, 327, 329decma2c 12143 . . . . . . . . 9 ((4 · 𝑁) + 2309) = 12321
3315, 11, 11, 11, 216, 214, 172, 131decadd 12144 . . . . . . . . . . . 12 (1 + 11) = 12
332231oveq1i 7161 . . . . . . . . . . . . . 14 ((1 · 1) + 1) = (1 + 1)
333332, 131, 1423eqtri 2852 . . . . . . . . . . . . 13 ((1 · 1) + 1) = 02
33411, 11, 5, 11, 214, 285, 11, 2, 5, 234, 333decmac 12142 . . . . . . . . . . . 12 ((11 · 1) + (1 + 0)) = 12
33552, 11, 11, 2, 284, 331, 11, 21, 5, 334, 237decmac 12142 . . . . . . . . . . 11 ((111 · 1) + (1 + 11)) = 123
33652, 11, 5, 11, 284, 216, 11, 2, 5, 252, 333decmac 12142 . . . . . . . . . . 11 ((111 · 1) + 1) = 112
33711, 11, 11, 11, 214, 214, 53, 2, 52, 335, 336decma2c 12143 . . . . . . . . . 10 ((111 · 11) + 11) = 1232
33853nn0cni 11901 . . . . . . . . . . 11 111 ∈ ℂ
339338mulid1i 10637 . . . . . . . . . 10 (111 · 1) = 111
34053, 52, 11, 284, 11, 52, 337, 339decmul2c 12156 . . . . . . . . 9 (111 · 111) = 12321
341330, 340eqtr4i 2851 . . . . . . . 8 ((4 · 𝑁) + 2309) = (111 · 111)
3429, 10, 50, 51, 53, 49, 304, 309, 341mod2xi 16397 . . . . . . 7 ((2↑78) mod 𝑁) = (2309 mod 𝑁)
343 eqid 2825 . . . . . . . 8 78 = 78
344 4p1e5 11775 . . . . . . . . 9 (4 + 1) = 5
345204, 77, 301mulcomli 10642 . . . . . . . . 9 (2 · 7) = 14
34611, 16, 344, 345decsuc 12121 . . . . . . . 8 ((2 · 7) + 1) = 15
347161, 77, 108mulcomli 10642 . . . . . . . 8 (2 · 8) = 16
3482, 30, 18, 343, 24, 11, 346, 347decmul2c 12156 . . . . . . 7 (2 · 78) = 156
349 eqid 2825 . . . . . . . . 9 194 = 194
3502, 16deccl 12105 . . . . . . . . . 10 24 ∈ ℕ0
351 eqid 2825 . . . . . . . . . . 11 24 = 24
3522, 16, 344, 351decsuc 12121 . . . . . . . . . 10 (24 + 1) = 25
353 eqid 2825 . . . . . . . . . . . 12 23 = 23
3542, 21, 100, 353decsuc 12121 . . . . . . . . . . 11 (23 + 1) = 24
35534, 5, 11, 27, 311, 116, 354, 183decadd 12144 . . . . . . . . . 10 (230 + 19) = 249
356350, 352, 355decsucc 12131 . . . . . . . . 9 ((230 + 19) + 1) = 250
357 9p4e13 12179 . . . . . . . . 9 (9 + 4) = 13
35848, 27, 45, 16, 310, 349, 356, 21, 357decaddc 12145 . . . . . . . 8 (2309 + 194) = 2503
359358, 1eqtr4i 2851 . . . . . . 7 (2309 + 194) = 𝑁
360 eqid 2825 . . . . . . . . 9 91 = 91
361 eqid 2825 . . . . . . . . . . . 12 15 = 15
362204addid2i 10820 . . . . . . . . . . . . 13 (0 + 7) = 7
363362, 192eqtri 2848 . . . . . . . . . . . 12 (0 + 7) = 07
36478, 172oveq12i 7163 . . . . . . . . . . . . 13 ((1 · 2) + (0 + 1)) = (2 + 1)
365364, 81eqtri 2848 . . . . . . . . . . . 12 ((1 · 2) + (0 + 1)) = 3
36611, 5, 30, 156, 362decaddi 12150 . . . . . . . . . . . 12 ((5 · 2) + 7) = 17
36711, 3, 5, 30, 361, 363, 2, 30, 11, 365, 366decmac 12142 . . . . . . . . . . 11 ((15 · 2) + (0 + 7)) = 37
36884, 135oveq12i 7163 . . . . . . . . . . . . 13 ((1 · 5) + (0 + 2)) = (5 + 2)
369 5p2e7 11785 . . . . . . . . . . . . 13 (5 + 2) = 7
370368, 369eqtri 2848 . . . . . . . . . . . 12 ((1 · 5) + (0 + 2)) = 7
37111, 3, 5, 11, 361, 216, 3, 24, 2, 370, 175decmac 12142 . . . . . . . . . . 11 ((15 · 5) + 1) = 76
3722, 3, 5, 11, 74, 285, 39, 24, 30, 367, 371decma2c 12143 . . . . . . . . . 10 ((15 · 25) + (1 + 0)) = 376
37339nn0cni 11901 . . . . . . . . . . . . 13 15 ∈ ℂ
374373mul01i 10822 . . . . . . . . . . . 12 (15 · 0) = 0
375374oveq1i 7161 . . . . . . . . . . 11 ((15 · 0) + 3) = (0 + 3)
376375, 157, 1933eqtri 2852 . . . . . . . . . 10 ((15 · 0) + 3) = 03
3774, 5, 11, 21, 71, 357, 39, 21, 5, 372, 376decma2c 12143 . . . . . . . . 9 ((15 · 250) + (9 + 4)) = 3763
37898, 172oveq12i 7163 . . . . . . . . . . 11 ((1 · 3) + (0 + 1)) = (3 + 1)
379378, 100eqtri 2848 . . . . . . . . . 10 ((1 · 3) + (0 + 1)) = 4
38011, 3, 5, 11, 361, 216, 21, 24, 11, 379, 196decmac 12142 . . . . . . . . 9 ((15 · 3) + 1) = 46
3816, 21, 27, 11, 1, 360, 39, 24, 16, 377, 380decma2c 12143 . . . . . . . 8 ((15 · 𝑁) + 91) = 37636
38245, 16deccl 12105 . . . . . . . . 9 194 ∈ ℕ0
383 eqid 2825 . . . . . . . . . 10 77 = 77
38411, 30deccl 12105 . . . . . . . . . . 11 17 ∈ ℕ0
385384, 3deccl 12105 . . . . . . . . . 10 175 ∈ ℕ0
386 eqid 2825 . . . . . . . . . . . 12 175 = 175
387384nn0cni 11901 . . . . . . . . . . . . . 14 17 ∈ ℂ
388387addid2i 10820 . . . . . . . . . . . . 13 (0 + 17) = 17
38911, 30, 152, 388decsuc 12121 . . . . . . . . . . . 12 ((0 + 17) + 1) = 18
390 7p5e12 12167 . . . . . . . . . . . 12 (7 + 5) = 12
3915, 30, 384, 3, 192, 386, 389, 2, 390decaddc 12145 . . . . . . . . . . 11 (7 + 175) = 182
392231, 131oveq12i 7163 . . . . . . . . . . . . 13 ((1 · 1) + (1 + 1)) = (1 + 2)
393392, 236eqtri 2848 . . . . . . . . . . . 12 ((1 · 1) + (1 + 1)) = 3
394120mulid1i 10637 . . . . . . . . . . . . . 14 (9 · 1) = 9
395394oveq1i 7161 . . . . . . . . . . . . 13 ((9 · 1) + 8) = (9 + 8)
396 9p8e17 12183 . . . . . . . . . . . . 13 (9 + 8) = 17
397395, 396eqtri 2848 . . . . . . . . . . . 12 ((9 · 1) + 8) = 17
39811, 27, 11, 18, 116, 229, 11, 30, 11, 393, 397decmac 12142 . . . . . . . . . . 11 ((19 · 1) + (18 + 0)) = 37
399169mulid1i 10637 . . . . . . . . . . . . 13 (4 · 1) = 4
400399oveq1i 7161 . . . . . . . . . . . 12 ((4 · 1) + 2) = (4 + 2)
401 4p2e6 11782 . . . . . . . . . . . 12 (4 + 2) = 6
402400, 401, 873eqtri 2852 . . . . . . . . . . 11 ((4 · 1) + 2) = 06
40345, 16, 63, 2, 349, 391, 11, 24, 5, 398, 402decmac 12142 . . . . . . . . . 10 ((194 · 1) + (7 + 175)) = 376
404120mulid2i 10638 . . . . . . . . . . . . . 14 (1 · 9) = 9
405161addid2i 10820 . . . . . . . . . . . . . 14 (0 + 8) = 8
406404, 405oveq12i 7163 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 8)) = (9 + 8)
407406, 396eqtri 2848 . . . . . . . . . . . 12 ((1 · 9) + (0 + 8)) = 17
408 9t9e81 12219 . . . . . . . . . . . . 13 (9 · 9) = 81
409169, 90, 344addcomli 10824 . . . . . . . . . . . . 13 (1 + 4) = 5
41018, 11, 16, 408, 409decaddi 12150 . . . . . . . . . . . 12 ((9 · 9) + 4) = 85
41111, 27, 5, 16, 116, 171, 27, 3, 18, 407, 410decmac 12142 . . . . . . . . . . 11 ((19 · 9) + (0 + 4)) = 175
412 9t4e36 12214 . . . . . . . . . . . . 13 (9 · 4) = 36
413120, 169, 412mulcomli 10642 . . . . . . . . . . . 12 (4 · 9) = 36
414 7p6e13 12168 . . . . . . . . . . . . 13 (7 + 6) = 13
415204, 93, 414addcomli 10824 . . . . . . . . . . . 12 (6 + 7) = 13
41621, 24, 30, 413, 100, 21, 415decaddci 12151 . . . . . . . . . . 11 ((4 · 9) + 7) = 43
41745, 16, 5, 30, 349, 192, 27, 21, 16, 411, 416decmac 12142 . . . . . . . . . 10 ((194 · 9) + 7) = 1753
41811, 27, 30, 30, 116, 383, 382, 21, 385, 403, 417decma2c 12143 . . . . . . . . 9 ((194 · 19) + 77) = 3763
419169mulid2i 10638 . . . . . . . . . . . . 13 (1 · 4) = 4
420419, 157oveq12i 7163 . . . . . . . . . . . 12 ((1 · 4) + (0 + 3)) = (4 + 3)
421 4p3e7 11783 . . . . . . . . . . . 12 (4 + 3) = 7
422420, 421eqtri 2848 . . . . . . . . . . 11 ((1 · 4) + (0 + 3)) = 7
42321, 24, 144, 412decsuc 12121 . . . . . . . . . . 11 ((9 · 4) + 1) = 37
42411, 27, 5, 11, 116, 216, 16, 30, 21, 422, 423decmac 12142 . . . . . . . . . 10 ((19 · 4) + 1) = 77
425 4t4e16 12189 . . . . . . . . . 10 (4 · 4) = 16
42616, 45, 16, 349, 24, 11, 424, 425decmul1c 12155 . . . . . . . . 9 (194 · 4) = 776
427382, 45, 16, 349, 24, 37, 418, 426decmul2c 12156 . . . . . . . 8 (194 · 194) = 37636
428381, 427eqtr4i 2851 . . . . . . 7 ((15 · 𝑁) + 91) = (194 · 194)
42910, 43, 44, 47, 42, 49, 342, 348, 359, 428mod2xnegi 16399 . . . . . 6 ((2↑156) mod 𝑁) = (91 mod 𝑁)
430 eqid 2825 . . . . . . 7 156 = 156
431117, 172oveq12i 7163 . . . . . . . . 9 ((2 · 1) + (0 + 1)) = (2 + 1)
432431, 81eqtri 2848 . . . . . . . 8 ((2 · 1) + (0 + 1)) = 3
43383, 77, 156mulcomli 10642 . . . . . . . . 9 (2 · 5) = 10
43411, 5, 172, 433decsuc 12121 . . . . . . . 8 ((2 · 5) + 1) = 11
43511, 3, 5, 11, 361, 216, 2, 11, 11, 432, 434decma2c 12143 . . . . . . 7 ((2 · 15) + 1) = 31
436 6t2e12 12194 . . . . . . . 8 (6 · 2) = 12
43793, 77, 436mulcomli 10642 . . . . . . 7 (2 · 6) = 12
4382, 39, 24, 430, 2, 11, 435, 437decmul2c 12156 . . . . . 6 (2 · 156) = 312
439 eqid 2825 . . . . . . . 8 772 = 772
44030, 30, 152, 383decsuc 12121 . . . . . . . . 9 (77 + 1) = 78
441204addid1i 10819 . . . . . . . . . . 11 (7 + 0) = 7
442441, 192eqtri 2848 . . . . . . . . . 10 (7 + 0) = 07
443110, 135oveq12i 7163 . . . . . . . . . . 11 ((3 · 2) + (0 + 2)) = (6 + 2)
444 6p2e8 11788 . . . . . . . . . . 11 (6 + 2) = 8
445443, 444eqtri 2848 . . . . . . . . . 10 ((3 · 2) + (0 + 2)) = 8
446204, 83, 390addcomli 10824 . . . . . . . . . . 11 (5 + 7) = 12
44711, 3, 30, 178, 131, 2, 446decaddci 12151 . . . . . . . . . 10 ((3 · 5) + 7) = 22
4482, 3, 5, 30, 74, 442, 21, 2, 2, 445, 447decma2c 12143 . . . . . . . . 9 ((3 · 25) + (7 + 0)) = 82
44997mul01i 10822 . . . . . . . . . . 11 (3 · 0) = 0
450449oveq1i 7161 . . . . . . . . . 10 ((3 · 0) + 8) = (0 + 8)
451450, 405, 2473eqtri 2852 . . . . . . . . 9 ((3 · 0) + 8) = 08
4524, 5, 30, 18, 71, 440, 21, 18, 5, 448, 451decma2c 12143 . . . . . . . 8 ((3 · 250) + (77 + 1)) = 828
453198oveq1i 7161 . . . . . . . . 9 ((3 · 3) + 2) = (9 + 2)
454453, 148eqtri 2848 . . . . . . . 8 ((3 · 3) + 2) = 11
4556, 21, 37, 2, 1, 439, 21, 11, 11, 452, 454decma2c 12143 . . . . . . 7 ((3 · 𝑁) + 772) = 8281
45618, 11, 131, 408decsuc 12121 . . . . . . . . 9 ((9 · 9) + 1) = 82
457404oveq1i 7161 . . . . . . . . . 10 ((1 · 9) + 9) = (9 + 9)
458 9p9e18 12184 . . . . . . . . . 10 (9 + 9) = 18
459457, 458eqtri 2848 . . . . . . . . 9 ((1 · 9) + 9) = 18
46027, 11, 27, 360, 27, 18, 11, 456, 459decrmac 12148 . . . . . . . 8 ((91 · 9) + 9) = 828
46142nn0cni 11901 . . . . . . . . 9 91 ∈ ℂ
462461mulid1i 10637 . . . . . . . 8 (91 · 1) = 91
46342, 27, 11, 360, 11, 27, 460, 462decmul2c 12156 . . . . . . 7 (91 · 91) = 8281
464455, 463eqtr4i 2851 . . . . . 6 ((3 · 𝑁) + 772) = (91 · 91)
4659, 10, 40, 41, 42, 38, 429, 438, 464mod2xi 16397 . . . . 5 ((2↑312) mod 𝑁) = (772 mod 𝑁)
466 eqid 2825 . . . . . 6 312 = 312
467 eqid 2825 . . . . . . . . 9 31 = 31
468306oveq1i 7161 . . . . . . . . . 10 ((2 · 3) + 0) = (6 + 0)
469468, 254eqtri 2848 . . . . . . . . 9 ((2 · 3) + 0) = 6
470117, 142eqtri 2848 . . . . . . . . 9 (2 · 1) = 02
4712, 21, 11, 467, 2, 5, 469, 470decmul2c 12156 . . . . . . . 8 (2 · 31) = 62
472471oveq1i 7161 . . . . . . 7 ((2 · 31) + 0) = (62 + 0)
47325nn0cni 11901 . . . . . . . 8 62 ∈ ℂ
474473addid1i 10819 . . . . . . 7 (62 + 0) = 62
475472, 474eqtri 2848 . . . . . 6 ((2 · 31) + 0) = 62
476112, 101eqtri 2848 . . . . . 6 (2 · 2) = 04
4772, 22, 2, 466, 16, 5, 475, 476decmul2c 12156 . . . . 5 (2 · 312) = 624
478 eqid 2825 . . . . . . 7 270 = 270
47930, 11deccl 12105 . . . . . . 7 71 ∈ ℕ0
480 eqid 2825 . . . . . . . . 9 71 = 71
481 7p2e9 11790 . . . . . . . . . 10 (7 + 2) = 9
482204, 77, 481addcomli 10824 . . . . . . . . 9 (2 + 7) = 9
4832, 30, 30, 11, 153, 480, 482, 152decadd 12144 . . . . . . . 8 (27 + 71) = 98
484120addid1i 10819 . . . . . . . . . 10 (9 + 0) = 9
485484, 168eqtri 2848 . . . . . . . . 9 (9 + 0) = 09
48652, 27deccl 12105 . . . . . . . . 9 119 ∈ ℕ0
487 eqid 2825 . . . . . . . . . 10 238 = 238
488486nn0cni 11901 . . . . . . . . . . 11 119 ∈ ℂ
489488addid2i 10820 . . . . . . . . . 10 (0 + 119) = 119
49011, 11, 2, 214, 236decaddi 12150 . . . . . . . . . . 11 (11 + 2) = 13
491112, 79oveq12i 7163 . . . . . . . . . . . 12 ((2 · 2) + (1 + 0)) = (4 + 1)
492491, 344eqtri 2848 . . . . . . . . . . 11 ((2 · 2) + (1 + 0)) = 5
493110oveq1i 7161 . . . . . . . . . . . 12 ((3 · 2) + 3) = (6 + 3)
494493, 132, 1683eqtri 2852 . . . . . . . . . . 11 ((3 · 2) + 3) = 09
4952, 21, 11, 21, 353, 490, 2, 27, 5, 492, 494decmac 12142 . . . . . . . . . 10 ((23 · 2) + (11 + 2)) = 59
496 9p6e15 12181 . . . . . . . . . . . 12 (9 + 6) = 15
497120, 93, 496addcomli 10824 . . . . . . . . . . 11 (6 + 9) = 15
49811, 24, 27, 108, 131, 3, 497decaddci 12151 . . . . . . . . . 10 ((8 · 2) + 9) = 25
49934, 18, 52, 27, 487, 489, 2, 3, 2, 495, 498decmac 12142 . . . . . . . . 9 ((238 · 2) + (0 + 119)) = 595
500172oveq2i 7162 . . . . . . . . . . . 12 ((2 · 5) + (0 + 1)) = ((2 · 5) + 1)
501500, 434eqtri 2848 . . . . . . . . . . 11 ((2 · 5) + (0 + 1)) = 11
5022, 21, 5, 16, 353, 171, 3, 27, 11, 501, 180decmac 12142 . . . . . . . . . 10 ((23 · 5) + (0 + 4)) = 119
50334, 18, 5, 27, 487, 168, 3, 27, 16, 502, 184decmac 12142 . . . . . . . . 9 ((238 · 5) + 9) = 1199
5042, 3, 5, 27, 74, 485, 35, 27, 486, 499, 503decma2c 12143 . . . . . . . 8 ((238 · 25) + (9 + 0)) = 5959
50535nn0cni 11901 . . . . . . . . . . 11 238 ∈ ℂ
506505mul01i 10822 . . . . . . . . . 10 (238 · 0) = 0
507506oveq1i 7161 . . . . . . . . 9 ((238 · 0) + 8) = (0 + 8)
508507, 405, 2473eqtri 2852 . . . . . . . 8 ((238 · 0) + 8) = 08
5094, 5, 27, 18, 71, 483, 35, 18, 5, 504, 508decma2c 12143 . . . . . . 7 ((238 · 250) + (27 + 71)) = 59598
510306, 172oveq12i 7163 . . . . . . . . . . . 12 ((2 · 3) + (0 + 1)) = (6 + 1)
511510, 144eqtri 2848 . . . . . . . . . . 11 ((2 · 3) + (0 + 1)) = 7
5122, 21, 5, 2, 353, 142, 21, 11, 11, 511, 454decmac 12142 . . . . . . . . . 10 ((23 · 3) + 2) = 71
51321, 34, 18, 487, 16, 2, 512, 203decmul1c 12155 . . . . . . . . 9 (238 · 3) = 714
514513oveq1i 7161 . . . . . . . 8 ((238 · 3) + 0) = (714 + 0)
515479, 16deccl 12105 . . . . . . . . . 10 714 ∈ ℕ0
516515nn0cni 11901 . . . . . . . . 9 714 ∈ ℂ
517516addid1i 10819 . . . . . . . 8 (714 + 0) = 714
518514, 517eqtri 2848 . . . . . . 7 ((238 · 3) + 0) = 714
5196, 21, 31, 5, 1, 478, 35, 16, 479, 509, 518decma2c 12143 . . . . . 6 ((238 · 𝑁) + 270) = 595984
52039, 16deccl 12105 . . . . . . 7 154 ∈ ℕ0
521 eqid 2825 . . . . . . . 8 154 = 154
5223, 16deccl 12105 . . . . . . . . 9 54 ∈ ℕ0
523522, 5deccl 12105 . . . . . . . 8 540 ∈ ℕ0
5243, 3deccl 12105 . . . . . . . . 9 55 ∈ ℕ0
525 eqid 2825 . . . . . . . . . 10 540 = 540
526 eqid 2825 . . . . . . . . . . 11 54 = 54
52783addid2i 10820 . . . . . . . . . . 11 (0 + 5) = 5
5285, 11, 3, 16, 216, 526, 527, 409decadd 12144 . . . . . . . . . 10 (1 + 54) = 55
52983addid1i 10819 . . . . . . . . . 10 (5 + 0) = 5
53011, 3, 522, 5, 361, 525, 528, 529decadd 12144 . . . . . . . . 9 (15 + 540) = 555
531 eqid 2825 . . . . . . . . . . 11 55 = 55
5323, 3, 86, 531decsuc 12121 . . . . . . . . . 10 (55 + 1) = 56
533 7t7e49 12204 . . . . . . . . . . 11 (7 · 7) = 49
534 5p5e10 12161 . . . . . . . . . . 11 (5 + 5) = 10
53516, 27, 11, 5, 533, 534, 344, 484decadd 12144 . . . . . . . . . 10 ((7 · 7) + (5 + 5)) = 59
53616, 27, 24, 533, 344, 3, 496decaddci 12151 . . . . . . . . . 10 ((7 · 7) + 6) = 55
53730, 30, 3, 24, 383, 532, 30, 3, 3, 535, 536decmac 12142 . . . . . . . . 9 ((77 · 7) + (55 + 1)) = 595
53883, 169, 179addcomli 10824 . . . . . . . . . 10 (4 + 5) = 9
53911, 16, 3, 345, 538decaddi 12150 . . . . . . . . 9 ((2 · 7) + 5) = 19
54037, 2, 524, 3, 439, 530, 30, 27, 11, 537, 539decmac 12142 . . . . . . . 8 ((772 · 7) + (15 + 540)) = 5959
541527oveq2i 7162 . . . . . . . . . . 11 ((7 · 7) + (0 + 5)) = ((7 · 7) + 5)
542 9p5e14 12180 . . . . . . . . . . . 12 (9 + 5) = 14
54316, 27, 3, 533, 344, 16, 542decaddci 12151 . . . . . . . . . . 11 ((7 · 7) + 5) = 54
544541, 543eqtri 2848 . . . . . . . . . 10 ((7 · 7) + (0 + 5)) = 54
54516, 344, 533decsucc 12131 . . . . . . . . . 10 ((7 · 7) + 1) = 50
54630, 30, 5, 11, 383, 262, 30, 5, 3, 544, 545decmac 12142 . . . . . . . . 9 ((77 · 7) + (0 + 1)) = 540
547 4p4e8 11784 . . . . . . . . . 10 (4 + 4) = 8
54811, 16, 16, 345, 547decaddi 12150 . . . . . . . . 9 ((2 · 7) + 4) = 18
54937, 2, 5, 16, 439, 101, 30, 18, 11, 546, 548decmac 12142 . . . . . . . 8 ((772 · 7) + 4) = 5408
55030, 30, 39, 16, 383, 521, 38, 18, 523, 540, 549decma2c 12143 . . . . . . 7 ((772 · 77) + 154) = 59598
55111, 16, 344, 301decsuc 12121 . . . . . . . . 9 ((7 · 2) + 1) = 15
5522, 30, 30, 383, 16, 11, 551, 301decmul1c 12155 . . . . . . . 8 (77 · 2) = 154
5532, 37, 2, 439, 552, 112decmul1 12154 . . . . . . 7 (772 · 2) = 1544
55438, 37, 2, 439, 16, 520, 550, 553decmul2c 12156 . . . . . 6 (772 · 772) = 595984
555519, 554eqtr4i 2851 . . . . 5 ((238 · 𝑁) + 270) = (772 · 772)
5569, 10, 33, 36, 38, 32, 465, 477, 555mod2xi 16397 . . . 4 ((2↑624) mod 𝑁) = (270 mod 𝑁)
557 eqid 2825 . . . . 5 624 = 624
558 eqid 2825 . . . . . . . 8 62 = 62
559437oveq1i 7161 . . . . . . . . 9 ((2 · 6) + 0) = (12 + 0)
56012nn0cni 11901 . . . . . . . . . 10 12 ∈ ℂ
561560addid1i 10819 . . . . . . . . 9 (12 + 0) = 12
562559, 561eqtri 2848 . . . . . . . 8 ((2 · 6) + 0) = 12
5632, 24, 2, 558, 16, 5, 562, 476decmul2c 12156 . . . . . . 7 (2 · 62) = 124
564563oveq1i 7161 . . . . . 6 ((2 · 62) + 0) = (124 + 0)
56517nn0cni 11901 . . . . . . 7 124 ∈ ℂ
566565addid1i 10819 . . . . . 6 (124 + 0) = 124
567564, 566eqtri 2848 . . . . 5 ((2 · 62) + 0) = 124
568169, 77, 315mulcomli 10642 . . . . . 6 (2 · 4) = 8
569568, 247eqtri 2848 . . . . 5 (2 · 4) = 08
5702, 25, 16, 557, 18, 5, 567, 569decmul2c 12156 . . . 4 (2 · 624) = 1248
571 eqid 2825 . . . . . 6 313 = 313
57221, 11, 27, 467, 100, 221decaddci2 12152 . . . . . . 7 (31 + 9) = 40
573169addid1i 10819 . . . . . . . . 9 (4 + 0) = 4
574573, 101eqtri 2848 . . . . . . . 8 (4 + 0) = 04
57511, 16deccl 12105 . . . . . . . 8 14 ∈ ℕ0
576 eqid 2825 . . . . . . . . 9 29 = 29
577575nn0cni 11901 . . . . . . . . . 10 14 ∈ ℂ
578577addid2i 10820 . . . . . . . . 9 (0 + 14) = 14
579112, 236oveq12i 7163 . . . . . . . . . 10 ((2 · 2) + (1 + 2)) = (4 + 3)
580579, 421eqtri 2848 . . . . . . . . 9 ((2 · 2) + (1 + 2)) = 7
58111, 18, 16, 121, 131, 2, 318decaddci 12151 . . . . . . . . 9 ((9 · 2) + 4) = 22
5822, 27, 11, 16, 576, 578, 2, 2, 2, 580, 581decmac 12142 . . . . . . . 8 ((29 · 2) + (0 + 14)) = 72
58311, 5, 16, 433, 170decaddi 12150 . . . . . . . . 9 ((2 · 5) + 4) = 14
584 9t5e45 12215 . . . . . . . . . 10 (9 · 5) = 45
58516, 3, 16, 584, 179decaddi 12150 . . . . . . . . 9 ((9 · 5) + 4) = 49
5862, 27, 16, 576, 3, 27, 16, 583, 585decrmac 12148 . . . . . . . 8 ((29 · 5) + 4) = 149
5872, 3, 5, 16, 74, 574, 28, 27, 575, 582, 586decma2c 12143 . . . . . . 7 ((29 · 25) + (4 + 0)) = 729
588137mul01i 10822 . . . . . . . . 9 (29 · 0) = 0
589588oveq1i 7161 . . . . . . . 8 ((29 · 0) + 0) = (0 + 0)
590589, 232, 2483eqtri 2852 . . . . . . 7 ((29 · 0) + 0) = 00
5914, 5, 16, 5, 71, 572, 28, 5, 5, 587, 590decma2c 12143 . . . . . 6 ((29 · 250) + (31 + 9)) = 7290
592306, 157oveq12i 7163 . . . . . . . 8 ((2 · 3) + (0 + 3)) = (6 + 3)
593592, 132eqtri 2848 . . . . . . 7 ((2 · 3) + (0 + 3)) = 9
594 9t3e27 12213 . . . . . . . 8 (9 · 3) = 27
595 7p3e10 12165 . . . . . . . 8 (7 + 3) = 10
5962, 30, 21, 594, 81, 595decaddci2 12152 . . . . . . 7 ((9 · 3) + 3) = 30
5972, 27, 5, 21, 576, 193, 21, 5, 21, 593, 596decmac 12142 . . . . . 6 ((29 · 3) + 3) = 90
5986, 21, 22, 21, 1, 571, 28, 5, 27, 591, 597decma2c 12143 . . . . 5 ((29 · 𝑁) + 313) = 72900
59963, 27deccl 12105 . . . . . . . . 9 189 ∈ ℕ0
600 eqid 2825 . . . . . . . . . 10 189 = 189
601161, 169, 318addcomli 10824 . . . . . . . . . . . 12 (4 + 8) = 12
60211, 16, 18, 301, 131, 2, 601decaddci 12151 . . . . . . . . . . 11 ((7 · 2) + 8) = 22
6032, 30, 11, 18, 153, 229, 2, 2, 2, 580, 602decmac 12142 . . . . . . . . . 10 ((27 · 2) + (18 + 0)) = 72
604297oveq1i 7161 . . . . . . . . . . 11 ((0 · 2) + 9) = (0 + 9)
605604, 183, 1683eqtri 2852 . . . . . . . . . 10 ((0 · 2) + 9) = 09
60631, 5, 63, 27, 478, 600, 2, 27, 5, 603, 605decmac 12142 . . . . . . . . 9 ((270 · 2) + 189) = 729
60730, 2, 30, 153, 27, 16, 548, 533decmul1c 12155 . . . . . . . . . 10 (27 · 7) = 189
608204mul02i 10821 . . . . . . . . . 10 (0 · 7) = 0
60930, 31, 5, 478, 607, 608decmul1 12154 . . . . . . . . 9 (270 · 7) = 1890
61032, 2, 30, 153, 5, 599, 606, 609decmul2c 12156 . . . . . . . 8 (270 · 27) = 7290
611610oveq1i 7161 . . . . . . 7 ((270 · 27) + 0) = (7290 + 0)
61230, 2deccl 12105 . . . . . . . . . . 11 72 ∈ ℕ0
613612, 27deccl 12105 . . . . . . . . . 10 729 ∈ ℕ0
614613, 5deccl 12105 . . . . . . . . 9 7290 ∈ ℕ0
615614nn0cni 11901 . . . . . . . 8 7290 ∈ ℂ
616615addid1i 10819 . . . . . . 7 (7290 + 0) = 7290
617611, 616eqtri 2848 . . . . . 6 ((270 · 27) + 0) = 7290
61832nn0cni 11901 . . . . . . . 8 270 ∈ ℂ
619618mul01i 10822 . . . . . . 7 (270 · 0) = 0
620619, 248eqtri 2848 . . . . . 6 (270 · 0) = 00
62132, 31, 5, 478, 5, 5, 617, 620decmul2c 12156 . . . . 5 (270 · 270) = 72900
622598, 621eqtr4i 2851 . . . 4 ((29 · 𝑁) + 313) = (270 · 270)
6239, 10, 26, 29, 32, 23, 556, 570, 622mod2xi 16397 . . 3 ((2↑1248) mod 𝑁) = (313 mod 𝑁)
624 cu2 13556 . . . 4 (2↑3) = 8
625624oveq1i 7161 . . 3 ((2↑3) mod 𝑁) = (8 mod 𝑁)
626 eqid 2825 . . . 4 1248 = 1248
627 eqid 2825 . . . . 5 124 = 124
62812, 16, 344, 627decsuc 12121 . . . 4 (124 + 1) = 125
629 8p3e11 12171 . . . 4 (8 + 3) = 11
63017, 18, 21, 626, 628, 11, 629decaddci 12151 . . 3 (1248 + 3) = 1251
6319nncni 11640 . . . . . . 7 𝑁 ∈ ℂ
632631mulid2i 10638 . . . . . 6 (1 · 𝑁) = 𝑁
633632, 1eqtri 2848 . . . . 5 (1 · 𝑁) = 2503
6346, 21, 100, 633decsuc 12121 . . . 4 ((1 · 𝑁) + 1) = 2504
635161, 97, 203mulcomli 10642 . . . . . . 7 (3 · 8) = 24
6362, 16, 344, 635decsuc 12121 . . . . . 6 ((3 · 8) + 1) = 25
637161mulid2i 10638 . . . . . . . 8 (1 · 8) = 8
638637oveq1i 7161 . . . . . . 7 ((1 · 8) + 2) = (8 + 2)
639 8p2e10 12170 . . . . . . 7 (8 + 2) = 10
640638, 639eqtri 2848 . . . . . 6 ((1 · 8) + 2) = 10
64121, 11, 2, 467, 18, 5, 11, 636, 640decrmac 12148 . . . . 5 ((31 · 8) + 2) = 250
64218, 22, 21, 571, 16, 2, 641, 635decmul1c 12155 . . . 4 (313 · 8) = 2504
643634, 642eqtr4i 2851 . . 3 ((1 · 𝑁) + 1) = (313 · 8)
6449, 10, 19, 20, 23, 11, 21, 18, 623, 625, 630, 643modxai 16396 . 2 ((2↑1251) mod 𝑁) = (1 mod 𝑁)
645 eqid 2825 . . . 4 1251 = 1251
646 eqid 2825 . . . . . 6 125 = 125
647 eqid 2825 . . . . . . 7 12 = 12
648117, 232oveq12i 7163 . . . . . . . 8 ((2 · 1) + (0 + 0)) = (2 + 0)
649648, 287eqtri 2848 . . . . . . 7 ((2 · 1) + (0 + 0)) = 2
650112oveq1i 7161 . . . . . . . 8 ((2 · 2) + 1) = (4 + 1)
6513dec0h 12112 . . . . . . . 8 5 = 05
652650, 344, 6513eqtri 2852 . . . . . . 7 ((2 · 2) + 1) = 05
65311, 2, 5, 11, 647, 216, 2, 3, 5, 649, 652decma2c 12143 . . . . . 6 ((2 · 12) + 1) = 25
6542, 12, 3, 646, 5, 11, 653, 433decmul2c 12156 . . . . 5 (2 · 125) = 250
6554, 5, 5, 654, 232decaddi 12150 . . . 4 ((2 · 125) + 0) = 250
6562, 13, 11, 645, 2, 5, 655, 470decmul2c 12156 . . 3 (2 · 1251) = 2502
6576, 2deccl 12105 . . . . 5 2502 ∈ ℕ0
658657nn0cni 11901 . . . 4 2502 ∈ ℂ
659 eqid 2825 . . . . . 6 2502 = 2502
6606, 2, 81, 659decsuc 12121 . . . . 5 (2502 + 1) = 2503
6611, 660eqtr4i 2851 . . . 4 𝑁 = (2502 + 1)
662658, 90, 661mvrraddi 10895 . . 3 (𝑁 − 1) = 2502
663656, 662eqtr4i 2851 . 2 (2 · 1251) = (𝑁 − 1)
664631mul02i 10821 . . . 4 (0 · 𝑁) = 0
665664oveq1i 7161 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
666231, 172eqtr4i 2851 . . 3 (1 · 1) = (0 + 1)
667665, 666eqtr4i 2851 . 2 ((0 · 𝑁) + 1) = (1 · 1)
6689, 10, 14, 15, 11, 11, 644, 663, 667mod2xi 16397 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7151  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  cmin 10862  cn 11630  2c2 11684  3c3 11685  4c4 11686  5c5 11687  6c6 11688  7c7 11689  8c8 11690  9c9 11691  cdc 12090   mod cmo 13230  cexp 13422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12383  df-fl 13155  df-mod 13231  df-seq 13363  df-exp 13423
This theorem is referenced by:  2503prm  16465
  Copyright terms: Public domain W3C validator