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

Theorem 4001lem4 16058
Description: Lemma for 4001prm 16059. 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 11458 . . . 4 2 ∈ ℕ
2 8nn0 11578 . . . . . 6 8 ∈ ℕ0
3 0nn0 11570 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11770 . . . . 5 80 ∈ ℕ0
54, 3deccl 11770 . . . 4 800 ∈ ℕ0
6 nnexpcl 13092 . . . 4 ((2 ∈ ℕ ∧ 800 ∈ ℕ0) → (2↑800) ∈ ℕ)
71, 5, 6mp2an 675 . . 3 (2↑800) ∈ ℕ
8 nnm1nn0 11596 . . 3 ((2↑800) ∈ ℕ → ((2↑800) − 1) ∈ ℕ0)
97, 8ax-mp 5 . 2 ((2↑800) − 1) ∈ ℕ0
10 2nn0 11572 . . . . 5 2 ∈ ℕ0
11 3nn0 11573 . . . . 5 3 ∈ ℕ0
1210, 11deccl 11770 . . . 4 23 ∈ ℕ0
13 1nn0 11571 . . . 4 1 ∈ ℕ0
1412, 13deccl 11770 . . 3 231 ∈ ℕ0
1514, 3deccl 11770 . 2 2310 ∈ ℕ0
16 4001prm.1 . . 3 𝑁 = 4001
17 4nn0 11574 . . . . . 6 4 ∈ ℕ0
1817, 3deccl 11770 . . . . 5 40 ∈ ℕ0
1918, 3deccl 11770 . . . 4 400 ∈ ℕ0
20 1nn 11312 . . . 4 1 ∈ ℕ
2119, 20decnncl 11775 . . 3 4001 ∈ ℕ
2216, 21eqeltri 2881 . 2 𝑁 ∈ ℕ
23164001lem2 16056 . . 3 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
24 0p1e1 11410 . . . 4 (0 + 1) = 1
25 eqid 2806 . . . 4 2310 = 2310
2614, 3, 24, 25decsuc 11786 . . 3 (2310 + 1) = 2311
2722, 7, 13, 15, 23, 26modsubi 15989 . 2 (((2↑800) − 1) mod 𝑁) = (2310 mod 𝑁)
28 6nn0 11576 . . . . . 6 6 ∈ ℕ0
2913, 28deccl 11770 . . . . 5 16 ∈ ℕ0
30 9nn0 11579 . . . . 5 9 ∈ ℕ0
3129, 30deccl 11770 . . . 4 169 ∈ ℕ0
3231, 13deccl 11770 . . 3 1691 ∈ ℕ0
3328, 13deccl 11770 . . . . 5 61 ∈ ℕ0
3433, 30deccl 11770 . . . 4 619 ∈ ℕ0
35 5nn0 11575 . . . . . . 7 5 ∈ ℕ0
3617, 35deccl 11770 . . . . . 6 45 ∈ ℕ0
3736, 11deccl 11770 . . . . 5 453 ∈ ℕ0
3829, 28deccl 11770 . . . . . 6 166 ∈ ℕ0
3913, 10deccl 11770 . . . . . . . 8 12 ∈ ℕ0
4039, 13deccl 11770 . . . . . . 7 121 ∈ ℕ0
4111, 13deccl 11770 . . . . . . . . 9 31 ∈ ℕ0
4213, 17deccl 11770 . . . . . . . . . 10 14 ∈ ℕ0
4342nn0zi 11664 . . . . . . . . . . . . 13 14 ∈ ℤ
4411nn0zi 11664 . . . . . . . . . . . . 13 3 ∈ ℤ
45 gcdcom 15450 . . . . . . . . . . . . 13 ((14 ∈ ℤ ∧ 3 ∈ ℤ) → (14 gcd 3) = (3 gcd 14))
4643, 44, 45mp2an 675 . . . . . . . . . . . 12 (14 gcd 3) = (3 gcd 14)
47 3nn 11459 . . . . . . . . . . . . . 14 3 ∈ ℕ
48 4cn 11378 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
49 3cn 11375 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
50 4t3e12 11853 . . . . . . . . . . . . . . . 16 (4 · 3) = 12
5148, 49, 50mulcomli 10330 . . . . . . . . . . . . . . 15 (3 · 4) = 12
52 2p2e4 11423 . . . . . . . . . . . . . . 15 (2 + 2) = 4
5313, 10, 10, 51, 52decaddi 11815 . . . . . . . . . . . . . 14 ((3 · 4) + 2) = 14
54 2lt3 11467 . . . . . . . . . . . . . 14 2 < 3
5547, 17, 1, 53, 54ndvdsi 15351 . . . . . . . . . . . . 13 ¬ 3 ∥ 14
56 3prm 15620 . . . . . . . . . . . . . 14 3 ∈ ℙ
57 coprm 15636 . . . . . . . . . . . . . 14 ((3 ∈ ℙ ∧ 14 ∈ ℤ) → (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1))
5856, 43, 57mp2an 675 . . . . . . . . . . . . 13 (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1)
5955, 58mpbi 221 . . . . . . . . . . . 12 (3 gcd 14) = 1
6046, 59eqtri 2828 . . . . . . . . . . 11 (14 gcd 3) = 1
61 eqid 2806 . . . . . . . . . . . 12 14 = 14
6211dec0h 11777 . . . . . . . . . . . 12 3 = 03
63 2t1e2 11450 . . . . . . . . . . . . . 14 (2 · 1) = 2
6463, 24oveq12i 6882 . . . . . . . . . . . . 13 ((2 · 1) + (0 + 1)) = (2 + 1)
65 2p1e3 11430 . . . . . . . . . . . . 13 (2 + 1) = 3
6664, 65eqtri 2828 . . . . . . . . . . . 12 ((2 · 1) + (0 + 1)) = 3
67 2cn 11371 . . . . . . . . . . . . . . 15 2 ∈ ℂ
68 4t2e8 11455 . . . . . . . . . . . . . . 15 (4 · 2) = 8
6948, 67, 68mulcomli 10330 . . . . . . . . . . . . . 14 (2 · 4) = 8
7069oveq1i 6880 . . . . . . . . . . . . 13 ((2 · 4) + 3) = (8 + 3)
71 8p3e11 11836 . . . . . . . . . . . . 13 (8 + 3) = 11
7270, 71eqtri 2828 . . . . . . . . . . . 12 ((2 · 4) + 3) = 11
7313, 17, 3, 11, 61, 62, 10, 13, 13, 66, 72decma2c 11808 . . . . . . . . . . 11 ((2 · 14) + 3) = 31
7410, 11, 42, 60, 73gcdi 15990 . . . . . . . . . 10 (31 gcd 14) = 1
75 eqid 2806 . . . . . . . . . . 11 31 = 31
7649mulid2i 10326 . . . . . . . . . . . . 13 (1 · 3) = 3
77 ax-1cn 10275 . . . . . . . . . . . . . 14 1 ∈ ℂ
7877addid1i 10504 . . . . . . . . . . . . 13 (1 + 0) = 1
7976, 78oveq12i 6882 . . . . . . . . . . . 12 ((1 · 3) + (1 + 0)) = (3 + 1)
80 3p1e4 11432 . . . . . . . . . . . 12 (3 + 1) = 4
8179, 80eqtri 2828 . . . . . . . . . . 11 ((1 · 3) + (1 + 0)) = 4
82 1t1e1 11449 . . . . . . . . . . . . 13 (1 · 1) = 1
8382oveq1i 6880 . . . . . . . . . . . 12 ((1 · 1) + 4) = (1 + 4)
84 4p1e5 11433 . . . . . . . . . . . . 13 (4 + 1) = 5
8548, 77, 84addcomli 10509 . . . . . . . . . . . 12 (1 + 4) = 5
8635dec0h 11777 . . . . . . . . . . . 12 5 = 05
8783, 85, 863eqtri 2832 . . . . . . . . . . 11 ((1 · 1) + 4) = 05
8811, 13, 13, 17, 75, 61, 13, 35, 3, 81, 87decma2c 11808 . . . . . . . . . 10 ((1 · 31) + 14) = 45
8913, 42, 41, 74, 88gcdi 15990 . . . . . . . . 9 (45 gcd 31) = 1
90 eqid 2806 . . . . . . . . . 10 45 = 45
9169, 80oveq12i 6882 . . . . . . . . . . 11 ((2 · 4) + (3 + 1)) = (8 + 4)
92 8p4e12 11837 . . . . . . . . . . 11 (8 + 4) = 12
9391, 92eqtri 2828 . . . . . . . . . 10 ((2 · 4) + (3 + 1)) = 12
94 5cn 11380 . . . . . . . . . . . 12 5 ∈ ℂ
95 5t2e10 11855 . . . . . . . . . . . 12 (5 · 2) = 10
9694, 67, 95mulcomli 10330 . . . . . . . . . . 11 (2 · 5) = 10
9713, 3, 24, 96decsuc 11786 . . . . . . . . . 10 ((2 · 5) + 1) = 11
9817, 35, 11, 13, 90, 75, 10, 13, 13, 93, 97decma2c 11808 . . . . . . . . 9 ((2 · 45) + 31) = 121
9910, 41, 36, 89, 98gcdi 15990 . . . . . . . 8 (121 gcd 45) = 1
100 eqid 2806 . . . . . . . . 9 121 = 121
101 eqid 2806 . . . . . . . . . 10 12 = 12
10248addid1i 10504 . . . . . . . . . . 11 (4 + 0) = 4
10317dec0h 11777 . . . . . . . . . . 11 4 = 04
104102, 103eqtri 2828 . . . . . . . . . 10 (4 + 0) = 04
105 00id 10492 . . . . . . . . . . . 12 (0 + 0) = 0
10682, 105oveq12i 6882 . . . . . . . . . . 11 ((1 · 1) + (0 + 0)) = (1 + 0)
107106, 78eqtri 2828 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = 1
10867mulid2i 10326 . . . . . . . . . . . 12 (1 · 2) = 2
109108oveq1i 6880 . . . . . . . . . . 11 ((1 · 2) + 4) = (2 + 4)
110 4p2e6 11440 . . . . . . . . . . . 12 (4 + 2) = 6
11148, 67, 110addcomli 10509 . . . . . . . . . . 11 (2 + 4) = 6
11228dec0h 11777 . . . . . . . . . . 11 6 = 06
113109, 111, 1123eqtri 2832 . . . . . . . . . 10 ((1 · 2) + 4) = 06
11413, 10, 3, 17, 101, 104, 13, 28, 3, 107, 113decma2c 11808 . . . . . . . . 9 ((1 · 12) + (4 + 0)) = 16
11582oveq1i 6880 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
116 5p1e6 11434 . . . . . . . . . . 11 (5 + 1) = 6
11794, 77, 116addcomli 10509 . . . . . . . . . 10 (1 + 5) = 6
118115, 117, 1123eqtri 2832 . . . . . . . . 9 ((1 · 1) + 5) = 06
11939, 13, 17, 35, 100, 90, 13, 28, 3, 114, 118decma2c 11808 . . . . . . . 8 ((1 · 121) + 45) = 166
12013, 36, 40, 99, 119gcdi 15990 . . . . . . 7 (166 gcd 121) = 1
121 eqid 2806 . . . . . . . 8 166 = 166
122 eqid 2806 . . . . . . . . 9 16 = 16
12313, 10, 65, 101decsuc 11786 . . . . . . . . 9 (12 + 1) = 13
124 1p1e2 11413 . . . . . . . . . . 11 (1 + 1) = 2
12563, 124oveq12i 6882 . . . . . . . . . 10 ((2 · 1) + (1 + 1)) = (2 + 2)
126125, 52eqtri 2828 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = 4
127 6cn 11382 . . . . . . . . . . 11 6 ∈ ℂ
128 6t2e12 11859 . . . . . . . . . . 11 (6 · 2) = 12
129127, 67, 128mulcomli 10330 . . . . . . . . . 10 (2 · 6) = 12
130 3p2e5 11438 . . . . . . . . . . 11 (3 + 2) = 5
13149, 67, 130addcomli 10509 . . . . . . . . . 10 (2 + 3) = 5
13213, 10, 11, 129, 131decaddi 11815 . . . . . . . . 9 ((2 · 6) + 3) = 15
13313, 28, 13, 11, 122, 123, 10, 35, 13, 126, 132decma2c 11808 . . . . . . . 8 ((2 · 16) + (12 + 1)) = 45
13413, 10, 65, 129decsuc 11786 . . . . . . . 8 ((2 · 6) + 1) = 13
13529, 28, 39, 13, 121, 100, 10, 11, 13, 133, 134decma2c 11808 . . . . . . 7 ((2 · 166) + 121) = 453
13610, 40, 38, 120, 135gcdi 15990 . . . . . 6 (453 gcd 166) = 1
137 eqid 2806 . . . . . . 7 453 = 453
13829nn0cni 11567 . . . . . . . . 9 16 ∈ ℂ
139138addid1i 10504 . . . . . . . 8 (16 + 0) = 16
14048mulid2i 10326 . . . . . . . . . 10 (1 · 4) = 4
141140, 124oveq12i 6882 . . . . . . . . 9 ((1 · 4) + (1 + 1)) = (4 + 2)
142141, 110eqtri 2828 . . . . . . . 8 ((1 · 4) + (1 + 1)) = 6
14394mulid2i 10326 . . . . . . . . . 10 (1 · 5) = 5
144143oveq1i 6880 . . . . . . . . 9 ((1 · 5) + 6) = (5 + 6)
145 6p5e11 11828 . . . . . . . . . 10 (6 + 5) = 11
146127, 94, 145addcomli 10509 . . . . . . . . 9 (5 + 6) = 11
147144, 146eqtri 2828 . . . . . . . 8 ((1 · 5) + 6) = 11
14817, 35, 13, 28, 90, 139, 13, 13, 13, 142, 147decma2c 11808 . . . . . . 7 ((1 · 45) + (16 + 0)) = 61
14976oveq1i 6880 . . . . . . . 8 ((1 · 3) + 6) = (3 + 6)
150 6p3e9 11447 . . . . . . . . 9 (6 + 3) = 9
151127, 49, 150addcomli 10509 . . . . . . . 8 (3 + 6) = 9
15230dec0h 11777 . . . . . . . 8 9 = 09
153149, 151, 1523eqtri 2832 . . . . . . 7 ((1 · 3) + 6) = 09
15436, 11, 29, 28, 137, 121, 13, 30, 3, 148, 153decma2c 11808 . . . . . 6 ((1 · 453) + 166) = 619
15513, 38, 37, 136, 154gcdi 15990 . . . . 5 (619 gcd 453) = 1
156 eqid 2806 . . . . . 6 619 = 619
157 7nn0 11577 . . . . . . 7 7 ∈ ℕ0
158 eqid 2806 . . . . . . 7 61 = 61
159 5p2e7 11443 . . . . . . . 8 (5 + 2) = 7
16017, 35, 10, 90, 159decaddi 11815 . . . . . . 7 (45 + 2) = 47
161102oveq2i 6881 . . . . . . . 8 ((2 · 6) + (4 + 0)) = ((2 · 6) + 4)
16213, 10, 17, 129, 111decaddi 11815 . . . . . . . 8 ((2 · 6) + 4) = 16
163161, 162eqtri 2828 . . . . . . 7 ((2 · 6) + (4 + 0)) = 16
16463oveq1i 6880 . . . . . . . 8 ((2 · 1) + 7) = (2 + 7)
165 7cn 11384 . . . . . . . . 9 7 ∈ ℂ
166 7p2e9 11448 . . . . . . . . 9 (7 + 2) = 9
167165, 67, 166addcomli 10509 . . . . . . . 8 (2 + 7) = 9
168164, 167, 1523eqtri 2832 . . . . . . 7 ((2 · 1) + 7) = 09
16928, 13, 17, 157, 158, 160, 10, 30, 3, 163, 168decma2c 11808 . . . . . 6 ((2 · 61) + (45 + 2)) = 169
170 9cn 11388 . . . . . . . 8 9 ∈ ℂ
171 9t2e18 11877 . . . . . . . 8 (9 · 2) = 18
172170, 67, 171mulcomli 10330 . . . . . . 7 (2 · 9) = 18
17313, 2, 11, 172, 124, 13, 71decaddci 11816 . . . . . 6 ((2 · 9) + 3) = 21
17433, 30, 36, 11, 156, 137, 10, 13, 10, 169, 173decma2c 11808 . . . . 5 ((2 · 619) + 453) = 1691
17510, 37, 34, 155, 174gcdi 15990 . . . 4 (1691 gcd 619) = 1
176 eqid 2806 . . . . 5 1691 = 1691
177 eqid 2806 . . . . . 6 169 = 169
17828, 13, 124, 158decsuc 11786 . . . . . 6 (61 + 1) = 62
179 6p1e7 11435 . . . . . . . 8 (6 + 1) = 7
180157dec0h 11777 . . . . . . . 8 7 = 07
181179, 180eqtri 2828 . . . . . . 7 (6 + 1) = 07
18282, 24oveq12i 6882 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
183182, 124eqtri 2828 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
184127mulid2i 10326 . . . . . . . . 9 (1 · 6) = 6
185184oveq1i 6880 . . . . . . . 8 ((1 · 6) + 7) = (6 + 7)
186 7p6e13 11833 . . . . . . . . 9 (7 + 6) = 13
187165, 127, 186addcomli 10509 . . . . . . . 8 (6 + 7) = 13
188185, 187eqtri 2828 . . . . . . 7 ((1 · 6) + 7) = 13
18913, 28, 3, 157, 122, 181, 13, 11, 13, 183, 188decma2c 11808 . . . . . 6 ((1 · 16) + (6 + 1)) = 23
190170mulid2i 10326 . . . . . . . 8 (1 · 9) = 9
191190oveq1i 6880 . . . . . . 7 ((1 · 9) + 2) = (9 + 2)
192 9p2e11 11842 . . . . . . 7 (9 + 2) = 11
193191, 192eqtri 2828 . . . . . 6 ((1 · 9) + 2) = 11
19429, 30, 28, 10, 177, 178, 13, 13, 13, 189, 193decma2c 11808 . . . . 5 ((1 · 169) + (61 + 1)) = 231
19582oveq1i 6880 . . . . . 6 ((1 · 1) + 9) = (1 + 9)
196 9p1e10 11757 . . . . . . 7 (9 + 1) = 10
197170, 77, 196addcomli 10509 . . . . . 6 (1 + 9) = 10
198195, 197eqtri 2828 . . . . 5 ((1 · 1) + 9) = 10
19931, 13, 33, 30, 176, 156, 13, 3, 13, 194, 198decma2c 11808 . . . 4 ((1 · 1691) + 619) = 2310
20013, 34, 32, 175, 199gcdi 15990 . . 3 (2310 gcd 1691) = 1
201 eqid 2806 . . . . . 6 231 = 231
20231nn0cni 11567 . . . . . . 7 169 ∈ ℂ
203202addid1i 10504 . . . . . 6 (169 + 0) = 169
204 eqid 2806 . . . . . . 7 23 = 23
20513, 28, 179, 122decsuc 11786 . . . . . . 7 (16 + 1) = 17
206108, 124oveq12i 6882 . . . . . . . 8 ((1 · 2) + (1 + 1)) = (2 + 2)
207206, 52eqtri 2828 . . . . . . 7 ((1 · 2) + (1 + 1)) = 4
20876oveq1i 6880 . . . . . . . 8 ((1 · 3) + 7) = (3 + 7)
209 7p3e10 11830 . . . . . . . . 9 (7 + 3) = 10
210165, 49, 209addcomli 10509 . . . . . . . 8 (3 + 7) = 10
211208, 210eqtri 2828 . . . . . . 7 ((1 · 3) + 7) = 10
21210, 11, 13, 157, 204, 205, 13, 3, 13, 207, 211decma2c 11808 . . . . . 6 ((1 · 23) + (16 + 1)) = 40
21312, 13, 29, 30, 201, 203, 13, 3, 13, 212, 198decma2c 11808 . . . . 5 ((1 · 231) + (169 + 0)) = 400
21477mul01i 10507 . . . . . . 7 (1 · 0) = 0
215214oveq1i 6880 . . . . . 6 ((1 · 0) + 1) = (0 + 1)
21613dec0h 11777 . . . . . 6 1 = 01
217215, 24, 2163eqtri 2832 . . . . 5 ((1 · 0) + 1) = 01
21814, 3, 31, 13, 25, 176, 13, 13, 3, 213, 217decma2c 11808 . . . 4 ((1 · 2310) + 1691) = 4001
219218, 16eqtr4i 2831 . . 3 ((1 · 2310) + 1691) = 𝑁
22013, 32, 15, 200, 219gcdi 15990 . 2 (𝑁 gcd 2310) = 1
2219, 15, 22, 27, 220gcdmodi 15991 1 (((2↑800) − 1) gcd 𝑁) = 1
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197   = wceq 1637  wcel 2156   class class class wbr 4844  (class class class)co 6870  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222  cmin 10547  cn 11301  2c2 11352  3c3 11353  4c4 11354  5c5 11355  6c6 11356  7c7 11357  8c8 11358  9c9 11359  0cn0 11555  cz 11639  cdc 11755  cexp 13079  cdvds 15199   gcd cgcd 15431  cprime 15599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-sup 8583  df-inf 8584  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-rp 12043  df-fz 12546  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-dvds 15200  df-gcd 15432  df-prm 15600
This theorem is referenced by:  4001prm  16059
  Copyright terms: Public domain W3C validator