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

Theorem 4001lem4 17079
Description: Lemma for 4001prm 17080. 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 12287 . . . 4 2 ∈ ℕ
2 8nn0 12497 . . . . . 6 8 ∈ ℕ0
3 0nn0 12489 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12694 . . . . 5 80 ∈ ℕ0
54, 3deccl 12694 . . . 4 800 ∈ ℕ0
6 nnexpcl 14042 . . . 4 ((2 ∈ ℕ ∧ 800 ∈ ℕ0) → (2↑800) ∈ ℕ)
71, 5, 6mp2an 690 . . 3 (2↑800) ∈ ℕ
8 nnm1nn0 12515 . . 3 ((2↑800) ∈ ℕ → ((2↑800) − 1) ∈ ℕ0)
97, 8ax-mp 5 . 2 ((2↑800) − 1) ∈ ℕ0
10 2nn0 12491 . . . . 5 2 ∈ ℕ0
11 3nn0 12492 . . . . 5 3 ∈ ℕ0
1210, 11deccl 12694 . . . 4 23 ∈ ℕ0
13 1nn0 12490 . . . 4 1 ∈ ℕ0
1412, 13deccl 12694 . . 3 231 ∈ ℕ0
1514, 3deccl 12694 . 2 2310 ∈ ℕ0
16 4001prm.1 . . 3 𝑁 = 4001
17 4nn0 12493 . . . . . 6 4 ∈ ℕ0
1817, 3deccl 12694 . . . . 5 40 ∈ ℕ0
1918, 3deccl 12694 . . . 4 400 ∈ ℕ0
20 1nn 12225 . . . 4 1 ∈ ℕ
2119, 20decnncl 12699 . . 3 4001 ∈ ℕ
2216, 21eqeltri 2829 . 2 𝑁 ∈ ℕ
23164001lem2 17077 . . 3 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
24 0p1e1 12336 . . . 4 (0 + 1) = 1
25 eqid 2732 . . . 4 2310 = 2310
2614, 3, 24, 25decsuc 12710 . . 3 (2310 + 1) = 2311
2722, 7, 13, 15, 23, 26modsubi 17007 . 2 (((2↑800) − 1) mod 𝑁) = (2310 mod 𝑁)
28 6nn0 12495 . . . . . 6 6 ∈ ℕ0
2913, 28deccl 12694 . . . . 5 16 ∈ ℕ0
30 9nn0 12498 . . . . 5 9 ∈ ℕ0
3129, 30deccl 12694 . . . 4 169 ∈ ℕ0
3231, 13deccl 12694 . . 3 1691 ∈ ℕ0
3328, 13deccl 12694 . . . . 5 61 ∈ ℕ0
3433, 30deccl 12694 . . . 4 619 ∈ ℕ0
35 5nn0 12494 . . . . . . 7 5 ∈ ℕ0
3617, 35deccl 12694 . . . . . 6 45 ∈ ℕ0
3736, 11deccl 12694 . . . . 5 453 ∈ ℕ0
3829, 28deccl 12694 . . . . . 6 166 ∈ ℕ0
3913, 10deccl 12694 . . . . . . . 8 12 ∈ ℕ0
4039, 13deccl 12694 . . . . . . 7 121 ∈ ℕ0
4111, 13deccl 12694 . . . . . . . . 9 31 ∈ ℕ0
4213, 17deccl 12694 . . . . . . . . . 10 14 ∈ ℕ0
4342nn0zi 12589 . . . . . . . . . . . . 13 14 ∈ ℤ
4411nn0zi 12589 . . . . . . . . . . . . 13 3 ∈ ℤ
45 gcdcom 16456 . . . . . . . . . . . . 13 ((14 ∈ ℤ ∧ 3 ∈ ℤ) → (14 gcd 3) = (3 gcd 14))
4643, 44, 45mp2an 690 . . . . . . . . . . . 12 (14 gcd 3) = (3 gcd 14)
47 3nn 12293 . . . . . . . . . . . . . 14 3 ∈ ℕ
48 4cn 12299 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
49 3cn 12295 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
50 4t3e12 12777 . . . . . . . . . . . . . . . 16 (4 · 3) = 12
5148, 49, 50mulcomli 11225 . . . . . . . . . . . . . . 15 (3 · 4) = 12
52 2p2e4 12349 . . . . . . . . . . . . . . 15 (2 + 2) = 4
5313, 10, 10, 51, 52decaddi 12739 . . . . . . . . . . . . . 14 ((3 · 4) + 2) = 14
54 2lt3 12386 . . . . . . . . . . . . . 14 2 < 3
5547, 17, 1, 53, 54ndvdsi 16357 . . . . . . . . . . . . 13 ¬ 3 ∥ 14
56 3prm 16633 . . . . . . . . . . . . . 14 3 ∈ ℙ
57 coprm 16650 . . . . . . . . . . . . . 14 ((3 ∈ ℙ ∧ 14 ∈ ℤ) → (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1))
5856, 43, 57mp2an 690 . . . . . . . . . . . . 13 (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1)
5955, 58mpbi 229 . . . . . . . . . . . 12 (3 gcd 14) = 1
6046, 59eqtri 2760 . . . . . . . . . . 11 (14 gcd 3) = 1
61 eqid 2732 . . . . . . . . . . . 12 14 = 14
6211dec0h 12701 . . . . . . . . . . . 12 3 = 03
63 2t1e2 12377 . . . . . . . . . . . . . 14 (2 · 1) = 2
6463, 24oveq12i 7423 . . . . . . . . . . . . 13 ((2 · 1) + (0 + 1)) = (2 + 1)
65 2p1e3 12356 . . . . . . . . . . . . 13 (2 + 1) = 3
6664, 65eqtri 2760 . . . . . . . . . . . 12 ((2 · 1) + (0 + 1)) = 3
67 2cn 12289 . . . . . . . . . . . . . . 15 2 ∈ ℂ
68 4t2e8 12382 . . . . . . . . . . . . . . 15 (4 · 2) = 8
6948, 67, 68mulcomli 11225 . . . . . . . . . . . . . 14 (2 · 4) = 8
7069oveq1i 7421 . . . . . . . . . . . . 13 ((2 · 4) + 3) = (8 + 3)
71 8p3e11 12760 . . . . . . . . . . . . 13 (8 + 3) = 11
7270, 71eqtri 2760 . . . . . . . . . . . 12 ((2 · 4) + 3) = 11
7313, 17, 3, 11, 61, 62, 10, 13, 13, 66, 72decma2c 12732 . . . . . . . . . . 11 ((2 · 14) + 3) = 31
7410, 11, 42, 60, 73gcdi 17008 . . . . . . . . . 10 (31 gcd 14) = 1
75 eqid 2732 . . . . . . . . . . 11 31 = 31
7649mullidi 11221 . . . . . . . . . . . . 13 (1 · 3) = 3
77 ax-1cn 11170 . . . . . . . . . . . . . 14 1 ∈ ℂ
7877addridi 11403 . . . . . . . . . . . . 13 (1 + 0) = 1
7976, 78oveq12i 7423 . . . . . . . . . . . 12 ((1 · 3) + (1 + 0)) = (3 + 1)
80 3p1e4 12359 . . . . . . . . . . . 12 (3 + 1) = 4
8179, 80eqtri 2760 . . . . . . . . . . 11 ((1 · 3) + (1 + 0)) = 4
82 1t1e1 12376 . . . . . . . . . . . . 13 (1 · 1) = 1
8382oveq1i 7421 . . . . . . . . . . . 12 ((1 · 1) + 4) = (1 + 4)
84 4p1e5 12360 . . . . . . . . . . . . 13 (4 + 1) = 5
8548, 77, 84addcomli 11408 . . . . . . . . . . . 12 (1 + 4) = 5
8635dec0h 12701 . . . . . . . . . . . 12 5 = 05
8783, 85, 863eqtri 2764 . . . . . . . . . . 11 ((1 · 1) + 4) = 05
8811, 13, 13, 17, 75, 61, 13, 35, 3, 81, 87decma2c 12732 . . . . . . . . . 10 ((1 · 31) + 14) = 45
8913, 42, 41, 74, 88gcdi 17008 . . . . . . . . 9 (45 gcd 31) = 1
90 eqid 2732 . . . . . . . . . 10 45 = 45
9169, 80oveq12i 7423 . . . . . . . . . . 11 ((2 · 4) + (3 + 1)) = (8 + 4)
92 8p4e12 12761 . . . . . . . . . . 11 (8 + 4) = 12
9391, 92eqtri 2760 . . . . . . . . . 10 ((2 · 4) + (3 + 1)) = 12
94 5cn 12302 . . . . . . . . . . . 12 5 ∈ ℂ
95 5t2e10 12779 . . . . . . . . . . . 12 (5 · 2) = 10
9694, 67, 95mulcomli 11225 . . . . . . . . . . 11 (2 · 5) = 10
9713, 3, 24, 96decsuc 12710 . . . . . . . . . 10 ((2 · 5) + 1) = 11
9817, 35, 11, 13, 90, 75, 10, 13, 13, 93, 97decma2c 12732 . . . . . . . . 9 ((2 · 45) + 31) = 121
9910, 41, 36, 89, 98gcdi 17008 . . . . . . . 8 (121 gcd 45) = 1
100 eqid 2732 . . . . . . . . 9 121 = 121
101 eqid 2732 . . . . . . . . . 10 12 = 12
10248addridi 11403 . . . . . . . . . . 11 (4 + 0) = 4
10317dec0h 12701 . . . . . . . . . . 11 4 = 04
104102, 103eqtri 2760 . . . . . . . . . 10 (4 + 0) = 04
105 00id 11391 . . . . . . . . . . . 12 (0 + 0) = 0
10682, 105oveq12i 7423 . . . . . . . . . . 11 ((1 · 1) + (0 + 0)) = (1 + 0)
107106, 78eqtri 2760 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = 1
10867mullidi 11221 . . . . . . . . . . . 12 (1 · 2) = 2
109108oveq1i 7421 . . . . . . . . . . 11 ((1 · 2) + 4) = (2 + 4)
110 4p2e6 12367 . . . . . . . . . . . 12 (4 + 2) = 6
11148, 67, 110addcomli 11408 . . . . . . . . . . 11 (2 + 4) = 6
11228dec0h 12701 . . . . . . . . . . 11 6 = 06
113109, 111, 1123eqtri 2764 . . . . . . . . . 10 ((1 · 2) + 4) = 06
11413, 10, 3, 17, 101, 104, 13, 28, 3, 107, 113decma2c 12732 . . . . . . . . 9 ((1 · 12) + (4 + 0)) = 16
11582oveq1i 7421 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
116 5p1e6 12361 . . . . . . . . . . 11 (5 + 1) = 6
11794, 77, 116addcomli 11408 . . . . . . . . . 10 (1 + 5) = 6
118115, 117, 1123eqtri 2764 . . . . . . . . 9 ((1 · 1) + 5) = 06
11939, 13, 17, 35, 100, 90, 13, 28, 3, 114, 118decma2c 12732 . . . . . . . 8 ((1 · 121) + 45) = 166
12013, 36, 40, 99, 119gcdi 17008 . . . . . . 7 (166 gcd 121) = 1
121 eqid 2732 . . . . . . . 8 166 = 166
122 eqid 2732 . . . . . . . . 9 16 = 16
12313, 10, 65, 101decsuc 12710 . . . . . . . . 9 (12 + 1) = 13
124 1p1e2 12339 . . . . . . . . . . 11 (1 + 1) = 2
12563, 124oveq12i 7423 . . . . . . . . . 10 ((2 · 1) + (1 + 1)) = (2 + 2)
126125, 52eqtri 2760 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = 4
127 6cn 12305 . . . . . . . . . . 11 6 ∈ ℂ
128 6t2e12 12783 . . . . . . . . . . 11 (6 · 2) = 12
129127, 67, 128mulcomli 11225 . . . . . . . . . 10 (2 · 6) = 12
130 3p2e5 12365 . . . . . . . . . . 11 (3 + 2) = 5
13149, 67, 130addcomli 11408 . . . . . . . . . 10 (2 + 3) = 5
13213, 10, 11, 129, 131decaddi 12739 . . . . . . . . 9 ((2 · 6) + 3) = 15
13313, 28, 13, 11, 122, 123, 10, 35, 13, 126, 132decma2c 12732 . . . . . . . 8 ((2 · 16) + (12 + 1)) = 45
13413, 10, 65, 129decsuc 12710 . . . . . . . 8 ((2 · 6) + 1) = 13
13529, 28, 39, 13, 121, 100, 10, 11, 13, 133, 134decma2c 12732 . . . . . . 7 ((2 · 166) + 121) = 453
13610, 40, 38, 120, 135gcdi 17008 . . . . . 6 (453 gcd 166) = 1
137 eqid 2732 . . . . . . 7 453 = 453
13829nn0cni 12486 . . . . . . . . 9 16 ∈ ℂ
139138addridi 11403 . . . . . . . 8 (16 + 0) = 16
14048mullidi 11221 . . . . . . . . . 10 (1 · 4) = 4
141140, 124oveq12i 7423 . . . . . . . . 9 ((1 · 4) + (1 + 1)) = (4 + 2)
142141, 110eqtri 2760 . . . . . . . 8 ((1 · 4) + (1 + 1)) = 6
14394mullidi 11221 . . . . . . . . . 10 (1 · 5) = 5
144143oveq1i 7421 . . . . . . . . 9 ((1 · 5) + 6) = (5 + 6)
145 6p5e11 12752 . . . . . . . . . 10 (6 + 5) = 11
146127, 94, 145addcomli 11408 . . . . . . . . 9 (5 + 6) = 11
147144, 146eqtri 2760 . . . . . . . 8 ((1 · 5) + 6) = 11
14817, 35, 13, 28, 90, 139, 13, 13, 13, 142, 147decma2c 12732 . . . . . . 7 ((1 · 45) + (16 + 0)) = 61
14976oveq1i 7421 . . . . . . . 8 ((1 · 3) + 6) = (3 + 6)
150 6p3e9 12374 . . . . . . . . 9 (6 + 3) = 9
151127, 49, 150addcomli 11408 . . . . . . . 8 (3 + 6) = 9
15230dec0h 12701 . . . . . . . 8 9 = 09
153149, 151, 1523eqtri 2764 . . . . . . 7 ((1 · 3) + 6) = 09
15436, 11, 29, 28, 137, 121, 13, 30, 3, 148, 153decma2c 12732 . . . . . 6 ((1 · 453) + 166) = 619
15513, 38, 37, 136, 154gcdi 17008 . . . . 5 (619 gcd 453) = 1
156 eqid 2732 . . . . . 6 619 = 619
157 7nn0 12496 . . . . . . 7 7 ∈ ℕ0
158 eqid 2732 . . . . . . 7 61 = 61
159 5p2e7 12370 . . . . . . . 8 (5 + 2) = 7
16017, 35, 10, 90, 159decaddi 12739 . . . . . . 7 (45 + 2) = 47
161102oveq2i 7422 . . . . . . . 8 ((2 · 6) + (4 + 0)) = ((2 · 6) + 4)
16213, 10, 17, 129, 111decaddi 12739 . . . . . . . 8 ((2 · 6) + 4) = 16
163161, 162eqtri 2760 . . . . . . 7 ((2 · 6) + (4 + 0)) = 16
16463oveq1i 7421 . . . . . . . 8 ((2 · 1) + 7) = (2 + 7)
165 7cn 12308 . . . . . . . . 9 7 ∈ ℂ
166 7p2e9 12375 . . . . . . . . 9 (7 + 2) = 9
167165, 67, 166addcomli 11408 . . . . . . . 8 (2 + 7) = 9
168164, 167, 1523eqtri 2764 . . . . . . 7 ((2 · 1) + 7) = 09
16928, 13, 17, 157, 158, 160, 10, 30, 3, 163, 168decma2c 12732 . . . . . 6 ((2 · 61) + (45 + 2)) = 169
170 9cn 12314 . . . . . . . 8 9 ∈ ℂ
171 9t2e18 12801 . . . . . . . 8 (9 · 2) = 18
172170, 67, 171mulcomli 11225 . . . . . . 7 (2 · 9) = 18
17313, 2, 11, 172, 124, 13, 71decaddci 12740 . . . . . 6 ((2 · 9) + 3) = 21
17433, 30, 36, 11, 156, 137, 10, 13, 10, 169, 173decma2c 12732 . . . . 5 ((2 · 619) + 453) = 1691
17510, 37, 34, 155, 174gcdi 17008 . . . 4 (1691 gcd 619) = 1
176 eqid 2732 . . . . 5 1691 = 1691
177 eqid 2732 . . . . . 6 169 = 169
17828, 13, 124, 158decsuc 12710 . . . . . 6 (61 + 1) = 62
179 6p1e7 12362 . . . . . . . 8 (6 + 1) = 7
180157dec0h 12701 . . . . . . . 8 7 = 07
181179, 180eqtri 2760 . . . . . . 7 (6 + 1) = 07
18282, 24oveq12i 7423 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
183182, 124eqtri 2760 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
184127mullidi 11221 . . . . . . . . 9 (1 · 6) = 6
185184oveq1i 7421 . . . . . . . 8 ((1 · 6) + 7) = (6 + 7)
186 7p6e13 12757 . . . . . . . . 9 (7 + 6) = 13
187165, 127, 186addcomli 11408 . . . . . . . 8 (6 + 7) = 13
188185, 187eqtri 2760 . . . . . . 7 ((1 · 6) + 7) = 13
18913, 28, 3, 157, 122, 181, 13, 11, 13, 183, 188decma2c 12732 . . . . . 6 ((1 · 16) + (6 + 1)) = 23
190170mullidi 11221 . . . . . . . 8 (1 · 9) = 9
191190oveq1i 7421 . . . . . . 7 ((1 · 9) + 2) = (9 + 2)
192 9p2e11 12766 . . . . . . 7 (9 + 2) = 11
193191, 192eqtri 2760 . . . . . 6 ((1 · 9) + 2) = 11
19429, 30, 28, 10, 177, 178, 13, 13, 13, 189, 193decma2c 12732 . . . . 5 ((1 · 169) + (61 + 1)) = 231
19582oveq1i 7421 . . . . . 6 ((1 · 1) + 9) = (1 + 9)
196 9p1e10 12681 . . . . . . 7 (9 + 1) = 10
197170, 77, 196addcomli 11408 . . . . . 6 (1 + 9) = 10
198195, 197eqtri 2760 . . . . 5 ((1 · 1) + 9) = 10
19931, 13, 33, 30, 176, 156, 13, 3, 13, 194, 198decma2c 12732 . . . 4 ((1 · 1691) + 619) = 2310
20013, 34, 32, 175, 199gcdi 17008 . . 3 (2310 gcd 1691) = 1
201 eqid 2732 . . . . . 6 231 = 231
20231nn0cni 12486 . . . . . . 7 169 ∈ ℂ
203202addridi 11403 . . . . . 6 (169 + 0) = 169
204 eqid 2732 . . . . . . 7 23 = 23
20513, 28, 179, 122decsuc 12710 . . . . . . 7 (16 + 1) = 17
206108, 124oveq12i 7423 . . . . . . . 8 ((1 · 2) + (1 + 1)) = (2 + 2)
207206, 52eqtri 2760 . . . . . . 7 ((1 · 2) + (1 + 1)) = 4
20876oveq1i 7421 . . . . . . . 8 ((1 · 3) + 7) = (3 + 7)
209 7p3e10 12754 . . . . . . . . 9 (7 + 3) = 10
210165, 49, 209addcomli 11408 . . . . . . . 8 (3 + 7) = 10
211208, 210eqtri 2760 . . . . . . 7 ((1 · 3) + 7) = 10
21210, 11, 13, 157, 204, 205, 13, 3, 13, 207, 211decma2c 12732 . . . . . 6 ((1 · 23) + (16 + 1)) = 40
21312, 13, 29, 30, 201, 203, 13, 3, 13, 212, 198decma2c 12732 . . . . 5 ((1 · 231) + (169 + 0)) = 400
21477mul01i 11406 . . . . . . 7 (1 · 0) = 0
215214oveq1i 7421 . . . . . 6 ((1 · 0) + 1) = (0 + 1)
21613dec0h 12701 . . . . . 6 1 = 01
217215, 24, 2163eqtri 2764 . . . . 5 ((1 · 0) + 1) = 01
21814, 3, 31, 13, 25, 176, 13, 13, 3, 213, 217decma2c 12732 . . . 4 ((1 · 2310) + 1691) = 4001
219218, 16eqtr4i 2763 . . 3 ((1 · 2310) + 1691) = 𝑁
22013, 32, 15, 200, 219gcdi 17008 . 2 (𝑁 gcd 2310) = 1
2219, 15, 22, 27, 220gcdmodi 17009 1 (((2↑800) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205   = wceq 1541  wcel 2106   class class class wbr 5148  (class class class)co 7411  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117  cmin 11446  cn 12214  2c2 12269  3c3 12270  4c4 12271  5c5 12272  6c6 12273  7c7 12274  8c8 12275  9c9 12276  0cn0 12474  cz 12560  cdc 12679  cexp 14029  cdvds 16199   gcd cgcd 16437  cprime 16610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-rp 12977  df-fz 13487  df-fl 13759  df-mod 13837  df-seq 13969  df-exp 14030  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-dvds 16200  df-gcd 16438  df-prm 16611
This theorem is referenced by:  4001prm  17080
  Copyright terms: Public domain W3C validator