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

Theorem 4001lem4 17077
Description: Lemma for 4001prm 17078. Calculate the GCD of 2↑800 − 1≡2310 with 𝑁 = 4001. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
4001prm.1 𝑁 = 4001
Assertion
Ref Expression
4001lem4 (((2↑800) − 1) gcd 𝑁) = 1

Proof of Theorem 4001lem4
StepHypRef Expression
1 2nn 12285 . . . 4 2 ∈ ℕ
2 8nn0 12495 . . . . . 6 8 ∈ ℕ0
3 0nn0 12487 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12692 . . . . 5 80 ∈ ℕ0
54, 3deccl 12692 . . . 4 800 ∈ ℕ0
6 nnexpcl 14040 . . . 4 ((2 ∈ ℕ ∧ 800 ∈ ℕ0) → (2↑800) ∈ ℕ)
71, 5, 6mp2an 691 . . 3 (2↑800) ∈ ℕ
8 nnm1nn0 12513 . . 3 ((2↑800) ∈ ℕ → ((2↑800) − 1) ∈ ℕ0)
97, 8ax-mp 5 . 2 ((2↑800) − 1) ∈ ℕ0
10 2nn0 12489 . . . . 5 2 ∈ ℕ0
11 3nn0 12490 . . . . 5 3 ∈ ℕ0
1210, 11deccl 12692 . . . 4 23 ∈ ℕ0
13 1nn0 12488 . . . 4 1 ∈ ℕ0
1412, 13deccl 12692 . . 3 231 ∈ ℕ0
1514, 3deccl 12692 . 2 2310 ∈ ℕ0
16 4001prm.1 . . 3 𝑁 = 4001
17 4nn0 12491 . . . . . 6 4 ∈ ℕ0
1817, 3deccl 12692 . . . . 5 40 ∈ ℕ0
1918, 3deccl 12692 . . . 4 400 ∈ ℕ0
20 1nn 12223 . . . 4 1 ∈ ℕ
2119, 20decnncl 12697 . . 3 4001 ∈ ℕ
2216, 21eqeltri 2830 . 2 𝑁 ∈ ℕ
23164001lem2 17075 . . 3 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
24 0p1e1 12334 . . . 4 (0 + 1) = 1
25 eqid 2733 . . . 4 2310 = 2310
2614, 3, 24, 25decsuc 12708 . . 3 (2310 + 1) = 2311
2722, 7, 13, 15, 23, 26modsubi 17005 . 2 (((2↑800) − 1) mod 𝑁) = (2310 mod 𝑁)
28 6nn0 12493 . . . . . 6 6 ∈ ℕ0
2913, 28deccl 12692 . . . . 5 16 ∈ ℕ0
30 9nn0 12496 . . . . 5 9 ∈ ℕ0
3129, 30deccl 12692 . . . 4 169 ∈ ℕ0
3231, 13deccl 12692 . . 3 1691 ∈ ℕ0
3328, 13deccl 12692 . . . . 5 61 ∈ ℕ0
3433, 30deccl 12692 . . . 4 619 ∈ ℕ0
35 5nn0 12492 . . . . . . 7 5 ∈ ℕ0
3617, 35deccl 12692 . . . . . 6 45 ∈ ℕ0
3736, 11deccl 12692 . . . . 5 453 ∈ ℕ0
3829, 28deccl 12692 . . . . . 6 166 ∈ ℕ0
3913, 10deccl 12692 . . . . . . . 8 12 ∈ ℕ0
4039, 13deccl 12692 . . . . . . 7 121 ∈ ℕ0
4111, 13deccl 12692 . . . . . . . . 9 31 ∈ ℕ0
4213, 17deccl 12692 . . . . . . . . . 10 14 ∈ ℕ0
4342nn0zi 12587 . . . . . . . . . . . . 13 14 ∈ ℤ
4411nn0zi 12587 . . . . . . . . . . . . 13 3 ∈ ℤ
45 gcdcom 16454 . . . . . . . . . . . . 13 ((14 ∈ ℤ ∧ 3 ∈ ℤ) → (14 gcd 3) = (3 gcd 14))
4643, 44, 45mp2an 691 . . . . . . . . . . . 12 (14 gcd 3) = (3 gcd 14)
47 3nn 12291 . . . . . . . . . . . . . 14 3 ∈ ℕ
48 4cn 12297 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
49 3cn 12293 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
50 4t3e12 12775 . . . . . . . . . . . . . . . 16 (4 · 3) = 12
5148, 49, 50mulcomli 11223 . . . . . . . . . . . . . . 15 (3 · 4) = 12
52 2p2e4 12347 . . . . . . . . . . . . . . 15 (2 + 2) = 4
5313, 10, 10, 51, 52decaddi 12737 . . . . . . . . . . . . . 14 ((3 · 4) + 2) = 14
54 2lt3 12384 . . . . . . . . . . . . . 14 2 < 3
5547, 17, 1, 53, 54ndvdsi 16355 . . . . . . . . . . . . 13 ¬ 3 ∥ 14
56 3prm 16631 . . . . . . . . . . . . . 14 3 ∈ ℙ
57 coprm 16648 . . . . . . . . . . . . . 14 ((3 ∈ ℙ ∧ 14 ∈ ℤ) → (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1))
5856, 43, 57mp2an 691 . . . . . . . . . . . . 13 (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1)
5955, 58mpbi 229 . . . . . . . . . . . 12 (3 gcd 14) = 1
6046, 59eqtri 2761 . . . . . . . . . . 11 (14 gcd 3) = 1
61 eqid 2733 . . . . . . . . . . . 12 14 = 14
6211dec0h 12699 . . . . . . . . . . . 12 3 = 03
63 2t1e2 12375 . . . . . . . . . . . . . 14 (2 · 1) = 2
6463, 24oveq12i 7421 . . . . . . . . . . . . 13 ((2 · 1) + (0 + 1)) = (2 + 1)
65 2p1e3 12354 . . . . . . . . . . . . 13 (2 + 1) = 3
6664, 65eqtri 2761 . . . . . . . . . . . 12 ((2 · 1) + (0 + 1)) = 3
67 2cn 12287 . . . . . . . . . . . . . . 15 2 ∈ ℂ
68 4t2e8 12380 . . . . . . . . . . . . . . 15 (4 · 2) = 8
6948, 67, 68mulcomli 11223 . . . . . . . . . . . . . 14 (2 · 4) = 8
7069oveq1i 7419 . . . . . . . . . . . . 13 ((2 · 4) + 3) = (8 + 3)
71 8p3e11 12758 . . . . . . . . . . . . 13 (8 + 3) = 11
7270, 71eqtri 2761 . . . . . . . . . . . 12 ((2 · 4) + 3) = 11
7313, 17, 3, 11, 61, 62, 10, 13, 13, 66, 72decma2c 12730 . . . . . . . . . . 11 ((2 · 14) + 3) = 31
7410, 11, 42, 60, 73gcdi 17006 . . . . . . . . . 10 (31 gcd 14) = 1
75 eqid 2733 . . . . . . . . . . 11 31 = 31
7649mullidi 11219 . . . . . . . . . . . . 13 (1 · 3) = 3
77 ax-1cn 11168 . . . . . . . . . . . . . 14 1 ∈ ℂ
7877addridi 11401 . . . . . . . . . . . . 13 (1 + 0) = 1
7976, 78oveq12i 7421 . . . . . . . . . . . 12 ((1 · 3) + (1 + 0)) = (3 + 1)
80 3p1e4 12357 . . . . . . . . . . . 12 (3 + 1) = 4
8179, 80eqtri 2761 . . . . . . . . . . 11 ((1 · 3) + (1 + 0)) = 4
82 1t1e1 12374 . . . . . . . . . . . . 13 (1 · 1) = 1
8382oveq1i 7419 . . . . . . . . . . . 12 ((1 · 1) + 4) = (1 + 4)
84 4p1e5 12358 . . . . . . . . . . . . 13 (4 + 1) = 5
8548, 77, 84addcomli 11406 . . . . . . . . . . . 12 (1 + 4) = 5
8635dec0h 12699 . . . . . . . . . . . 12 5 = 05
8783, 85, 863eqtri 2765 . . . . . . . . . . 11 ((1 · 1) + 4) = 05
8811, 13, 13, 17, 75, 61, 13, 35, 3, 81, 87decma2c 12730 . . . . . . . . . 10 ((1 · 31) + 14) = 45
8913, 42, 41, 74, 88gcdi 17006 . . . . . . . . 9 (45 gcd 31) = 1
90 eqid 2733 . . . . . . . . . 10 45 = 45
9169, 80oveq12i 7421 . . . . . . . . . . 11 ((2 · 4) + (3 + 1)) = (8 + 4)
92 8p4e12 12759 . . . . . . . . . . 11 (8 + 4) = 12
9391, 92eqtri 2761 . . . . . . . . . 10 ((2 · 4) + (3 + 1)) = 12
94 5cn 12300 . . . . . . . . . . . 12 5 ∈ ℂ
95 5t2e10 12777 . . . . . . . . . . . 12 (5 · 2) = 10
9694, 67, 95mulcomli 11223 . . . . . . . . . . 11 (2 · 5) = 10
9713, 3, 24, 96decsuc 12708 . . . . . . . . . 10 ((2 · 5) + 1) = 11
9817, 35, 11, 13, 90, 75, 10, 13, 13, 93, 97decma2c 12730 . . . . . . . . 9 ((2 · 45) + 31) = 121
9910, 41, 36, 89, 98gcdi 17006 . . . . . . . 8 (121 gcd 45) = 1
100 eqid 2733 . . . . . . . . 9 121 = 121
101 eqid 2733 . . . . . . . . . 10 12 = 12
10248addridi 11401 . . . . . . . . . . 11 (4 + 0) = 4
10317dec0h 12699 . . . . . . . . . . 11 4 = 04
104102, 103eqtri 2761 . . . . . . . . . 10 (4 + 0) = 04
105 00id 11389 . . . . . . . . . . . 12 (0 + 0) = 0
10682, 105oveq12i 7421 . . . . . . . . . . 11 ((1 · 1) + (0 + 0)) = (1 + 0)
107106, 78eqtri 2761 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = 1
10867mullidi 11219 . . . . . . . . . . . 12 (1 · 2) = 2
109108oveq1i 7419 . . . . . . . . . . 11 ((1 · 2) + 4) = (2 + 4)
110 4p2e6 12365 . . . . . . . . . . . 12 (4 + 2) = 6
11148, 67, 110addcomli 11406 . . . . . . . . . . 11 (2 + 4) = 6
11228dec0h 12699 . . . . . . . . . . 11 6 = 06
113109, 111, 1123eqtri 2765 . . . . . . . . . 10 ((1 · 2) + 4) = 06
11413, 10, 3, 17, 101, 104, 13, 28, 3, 107, 113decma2c 12730 . . . . . . . . 9 ((1 · 12) + (4 + 0)) = 16
11582oveq1i 7419 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
116 5p1e6 12359 . . . . . . . . . . 11 (5 + 1) = 6
11794, 77, 116addcomli 11406 . . . . . . . . . 10 (1 + 5) = 6
118115, 117, 1123eqtri 2765 . . . . . . . . 9 ((1 · 1) + 5) = 06
11939, 13, 17, 35, 100, 90, 13, 28, 3, 114, 118decma2c 12730 . . . . . . . 8 ((1 · 121) + 45) = 166
12013, 36, 40, 99, 119gcdi 17006 . . . . . . 7 (166 gcd 121) = 1
121 eqid 2733 . . . . . . . 8 166 = 166
122 eqid 2733 . . . . . . . . 9 16 = 16
12313, 10, 65, 101decsuc 12708 . . . . . . . . 9 (12 + 1) = 13
124 1p1e2 12337 . . . . . . . . . . 11 (1 + 1) = 2
12563, 124oveq12i 7421 . . . . . . . . . 10 ((2 · 1) + (1 + 1)) = (2 + 2)
126125, 52eqtri 2761 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = 4
127 6cn 12303 . . . . . . . . . . 11 6 ∈ ℂ
128 6t2e12 12781 . . . . . . . . . . 11 (6 · 2) = 12
129127, 67, 128mulcomli 11223 . . . . . . . . . 10 (2 · 6) = 12
130 3p2e5 12363 . . . . . . . . . . 11 (3 + 2) = 5
13149, 67, 130addcomli 11406 . . . . . . . . . 10 (2 + 3) = 5
13213, 10, 11, 129, 131decaddi 12737 . . . . . . . . 9 ((2 · 6) + 3) = 15
13313, 28, 13, 11, 122, 123, 10, 35, 13, 126, 132decma2c 12730 . . . . . . . 8 ((2 · 16) + (12 + 1)) = 45
13413, 10, 65, 129decsuc 12708 . . . . . . . 8 ((2 · 6) + 1) = 13
13529, 28, 39, 13, 121, 100, 10, 11, 13, 133, 134decma2c 12730 . . . . . . 7 ((2 · 166) + 121) = 453
13610, 40, 38, 120, 135gcdi 17006 . . . . . 6 (453 gcd 166) = 1
137 eqid 2733 . . . . . . 7 453 = 453
13829nn0cni 12484 . . . . . . . . 9 16 ∈ ℂ
139138addridi 11401 . . . . . . . 8 (16 + 0) = 16
14048mullidi 11219 . . . . . . . . . 10 (1 · 4) = 4
141140, 124oveq12i 7421 . . . . . . . . 9 ((1 · 4) + (1 + 1)) = (4 + 2)
142141, 110eqtri 2761 . . . . . . . 8 ((1 · 4) + (1 + 1)) = 6
14394mullidi 11219 . . . . . . . . . 10 (1 · 5) = 5
144143oveq1i 7419 . . . . . . . . 9 ((1 · 5) + 6) = (5 + 6)
145 6p5e11 12750 . . . . . . . . . 10 (6 + 5) = 11
146127, 94, 145addcomli 11406 . . . . . . . . 9 (5 + 6) = 11
147144, 146eqtri 2761 . . . . . . . 8 ((1 · 5) + 6) = 11
14817, 35, 13, 28, 90, 139, 13, 13, 13, 142, 147decma2c 12730 . . . . . . 7 ((1 · 45) + (16 + 0)) = 61
14976oveq1i 7419 . . . . . . . 8 ((1 · 3) + 6) = (3 + 6)
150 6p3e9 12372 . . . . . . . . 9 (6 + 3) = 9
151127, 49, 150addcomli 11406 . . . . . . . 8 (3 + 6) = 9
15230dec0h 12699 . . . . . . . 8 9 = 09
153149, 151, 1523eqtri 2765 . . . . . . 7 ((1 · 3) + 6) = 09
15436, 11, 29, 28, 137, 121, 13, 30, 3, 148, 153decma2c 12730 . . . . . 6 ((1 · 453) + 166) = 619
15513, 38, 37, 136, 154gcdi 17006 . . . . 5 (619 gcd 453) = 1
156 eqid 2733 . . . . . 6 619 = 619
157 7nn0 12494 . . . . . . 7 7 ∈ ℕ0
158 eqid 2733 . . . . . . 7 61 = 61
159 5p2e7 12368 . . . . . . . 8 (5 + 2) = 7
16017, 35, 10, 90, 159decaddi 12737 . . . . . . 7 (45 + 2) = 47
161102oveq2i 7420 . . . . . . . 8 ((2 · 6) + (4 + 0)) = ((2 · 6) + 4)
16213, 10, 17, 129, 111decaddi 12737 . . . . . . . 8 ((2 · 6) + 4) = 16
163161, 162eqtri 2761 . . . . . . 7 ((2 · 6) + (4 + 0)) = 16
16463oveq1i 7419 . . . . . . . 8 ((2 · 1) + 7) = (2 + 7)
165 7cn 12306 . . . . . . . . 9 7 ∈ ℂ
166 7p2e9 12373 . . . . . . . . 9 (7 + 2) = 9
167165, 67, 166addcomli 11406 . . . . . . . 8 (2 + 7) = 9
168164, 167, 1523eqtri 2765 . . . . . . 7 ((2 · 1) + 7) = 09
16928, 13, 17, 157, 158, 160, 10, 30, 3, 163, 168decma2c 12730 . . . . . 6 ((2 · 61) + (45 + 2)) = 169
170 9cn 12312 . . . . . . . 8 9 ∈ ℂ
171 9t2e18 12799 . . . . . . . 8 (9 · 2) = 18
172170, 67, 171mulcomli 11223 . . . . . . 7 (2 · 9) = 18
17313, 2, 11, 172, 124, 13, 71decaddci 12738 . . . . . 6 ((2 · 9) + 3) = 21
17433, 30, 36, 11, 156, 137, 10, 13, 10, 169, 173decma2c 12730 . . . . 5 ((2 · 619) + 453) = 1691
17510, 37, 34, 155, 174gcdi 17006 . . . 4 (1691 gcd 619) = 1
176 eqid 2733 . . . . 5 1691 = 1691
177 eqid 2733 . . . . . 6 169 = 169
17828, 13, 124, 158decsuc 12708 . . . . . 6 (61 + 1) = 62
179 6p1e7 12360 . . . . . . . 8 (6 + 1) = 7
180157dec0h 12699 . . . . . . . 8 7 = 07
181179, 180eqtri 2761 . . . . . . 7 (6 + 1) = 07
18282, 24oveq12i 7421 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
183182, 124eqtri 2761 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
184127mullidi 11219 . . . . . . . . 9 (1 · 6) = 6
185184oveq1i 7419 . . . . . . . 8 ((1 · 6) + 7) = (6 + 7)
186 7p6e13 12755 . . . . . . . . 9 (7 + 6) = 13
187165, 127, 186addcomli 11406 . . . . . . . 8 (6 + 7) = 13
188185, 187eqtri 2761 . . . . . . 7 ((1 · 6) + 7) = 13
18913, 28, 3, 157, 122, 181, 13, 11, 13, 183, 188decma2c 12730 . . . . . 6 ((1 · 16) + (6 + 1)) = 23
190170mullidi 11219 . . . . . . . 8 (1 · 9) = 9
191190oveq1i 7419 . . . . . . 7 ((1 · 9) + 2) = (9 + 2)
192 9p2e11 12764 . . . . . . 7 (9 + 2) = 11
193191, 192eqtri 2761 . . . . . 6 ((1 · 9) + 2) = 11
19429, 30, 28, 10, 177, 178, 13, 13, 13, 189, 193decma2c 12730 . . . . 5 ((1 · 169) + (61 + 1)) = 231
19582oveq1i 7419 . . . . . 6 ((1 · 1) + 9) = (1 + 9)
196 9p1e10 12679 . . . . . . 7 (9 + 1) = 10
197170, 77, 196addcomli 11406 . . . . . 6 (1 + 9) = 10
198195, 197eqtri 2761 . . . . 5 ((1 · 1) + 9) = 10
19931, 13, 33, 30, 176, 156, 13, 3, 13, 194, 198decma2c 12730 . . . 4 ((1 · 1691) + 619) = 2310
20013, 34, 32, 175, 199gcdi 17006 . . 3 (2310 gcd 1691) = 1
201 eqid 2733 . . . . . 6 231 = 231
20231nn0cni 12484 . . . . . . 7 169 ∈ ℂ
203202addridi 11401 . . . . . 6 (169 + 0) = 169
204 eqid 2733 . . . . . . 7 23 = 23
20513, 28, 179, 122decsuc 12708 . . . . . . 7 (16 + 1) = 17
206108, 124oveq12i 7421 . . . . . . . 8 ((1 · 2) + (1 + 1)) = (2 + 2)
207206, 52eqtri 2761 . . . . . . 7 ((1 · 2) + (1 + 1)) = 4
20876oveq1i 7419 . . . . . . . 8 ((1 · 3) + 7) = (3 + 7)
209 7p3e10 12752 . . . . . . . . 9 (7 + 3) = 10
210165, 49, 209addcomli 11406 . . . . . . . 8 (3 + 7) = 10
211208, 210eqtri 2761 . . . . . . 7 ((1 · 3) + 7) = 10
21210, 11, 13, 157, 204, 205, 13, 3, 13, 207, 211decma2c 12730 . . . . . 6 ((1 · 23) + (16 + 1)) = 40
21312, 13, 29, 30, 201, 203, 13, 3, 13, 212, 198decma2c 12730 . . . . 5 ((1 · 231) + (169 + 0)) = 400
21477mul01i 11404 . . . . . . 7 (1 · 0) = 0
215214oveq1i 7419 . . . . . 6 ((1 · 0) + 1) = (0 + 1)
21613dec0h 12699 . . . . . 6 1 = 01
217215, 24, 2163eqtri 2765 . . . . 5 ((1 · 0) + 1) = 01
21814, 3, 31, 13, 25, 176, 13, 13, 3, 213, 217decma2c 12730 . . . 4 ((1 · 2310) + 1691) = 4001
219218, 16eqtr4i 2764 . . 3 ((1 · 2310) + 1691) = 𝑁
22013, 32, 15, 200, 219gcdi 17006 . 2 (𝑁 gcd 2310) = 1
2219, 15, 22, 27, 220gcdmodi 17007 1 (((2↑800) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1542  wcel 2107   class class class wbr 5149  (class class class)co 7409  0cc0 11110  1c1 11111   + caddc 11113   · cmul 11115  cmin 11444  cn 12212  2c2 12267  3c3 12268  4c4 12269  5c5 12270  6c6 12271  7c7 12272  8c8 12273  9c9 12274  0cn0 12472  cz 12558  cdc 12677  cexp 14027  cdvds 16197   gcd cgcd 16435  cprime 16608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-dvds 16198  df-gcd 16436  df-prm 16609
This theorem is referenced by:  4001prm  17078
  Copyright terms: Public domain W3C validator