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

Theorem 4001lem4 15974
 Description: Lemma for 4001prm 15975. 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 11298 . . . 4 2 ∈ ℕ
2 8nn0 11428 . . . . . 6 8 ∈ ℕ0
3 0nn0 11420 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11625 . . . . 5 80 ∈ ℕ0
54, 3deccl 11625 . . . 4 800 ∈ ℕ0
6 nnexpcl 12988 . . . 4 ((2 ∈ ℕ ∧ 800 ∈ ℕ0) → (2↑800) ∈ ℕ)
71, 5, 6mp2an 710 . . 3 (2↑800) ∈ ℕ
8 nnm1nn0 11447 . . 3 ((2↑800) ∈ ℕ → ((2↑800) − 1) ∈ ℕ0)
97, 8ax-mp 5 . 2 ((2↑800) − 1) ∈ ℕ0
10 2nn0 11422 . . . . 5 2 ∈ ℕ0
11 3nn0 11423 . . . . 5 3 ∈ ℕ0
1210, 11deccl 11625 . . . 4 23 ∈ ℕ0
13 1nn0 11421 . . . 4 1 ∈ ℕ0
1412, 13deccl 11625 . . 3 231 ∈ ℕ0
1514, 3deccl 11625 . 2 2310 ∈ ℕ0
16 4001prm.1 . . 3 𝑁 = 4001
17 4nn0 11424 . . . . . 6 4 ∈ ℕ0
1817, 3deccl 11625 . . . . 5 40 ∈ ℕ0
1918, 3deccl 11625 . . . 4 400 ∈ ℕ0
20 1nn 11144 . . . 4 1 ∈ ℕ
2119, 20decnncl 11631 . . 3 4001 ∈ ℕ
2216, 21eqeltri 2799 . 2 𝑁 ∈ ℕ
23164001lem2 15972 . . 3 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
24 0p1e1 11245 . . . 4 (0 + 1) = 1
25 eqid 2724 . . . 4 2310 = 2310
2614, 3, 24, 25decsuc 11648 . . 3 (2310 + 1) = 2311
2722, 7, 13, 15, 23, 26modsubi 15899 . 2 (((2↑800) − 1) mod 𝑁) = (2310 mod 𝑁)
28 6nn0 11426 . . . . . 6 6 ∈ ℕ0
2913, 28deccl 11625 . . . . 5 16 ∈ ℕ0
30 9nn0 11429 . . . . 5 9 ∈ ℕ0
3129, 30deccl 11625 . . . 4 169 ∈ ℕ0
3231, 13deccl 11625 . . 3 1691 ∈ ℕ0
3328, 13deccl 11625 . . . . 5 61 ∈ ℕ0
3433, 30deccl 11625 . . . 4 619 ∈ ℕ0
35 5nn0 11425 . . . . . . 7 5 ∈ ℕ0
3617, 35deccl 11625 . . . . . 6 45 ∈ ℕ0
3736, 11deccl 11625 . . . . 5 453 ∈ ℕ0
3829, 28deccl 11625 . . . . . 6 166 ∈ ℕ0
3913, 10deccl 11625 . . . . . . . 8 12 ∈ ℕ0
4039, 13deccl 11625 . . . . . . 7 121 ∈ ℕ0
4111, 13deccl 11625 . . . . . . . . 9 31 ∈ ℕ0
4213, 17deccl 11625 . . . . . . . . . 10 14 ∈ ℕ0
4342nn0zi 11515 . . . . . . . . . . . . 13 14 ∈ ℤ
4411nn0zi 11515 . . . . . . . . . . . . 13 3 ∈ ℤ
45 gcdcom 15358 . . . . . . . . . . . . 13 ((14 ∈ ℤ ∧ 3 ∈ ℤ) → (14 gcd 3) = (3 gcd 14))
4643, 44, 45mp2an 710 . . . . . . . . . . . 12 (14 gcd 3) = (3 gcd 14)
47 3nn 11299 . . . . . . . . . . . . . 14 3 ∈ ℕ
48 4cn 11211 . . . . . . . . . . . . . . . 16 4 ∈ ℂ
49 3cn 11208 . . . . . . . . . . . . . . . 16 3 ∈ ℂ
50 4t3e12 11745 . . . . . . . . . . . . . . . 16 (4 · 3) = 12
5148, 49, 50mulcomli 10160 . . . . . . . . . . . . . . 15 (3 · 4) = 12
52 2p2e4 11257 . . . . . . . . . . . . . . 15 (2 + 2) = 4
5313, 10, 10, 51, 52decaddi 11692 . . . . . . . . . . . . . 14 ((3 · 4) + 2) = 14
54 2lt3 11308 . . . . . . . . . . . . . 14 2 < 3
5547, 17, 1, 53, 54ndvdsi 15259 . . . . . . . . . . . . 13 ¬ 3 ∥ 14
56 3prm 15529 . . . . . . . . . . . . . 14 3 ∈ ℙ
57 coprm 15546 . . . . . . . . . . . . . 14 ((3 ∈ ℙ ∧ 14 ∈ ℤ) → (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1))
5856, 43, 57mp2an 710 . . . . . . . . . . . . 13 (¬ 3 ∥ 14 ↔ (3 gcd 14) = 1)
5955, 58mpbi 220 . . . . . . . . . . . 12 (3 gcd 14) = 1
6046, 59eqtri 2746 . . . . . . . . . . 11 (14 gcd 3) = 1
61 eqid 2724 . . . . . . . . . . . 12 14 = 14
6211dec0h 11635 . . . . . . . . . . . 12 3 = 03
63 2t1e2 11289 . . . . . . . . . . . . . 14 (2 · 1) = 2
6463, 24oveq12i 6777 . . . . . . . . . . . . 13 ((2 · 1) + (0 + 1)) = (2 + 1)
65 2p1e3 11264 . . . . . . . . . . . . 13 (2 + 1) = 3
6664, 65eqtri 2746 . . . . . . . . . . . 12 ((2 · 1) + (0 + 1)) = 3
67 2cn 11204 . . . . . . . . . . . . . . 15 2 ∈ ℂ
68 4t2e8 11294 . . . . . . . . . . . . . . 15 (4 · 2) = 8
6948, 67, 68mulcomli 10160 . . . . . . . . . . . . . 14 (2 · 4) = 8
7069oveq1i 6775 . . . . . . . . . . . . 13 ((2 · 4) + 3) = (8 + 3)
71 8p3e11 11725 . . . . . . . . . . . . 13 (8 + 3) = 11
7270, 71eqtri 2746 . . . . . . . . . . . 12 ((2 · 4) + 3) = 11
7313, 17, 3, 11, 61, 62, 10, 13, 13, 66, 72decma2c 11681 . . . . . . . . . . 11 ((2 · 14) + 3) = 31
7410, 11, 42, 60, 73gcdi 15900 . . . . . . . . . 10 (31 gcd 14) = 1
75 eqid 2724 . . . . . . . . . . 11 31 = 31
7649mulid2i 10156 . . . . . . . . . . . . 13 (1 · 3) = 3
77 ax-1cn 10107 . . . . . . . . . . . . . 14 1 ∈ ℂ
7877addid1i 10336 . . . . . . . . . . . . 13 (1 + 0) = 1
7976, 78oveq12i 6777 . . . . . . . . . . . 12 ((1 · 3) + (1 + 0)) = (3 + 1)
80 3p1e4 11266 . . . . . . . . . . . 12 (3 + 1) = 4
8179, 80eqtri 2746 . . . . . . . . . . 11 ((1 · 3) + (1 + 0)) = 4
82 1t1e1 11288 . . . . . . . . . . . . 13 (1 · 1) = 1
8382oveq1i 6775 . . . . . . . . . . . 12 ((1 · 1) + 4) = (1 + 4)
84 4p1e5 11267 . . . . . . . . . . . . 13 (4 + 1) = 5
8548, 77, 84addcomli 10341 . . . . . . . . . . . 12 (1 + 4) = 5
8635dec0h 11635 . . . . . . . . . . . 12 5 = 05
8783, 85, 863eqtri 2750 . . . . . . . . . . 11 ((1 · 1) + 4) = 05
8811, 13, 13, 17, 75, 61, 13, 35, 3, 81, 87decma2c 11681 . . . . . . . . . 10 ((1 · 31) + 14) = 45
8913, 42, 41, 74, 88gcdi 15900 . . . . . . . . 9 (45 gcd 31) = 1
90 eqid 2724 . . . . . . . . . 10 45 = 45
9169, 80oveq12i 6777 . . . . . . . . . . 11 ((2 · 4) + (3 + 1)) = (8 + 4)
92 8p4e12 11727 . . . . . . . . . . 11 (8 + 4) = 12
9391, 92eqtri 2746 . . . . . . . . . 10 ((2 · 4) + (3 + 1)) = 12
94 5cn 11213 . . . . . . . . . . . 12 5 ∈ ℂ
95 5t2e10 11747 . . . . . . . . . . . 12 (5 · 2) = 10
9694, 67, 95mulcomli 10160 . . . . . . . . . . 11 (2 · 5) = 10
9713, 3, 24, 96decsuc 11648 . . . . . . . . . 10 ((2 · 5) + 1) = 11
9817, 35, 11, 13, 90, 75, 10, 13, 13, 93, 97decma2c 11681 . . . . . . . . 9 ((2 · 45) + 31) = 121
9910, 41, 36, 89, 98gcdi 15900 . . . . . . . 8 (121 gcd 45) = 1
100 eqid 2724 . . . . . . . . 9 121 = 121
101 eqid 2724 . . . . . . . . . 10 12 = 12
10248addid1i 10336 . . . . . . . . . . 11 (4 + 0) = 4
10317dec0h 11635 . . . . . . . . . . 11 4 = 04
104102, 103eqtri 2746 . . . . . . . . . 10 (4 + 0) = 04
105 00id 10324 . . . . . . . . . . . 12 (0 + 0) = 0
10682, 105oveq12i 6777 . . . . . . . . . . 11 ((1 · 1) + (0 + 0)) = (1 + 0)
107106, 78eqtri 2746 . . . . . . . . . 10 ((1 · 1) + (0 + 0)) = 1
10867mulid2i 10156 . . . . . . . . . . . 12 (1 · 2) = 2
109108oveq1i 6775 . . . . . . . . . . 11 ((1 · 2) + 4) = (2 + 4)
110 4p2e6 11275 . . . . . . . . . . . 12 (4 + 2) = 6
11148, 67, 110addcomli 10341 . . . . . . . . . . 11 (2 + 4) = 6
11228dec0h 11635 . . . . . . . . . . 11 6 = 06
113109, 111, 1123eqtri 2750 . . . . . . . . . 10 ((1 · 2) + 4) = 06
11413, 10, 3, 17, 101, 104, 13, 28, 3, 107, 113decma2c 11681 . . . . . . . . 9 ((1 · 12) + (4 + 0)) = 16
11582oveq1i 6775 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
116 5p1e6 11268 . . . . . . . . . . 11 (5 + 1) = 6
11794, 77, 116addcomli 10341 . . . . . . . . . 10 (1 + 5) = 6
118115, 117, 1123eqtri 2750 . . . . . . . . 9 ((1 · 1) + 5) = 06
11939, 13, 17, 35, 100, 90, 13, 28, 3, 114, 118decma2c 11681 . . . . . . . 8 ((1 · 121) + 45) = 166
12013, 36, 40, 99, 119gcdi 15900 . . . . . . 7 (166 gcd 121) = 1
121 eqid 2724 . . . . . . . 8 166 = 166
122 eqid 2724 . . . . . . . . 9 16 = 16
12313, 10, 65, 101decsuc 11648 . . . . . . . . 9 (12 + 1) = 13
124 1p1e2 11247 . . . . . . . . . . 11 (1 + 1) = 2
12563, 124oveq12i 6777 . . . . . . . . . 10 ((2 · 1) + (1 + 1)) = (2 + 2)
126125, 52eqtri 2746 . . . . . . . . 9 ((2 · 1) + (1 + 1)) = 4
127 6cn 11215 . . . . . . . . . . 11 6 ∈ ℂ
128 6t2e12 11754 . . . . . . . . . . 11 (6 · 2) = 12
129127, 67, 128mulcomli 10160 . . . . . . . . . 10 (2 · 6) = 12
130 3p2e5 11273 . . . . . . . . . . 11 (3 + 2) = 5
13149, 67, 130addcomli 10341 . . . . . . . . . 10 (2 + 3) = 5
13213, 10, 11, 129, 131decaddi 11692 . . . . . . . . 9 ((2 · 6) + 3) = 15
13313, 28, 13, 11, 122, 123, 10, 35, 13, 126, 132decma2c 11681 . . . . . . . 8 ((2 · 16) + (12 + 1)) = 45
13413, 10, 65, 129decsuc 11648 . . . . . . . 8 ((2 · 6) + 1) = 13
13529, 28, 39, 13, 121, 100, 10, 11, 13, 133, 134decma2c 11681 . . . . . . 7 ((2 · 166) + 121) = 453
13610, 40, 38, 120, 135gcdi 15900 . . . . . 6 (453 gcd 166) = 1
137 eqid 2724 . . . . . . 7 453 = 453
13829nn0cni 11417 . . . . . . . . 9 16 ∈ ℂ
139138addid1i 10336 . . . . . . . 8 (16 + 0) = 16
14048mulid2i 10156 . . . . . . . . . 10 (1 · 4) = 4
141140, 124oveq12i 6777 . . . . . . . . 9 ((1 · 4) + (1 + 1)) = (4 + 2)
142141, 110eqtri 2746 . . . . . . . 8 ((1 · 4) + (1 + 1)) = 6
14394mulid2i 10156 . . . . . . . . . 10 (1 · 5) = 5
144143oveq1i 6775 . . . . . . . . 9 ((1 · 5) + 6) = (5 + 6)
145 6p5e11 11713 . . . . . . . . . 10 (6 + 5) = 11
146127, 94, 145addcomli 10341 . . . . . . . . 9 (5 + 6) = 11
147144, 146eqtri 2746 . . . . . . . 8 ((1 · 5) + 6) = 11
14817, 35, 13, 28, 90, 139, 13, 13, 13, 142, 147decma2c 11681 . . . . . . 7 ((1 · 45) + (16 + 0)) = 61
14976oveq1i 6775 . . . . . . . 8 ((1 · 3) + 6) = (3 + 6)
150 6p3e9 11283 . . . . . . . . 9 (6 + 3) = 9
151127, 49, 150addcomli 10341 . . . . . . . 8 (3 + 6) = 9
15230dec0h 11635 . . . . . . . 8 9 = 09
153149, 151, 1523eqtri 2750 . . . . . . 7 ((1 · 3) + 6) = 09
15436, 11, 29, 28, 137, 121, 13, 30, 3, 148, 153decma2c 11681 . . . . . 6 ((1 · 453) + 166) = 619
15513, 38, 37, 136, 154gcdi 15900 . . . . 5 (619 gcd 453) = 1
156 eqid 2724 . . . . . 6 619 = 619
157 7nn0 11427 . . . . . . 7 7 ∈ ℕ0
158 eqid 2724 . . . . . . 7 61 = 61
159 5p2e7 11278 . . . . . . . 8 (5 + 2) = 7
16017, 35, 10, 90, 159decaddi 11692 . . . . . . 7 (45 + 2) = 47
161102oveq2i 6776 . . . . . . . 8 ((2 · 6) + (4 + 0)) = ((2 · 6) + 4)
16213, 10, 17, 129, 111decaddi 11692 . . . . . . . 8 ((2 · 6) + 4) = 16
163161, 162eqtri 2746 . . . . . . 7 ((2 · 6) + (4 + 0)) = 16
16463oveq1i 6775 . . . . . . . 8 ((2 · 1) + 7) = (2 + 7)
165 7cn 11217 . . . . . . . . 9 7 ∈ ℂ
166 7p2e9 11285 . . . . . . . . 9 (7 + 2) = 9
167165, 67, 166addcomli 10341 . . . . . . . 8 (2 + 7) = 9
168164, 167, 1523eqtri 2750 . . . . . . 7 ((2 · 1) + 7) = 09
16928, 13, 17, 157, 158, 160, 10, 30, 3, 163, 168decma2c 11681 . . . . . 6 ((2 · 61) + (45 + 2)) = 169
170 9cn 11221 . . . . . . . 8 9 ∈ ℂ
171 9t2e18 11776 . . . . . . . 8 (9 · 2) = 18
172170, 67, 171mulcomli 10160 . . . . . . 7 (2 · 9) = 18
17313, 2, 11, 172, 124, 13, 71decaddci 11693 . . . . . 6 ((2 · 9) + 3) = 21
17433, 30, 36, 11, 156, 137, 10, 13, 10, 169, 173decma2c 11681 . . . . 5 ((2 · 619) + 453) = 1691
17510, 37, 34, 155, 174gcdi 15900 . . . 4 (1691 gcd 619) = 1
176 eqid 2724 . . . . 5 1691 = 1691
177 eqid 2724 . . . . . 6 169 = 169
17828, 13, 124, 158decsuc 11648 . . . . . 6 (61 + 1) = 62
179 6p1e7 11269 . . . . . . . 8 (6 + 1) = 7
180157dec0h 11635 . . . . . . . 8 7 = 07
181179, 180eqtri 2746 . . . . . . 7 (6 + 1) = 07
18282, 24oveq12i 6777 . . . . . . . 8 ((1 · 1) + (0 + 1)) = (1 + 1)
183182, 124eqtri 2746 . . . . . . 7 ((1 · 1) + (0 + 1)) = 2
184127mulid2i 10156 . . . . . . . . 9 (1 · 6) = 6
185184oveq1i 6775 . . . . . . . 8 ((1 · 6) + 7) = (6 + 7)
186 7p6e13 11721 . . . . . . . . 9 (7 + 6) = 13
187165, 127, 186addcomli 10341 . . . . . . . 8 (6 + 7) = 13
188185, 187eqtri 2746 . . . . . . 7 ((1 · 6) + 7) = 13
18913, 28, 3, 157, 122, 181, 13, 11, 13, 183, 188decma2c 11681 . . . . . 6 ((1 · 16) + (6 + 1)) = 23
190170mulid2i 10156 . . . . . . . 8 (1 · 9) = 9
191190oveq1i 6775 . . . . . . 7 ((1 · 9) + 2) = (9 + 2)
192 9p2e11 11732 . . . . . . 7 (9 + 2) = 11
193191, 192eqtri 2746 . . . . . 6 ((1 · 9) + 2) = 11
19429, 30, 28, 10, 177, 178, 13, 13, 13, 189, 193decma2c 11681 . . . . 5 ((1 · 169) + (61 + 1)) = 231
19582oveq1i 6775 . . . . . 6 ((1 · 1) + 9) = (1 + 9)
196 9p1e10 11609 . . . . . . 7 (9 + 1) = 10
197170, 77, 196addcomli 10341 . . . . . 6 (1 + 9) = 10
198195, 197eqtri 2746 . . . . 5 ((1 · 1) + 9) = 10
19931, 13, 33, 30, 176, 156, 13, 3, 13, 194, 198decma2c 11681 . . . 4 ((1 · 1691) + 619) = 2310
20013, 34, 32, 175, 199gcdi 15900 . . 3 (2310 gcd 1691) = 1
201 eqid 2724 . . . . . 6 231 = 231
20231nn0cni 11417 . . . . . . 7 169 ∈ ℂ
203202addid1i 10336 . . . . . 6 (169 + 0) = 169
204 eqid 2724 . . . . . . 7 23 = 23
20513, 28, 179, 122decsuc 11648 . . . . . . 7 (16 + 1) = 17
206108, 124oveq12i 6777 . . . . . . . 8 ((1 · 2) + (1 + 1)) = (2 + 2)
207206, 52eqtri 2746 . . . . . . 7 ((1 · 2) + (1 + 1)) = 4
20876oveq1i 6775 . . . . . . . 8 ((1 · 3) + 7) = (3 + 7)
209 7p3e10 11716 . . . . . . . . 9 (7 + 3) = 10
210165, 49, 209addcomli 10341 . . . . . . . 8 (3 + 7) = 10
211208, 210eqtri 2746 . . . . . . 7 ((1 · 3) + 7) = 10
21210, 11, 13, 157, 204, 205, 13, 3, 13, 207, 211decma2c 11681 . . . . . 6 ((1 · 23) + (16 + 1)) = 40
21312, 13, 29, 30, 201, 203, 13, 3, 13, 212, 198decma2c 11681 . . . . 5 ((1 · 231) + (169 + 0)) = 400
21477mul01i 10339 . . . . . . 7 (1 · 0) = 0
215214oveq1i 6775 . . . . . 6 ((1 · 0) + 1) = (0 + 1)
21613dec0h 11635 . . . . . 6 1 = 01
217215, 24, 2163eqtri 2750 . . . . 5 ((1 · 0) + 1) = 01
21814, 3, 31, 13, 25, 176, 13, 13, 3, 213, 217decma2c 11681 . . . 4 ((1 · 2310) + 1691) = 4001
219218, 16eqtr4i 2749 . . 3 ((1 · 2310) + 1691) = 𝑁
22013, 32, 15, 200, 219gcdi 15900 . 2 (𝑁 gcd 2310) = 1
2219, 15, 22, 27, 220gcdmodi 15901 1 (((2↑800) − 1) gcd 𝑁) = 1
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196   = wceq 1596   ∈ wcel 2103   class class class wbr 4760  (class class class)co 6765  0cc0 10049  1c1 10050   + caddc 10052   · cmul 10054   − cmin 10379  ℕcn 11133  2c2 11183  3c3 11184  4c4 11185  5c5 11186  6c6 11187  7c7 11188  8c8 11189  9c9 11190  ℕ0cn0 11405  ℤcz 11490  ;cdc 11606  ↑cexp 12975   ∥ cdvds 15103   gcd cgcd 15339  ℙcprime 15508 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-2o 7681  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-inf 8465  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-rp 11947  df-fz 12441  df-fl 12708  df-mod 12784  df-seq 12917  df-exp 12976  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-dvds 15104  df-gcd 15340  df-prm 15509 This theorem is referenced by:  4001prm  15975
 Copyright terms: Public domain W3C validator