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

Theorem 4001lem4 16059
Description: Lemma for 4001prm 16060. 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 11388 . . . 4 2 ∈ ℕ
2 8nn0 11518 . . . . . 6 8 ∈ ℕ0
3 0nn0 11510 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11715 . . . . 5 80 ∈ ℕ0
54, 3deccl 11715 . . . 4 800 ∈ ℕ0
6 nnexpcl 13081 . . . 4 ((2 ∈ ℕ ∧ 800 ∈ ℕ0) → (2↑800) ∈ ℕ)
71, 5, 6mp2an 666 . . 3 (2↑800) ∈ ℕ
8 nnm1nn0 11537 . . 3 ((2↑800) ∈ ℕ → ((2↑800) − 1) ∈ ℕ0)
97, 8ax-mp 5 . 2 ((2↑800) − 1) ∈ ℕ0
10 2nn0 11512 . . . . 5 2 ∈ ℕ0
11 3nn0 11513 . . . . 5 3 ∈ ℕ0
1210, 11deccl 11715 . . . 4 23 ∈ ℕ0
13 1nn0 11511 . . . 4 1 ∈ ℕ0
1412, 13deccl 11715 . . 3 231 ∈ ℕ0
1514, 3deccl 11715 . 2 2310 ∈ ℕ0
16 4001prm.1 . . 3 𝑁 = 4001
17 4nn0 11514 . . . . . 6 4 ∈ ℕ0
1817, 3deccl 11715 . . . . 5 40 ∈ ℕ0
1918, 3deccl 11715 . . . 4 400 ∈ ℕ0
20 1nn 11234 . . . 4 1 ∈ ℕ
2119, 20decnncl 11721 . . 3 4001 ∈ ℕ
2216, 21eqeltri 2846 . 2 𝑁 ∈ ℕ
23164001lem2 16057 . . 3 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
24 0p1e1 11335 . . . 4 (0 + 1) = 1
25 eqid 2771 . . . 4 2310 = 2310
2614, 3, 24, 25decsuc 11738 . . 3 (2310 + 1) = 2311
2722, 7, 13, 15, 23, 26modsubi 15984 . 2 (((2↑800) − 1) mod 𝑁) = (2310 mod 𝑁)
28 6nn0 11516 . . . . . 6 6 ∈ ℕ0
2913, 28deccl 11715 . . . . 5 16 ∈ ℕ0
30 9nn0 11519 . . . . 5 9 ∈ ℕ0
3129, 30deccl 11715 . . . 4 169 ∈ ℕ0
3231, 13deccl 11715 . . 3 1691 ∈ ℕ0
3328, 13deccl 11715 . . . . 5 61 ∈ ℕ0
3433, 30deccl 11715 . . . 4 619 ∈ ℕ0
35 5nn0 11515 . . . . . . 7 5 ∈ ℕ0
3617, 35deccl 11715 . . . . . 6 45 ∈ ℕ0
3736, 11deccl 11715 . . . . 5 453 ∈ ℕ0
3829, 28deccl 11715 . . . . . 6 166 ∈ ℕ0
3913, 10deccl 11715 . . . . . . . 8 12 ∈ ℕ0
4039, 13deccl 11715 . . . . . . 7 121 ∈ ℕ0
4111, 13deccl 11715 . . . . . . . . 9 31 ∈ ℕ0
4213, 17deccl 11715 . . . . . . . . . 10 14 ∈ ℕ0
4342nn0zi 11605 . . . . . . . . . . . . 13 14 ∈ ℤ
4411nn0zi 11605 . . . . . . . . . . . . 13 3 ∈ ℤ
45 gcdcom 15444 . . . . . . . . . . . . 13 ((14 ∈ ℤ ∧ 3 ∈ ℤ) → (14 gcd 3) = (3 gcd 14))
4643, 44, 45mp2an 666 . . . . . . . . . . . 12 (14 gcd 3) = (3 gcd 14)
47 3nn 11389 . . . . . . . . . . . . . 14 3 ∈ ℕ
48 4cn 11301 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
49 3cn 11298 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
50 4t3e12 11834 . . . . . . . . . . . . . . . 16 (4 · 3) = 12
5148, 49, 50mulcomli 10250 . . . . . . . . . . . . . . 15 (3 · 4) = 12
52 2p2e4 11347 . . . . . . . . . . . . . . 15 (2 + 2) = 4
5313, 10, 10, 51, 52decaddi 11781 . . . . . . . . . . . . . 14 ((3 · 4) + 2) = 14
54 2lt3 11398 . . . . . . . . . . . . . 14 2 < 3
5547, 17, 1, 53, 54ndvdsi 15345 . . . . . . . . . . . . 13 ¬ 3 ∥ 14
56 3prm 15614 . . . . . . . . . . . . . 14 3 ∈ ℙ
57 coprm 15631 . . . . . . . . . . . . . 14 ((3 ∈ ℙ ∧ 14 ∈ ℤ) → (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1))
5856, 43, 57mp2an 666 . . . . . . . . . . . . 13 (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1)
5955, 58mpbi 220 . . . . . . . . . . . 12 (3 gcd 14) = 1
6046, 59eqtri 2793 . . . . . . . . . . 11 (14 gcd 3) = 1
61 eqid 2771 . . . . . . . . . . . 12 14 = 14
6211dec0h 11725 . . . . . . . . . . . 12 3 = 03
63 2t1e2 11379 . . . . . . . . . . . . . 14 (2 · 1) = 2
6463, 24oveq12i 6806 . . . . . . . . . . . . 13 ((2 · 1) + (0 + 1)) = (2 + 1)
65 2p1e3 11354 . . . . . . . . . . . . 13 (2 + 1) = 3
6664, 65eqtri 2793 . . . . . . . . . . . 12 ((2 · 1) + (0 + 1)) = 3
67 2cn 11294 . . . . . . . . . . . . . . 15 2 ∈ ℂ
68 4t2e8 11384 . . . . . . . . . . . . . . 15 (4 · 2) = 8
6948, 67, 68mulcomli 10250 . . . . . . . . . . . . . 14 (2 · 4) = 8
7069oveq1i 6804 . . . . . . . . . . . . 13 ((2 · 4) + 3) = (8 + 3)
71 8p3e11 11814 . . . . . . . . . . . . 13 (8 + 3) = 11
7270, 71eqtri 2793 . . . . . . . . . . . 12 ((2 · 4) + 3) = 11
7313, 17, 3, 11, 61, 62, 10, 13, 13, 66, 72decma2c 11770 . . . . . . . . . . 11 ((2 · 14) + 3) = 31
7410, 11, 42, 60, 73gcdi 15985 . . . . . . . . . 10 (31 gcd 14) = 1
75 eqid 2771 . . . . . . . . . . 11 31 = 31
7649mulid2i 10246 . . . . . . . . . . . . 13 (1 · 3) = 3
77 ax-1cn 10197 . . . . . . . . . . . . . 14 1 ∈ ℂ
7877addid1i 10426 . . . . . . . . . . . . 13 (1 + 0) = 1
7976, 78oveq12i 6806 . . . . . . . . . . . 12 ((1 · 3) + (1 + 0)) = (3 + 1)
80 3p1e4 11356 . . . . . . . . . . . 12 (3 + 1) = 4
8179, 80eqtri 2793 . . . . . . . . . . 11 ((1 · 3) + (1 + 0)) = 4
82 1t1e1 11378 . . . . . . . . . . . . 13 (1 · 1) = 1
8382oveq1i 6804 . . . . . . . . . . . 12 ((1 · 1) + 4) = (1 + 4)
84 4p1e5 11357 . . . . . . . . . . . . 13 (4 + 1) = 5
8548, 77, 84addcomli 10431 . . . . . . . . . . . 12 (1 + 4) = 5
8635dec0h 11725 . . . . . . . . . . . 12 5 = 05
8783, 85, 863eqtri 2797 . . . . . . . . . . 11 ((1 · 1) + 4) = 05
8811, 13, 13, 17, 75, 61, 13, 35, 3, 81, 87decma2c 11770 . . . . . . . . . 10 ((1 · 31) + 14) = 45
8913, 42, 41, 74, 88gcdi 15985 . . . . . . . . 9 (45 gcd 31) = 1
90 eqid 2771 . . . . . . . . . 10 45 = 45
9169, 80oveq12i 6806 . . . . . . . . . . 11 ((2 · 4) + (3 + 1)) = (8 + 4)
92 8p4e12 11816 . . . . . . . . . . 11 (8 + 4) = 12
9391, 92eqtri 2793 . . . . . . . . . 10 ((2 · 4) + (3 + 1)) = 12
94 5cn 11303 . . . . . . . . . . . 12 5 ∈ ℂ
95 5t2e10 11836 . . . . . . . . . . . 12 (5 · 2) = 10
9694, 67, 95mulcomli 10250 . . . . . . . . . . 11 (2 · 5) = 10
9713, 3, 24, 96decsuc 11738 . . . . . . . . . 10 ((2 · 5) + 1) = 11
9817, 35, 11, 13, 90, 75, 10, 13, 13, 93, 97decma2c 11770 . . . . . . . . 9 ((2 · 45) + 31) = 121
9910, 41, 36, 89, 98gcdi 15985 . . . . . . . 8 (121 gcd 45) = 1
100 eqid 2771 . . . . . . . . 9 121 = 121
101 eqid 2771 . . . . . . . . . 10 12 = 12
10248addid1i 10426 . . . . . . . . . . 11 (4 + 0) = 4
10317dec0h 11725 . . . . . . . . . . 11 4 = 04
104102, 103eqtri 2793 . . . . . . . . . 10 (4 + 0) = 04
105 00id 10414 . . . . . . . . . . . 12 (0 + 0) = 0
10682, 105oveq12i 6806 . . . . . . . . . . 11 ((1 · 1) + (0 + 0)) = (1 + 0)
107106, 78eqtri 2793 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = 1
10867mulid2i 10246 . . . . . . . . . . . 12 (1 · 2) = 2
109108oveq1i 6804 . . . . . . . . . . 11 ((1 · 2) + 4) = (2 + 4)
110 4p2e6 11365 . . . . . . . . . . . 12 (4 + 2) = 6
11148, 67, 110addcomli 10431 . . . . . . . . . . 11 (2 + 4) = 6
11228dec0h 11725 . . . . . . . . . . 11 6 = 06
113109, 111, 1123eqtri 2797 . . . . . . . . . 10 ((1 · 2) + 4) = 06
11413, 10, 3, 17, 101, 104, 13, 28, 3, 107, 113decma2c 11770 . . . . . . . . 9 ((1 · 12) + (4 + 0)) = 16
11582oveq1i 6804 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
116 5p1e6 11358 . . . . . . . . . . 11 (5 + 1) = 6
11794, 77, 116addcomli 10431 . . . . . . . . . 10 (1 + 5) = 6
118115, 117, 1123eqtri 2797 . . . . . . . . 9 ((1 · 1) + 5) = 06
11939, 13, 17, 35, 100, 90, 13, 28, 3, 114, 118decma2c 11770 . . . . . . . 8 ((1 · 121) + 45) = 166
12013, 36, 40, 99, 119gcdi 15985 . . . . . . 7 (166 gcd 121) = 1
121 eqid 2771 . . . . . . . 8 166 = 166
122 eqid 2771 . . . . . . . . 9 16 = 16
12313, 10, 65, 101decsuc 11738 . . . . . . . . 9 (12 + 1) = 13
124 1p1e2 11337 . . . . . . . . . . 11 (1 + 1) = 2
12563, 124oveq12i 6806 . . . . . . . . . 10 ((2 · 1) + (1 + 1)) = (2 + 2)
126125, 52eqtri 2793 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = 4
127 6cn 11305 . . . . . . . . . . 11 6 ∈ ℂ
128 6t2e12 11843 . . . . . . . . . . 11 (6 · 2) = 12
129127, 67, 128mulcomli 10250 . . . . . . . . . 10 (2 · 6) = 12
130 3p2e5 11363 . . . . . . . . . . 11 (3 + 2) = 5
13149, 67, 130addcomli 10431 . . . . . . . . . 10 (2 + 3) = 5
13213, 10, 11, 129, 131decaddi 11781 . . . . . . . . 9 ((2 · 6) + 3) = 15
13313, 28, 13, 11, 122, 123, 10, 35, 13, 126, 132decma2c 11770 . . . . . . . 8 ((2 · 16) + (12 + 1)) = 45
13413, 10, 65, 129decsuc 11738 . . . . . . . 8 ((2 · 6) + 1) = 13
13529, 28, 39, 13, 121, 100, 10, 11, 13, 133, 134decma2c 11770 . . . . . . 7 ((2 · 166) + 121) = 453
13610, 40, 38, 120, 135gcdi 15985 . . . . . 6 (453 gcd 166) = 1
137 eqid 2771 . . . . . . 7 453 = 453
13829nn0cni 11507 . . . . . . . . 9 16 ∈ ℂ
139138addid1i 10426 . . . . . . . 8 (16 + 0) = 16
14048mulid2i 10246 . . . . . . . . . 10 (1 · 4) = 4
141140, 124oveq12i 6806 . . . . . . . . 9 ((1 · 4) + (1 + 1)) = (4 + 2)
142141, 110eqtri 2793 . . . . . . . 8 ((1 · 4) + (1 + 1)) = 6
14394mulid2i 10246 . . . . . . . . . 10 (1 · 5) = 5
144143oveq1i 6804 . . . . . . . . 9 ((1 · 5) + 6) = (5 + 6)
145 6p5e11 11802 . . . . . . . . . 10 (6 + 5) = 11
146127, 94, 145addcomli 10431 . . . . . . . . 9 (5 + 6) = 11
147144, 146eqtri 2793 . . . . . . . 8 ((1 · 5) + 6) = 11
14817, 35, 13, 28, 90, 139, 13, 13, 13, 142, 147decma2c 11770 . . . . . . 7 ((1 · 45) + (16 + 0)) = 61
14976oveq1i 6804 . . . . . . . 8 ((1 · 3) + 6) = (3 + 6)
150 6p3e9 11373 . . . . . . . . 9 (6 + 3) = 9
151127, 49, 150addcomli 10431 . . . . . . . 8 (3 + 6) = 9
15230dec0h 11725 . . . . . . . 8 9 = 09
153149, 151, 1523eqtri 2797 . . . . . . 7 ((1 · 3) + 6) = 09
15436, 11, 29, 28, 137, 121, 13, 30, 3, 148, 153decma2c 11770 . . . . . 6 ((1 · 453) + 166) = 619
15513, 38, 37, 136, 154gcdi 15985 . . . . 5 (619 gcd 453) = 1
156 eqid 2771 . . . . . 6 619 = 619
157 7nn0 11517 . . . . . . 7 7 ∈ ℕ0
158 eqid 2771 . . . . . . 7 61 = 61
159 5p2e7 11368 . . . . . . . 8 (5 + 2) = 7
16017, 35, 10, 90, 159decaddi 11781 . . . . . . 7 (45 + 2) = 47
161102oveq2i 6805 . . . . . . . 8 ((2 · 6) + (4 + 0)) = ((2 · 6) + 4)
16213, 10, 17, 129, 111decaddi 11781 . . . . . . . 8 ((2 · 6) + 4) = 16
163161, 162eqtri 2793 . . . . . . 7 ((2 · 6) + (4 + 0)) = 16
16463oveq1i 6804 . . . . . . . 8 ((2 · 1) + 7) = (2 + 7)
165 7cn 11307 . . . . . . . . 9 7 ∈ ℂ
166 7p2e9 11375 . . . . . . . . 9 (7 + 2) = 9
167165, 67, 166addcomli 10431 . . . . . . . 8 (2 + 7) = 9
168164, 167, 1523eqtri 2797 . . . . . . 7 ((2 · 1) + 7) = 09
16928, 13, 17, 157, 158, 160, 10, 30, 3, 163, 168decma2c 11770 . . . . . 6 ((2 · 61) + (45 + 2)) = 169
170 9cn 11311 . . . . . . . 8 9 ∈ ℂ
171 9t2e18 11865 . . . . . . . 8 (9 · 2) = 18
172170, 67, 171mulcomli 10250 . . . . . . 7 (2 · 9) = 18
17313, 2, 11, 172, 124, 13, 71decaddci 11782 . . . . . 6 ((2 · 9) + 3) = 21
17433, 30, 36, 11, 156, 137, 10, 13, 10, 169, 173decma2c 11770 . . . . 5 ((2 · 619) + 453) = 1691
17510, 37, 34, 155, 174gcdi 15985 . . . 4 (1691 gcd 619) = 1
176 eqid 2771 . . . . 5 1691 = 1691
177 eqid 2771 . . . . . 6 169 = 169
17828, 13, 124, 158decsuc 11738 . . . . . 6 (61 + 1) = 62
179 6p1e7 11359 . . . . . . . 8 (6 + 1) = 7
180157dec0h 11725 . . . . . . . 8 7 = 07
181179, 180eqtri 2793 . . . . . . 7 (6 + 1) = 07
18282, 24oveq12i 6806 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
183182, 124eqtri 2793 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
184127mulid2i 10246 . . . . . . . . 9 (1 · 6) = 6
185184oveq1i 6804 . . . . . . . 8 ((1 · 6) + 7) = (6 + 7)
186 7p6e13 11810 . . . . . . . . 9 (7 + 6) = 13
187165, 127, 186addcomli 10431 . . . . . . . 8 (6 + 7) = 13
188185, 187eqtri 2793 . . . . . . 7 ((1 · 6) + 7) = 13
18913, 28, 3, 157, 122, 181, 13, 11, 13, 183, 188decma2c 11770 . . . . . 6 ((1 · 16) + (6 + 1)) = 23
190170mulid2i 10246 . . . . . . . 8 (1 · 9) = 9
191190oveq1i 6804 . . . . . . 7 ((1 · 9) + 2) = (9 + 2)
192 9p2e11 11821 . . . . . . 7 (9 + 2) = 11
193191, 192eqtri 2793 . . . . . 6 ((1 · 9) + 2) = 11
19429, 30, 28, 10, 177, 178, 13, 13, 13, 189, 193decma2c 11770 . . . . 5 ((1 · 169) + (61 + 1)) = 231
19582oveq1i 6804 . . . . . 6 ((1 · 1) + 9) = (1 + 9)
196 9p1e10 11699 . . . . . . 7 (9 + 1) = 10
197170, 77, 196addcomli 10431 . . . . . 6 (1 + 9) = 10
198195, 197eqtri 2793 . . . . 5 ((1 · 1) + 9) = 10
19931, 13, 33, 30, 176, 156, 13, 3, 13, 194, 198decma2c 11770 . . . 4 ((1 · 1691) + 619) = 2310
20013, 34, 32, 175, 199gcdi 15985 . . 3 (2310 gcd 1691) = 1
201 eqid 2771 . . . . . 6 231 = 231
20231nn0cni 11507 . . . . . . 7 169 ∈ ℂ
203202addid1i 10426 . . . . . 6 (169 + 0) = 169
204 eqid 2771 . . . . . . 7 23 = 23
20513, 28, 179, 122decsuc 11738 . . . . . . 7 (16 + 1) = 17
206108, 124oveq12i 6806 . . . . . . . 8 ((1 · 2) + (1 + 1)) = (2 + 2)
207206, 52eqtri 2793 . . . . . . 7 ((1 · 2) + (1 + 1)) = 4
20876oveq1i 6804 . . . . . . . 8 ((1 · 3) + 7) = (3 + 7)
209 7p3e10 11805 . . . . . . . . 9 (7 + 3) = 10
210165, 49, 209addcomli 10431 . . . . . . . 8 (3 + 7) = 10
211208, 210eqtri 2793 . . . . . . 7 ((1 · 3) + 7) = 10
21210, 11, 13, 157, 204, 205, 13, 3, 13, 207, 211decma2c 11770 . . . . . 6 ((1 · 23) + (16 + 1)) = 40
21312, 13, 29, 30, 201, 203, 13, 3, 13, 212, 198decma2c 11770 . . . . 5 ((1 · 231) + (169 + 0)) = 400
21477mul01i 10429 . . . . . . 7 (1 · 0) = 0
215214oveq1i 6804 . . . . . 6 ((1 · 0) + 1) = (0 + 1)
21613dec0h 11725 . . . . . 6 1 = 01
217215, 24, 2163eqtri 2797 . . . . 5 ((1 · 0) + 1) = 01
21814, 3, 31, 13, 25, 176, 13, 13, 3, 213, 217decma2c 11770 . . . 4 ((1 · 2310) + 1691) = 4001
219218, 16eqtr4i 2796 . . 3 ((1 · 2310) + 1691) = 𝑁
22013, 32, 15, 200, 219gcdi 15985 . 2 (𝑁 gcd 2310) = 1
2219, 15, 22, 27, 220gcdmodi 15986 1 (((2↑800) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196   = wceq 1631  wcel 2145   class class class wbr 4787  (class class class)co 6794  0cc0 10139  1c1 10140   + caddc 10142   · cmul 10144  cmin 10469  cn 11223  2c2 11273  3c3 11274  4c4 11275  5c5 11276  6c6 11277  7c7 11278  8c8 11279  9c9 11280  0cn0 11495  cz 11580  cdc 11696  cexp 13068  cdvds 15190   gcd cgcd 15425  cprime 15593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-2o 7715  df-er 7897  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-sup 8505  df-inf 8506  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-rp 12037  df-fz 12535  df-fl 12802  df-mod 12878  df-seq 13010  df-exp 13069  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-dvds 15191  df-gcd 15426  df-prm 15594
This theorem is referenced by:  4001prm  16060
  Copyright terms: Public domain W3C validator