Step | Hyp | Ref
| Expression |
1 | | prmex 16382 |
. . . . . 6
⊢ ℙ
∈ V |
2 | 1 | mptex 7099 |
. . . . 5
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V |
3 | | 1arith.1 |
. . . . 5
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
4 | 2, 3 | fnmpti 6576 |
. . . 4
⊢ 𝑀 Fn ℕ |
5 | 3 | 1arithlem3 16626 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥):ℙ⟶ℕ0) |
6 | | nn0ex 12239 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
7 | 6, 1 | elmap 8659 |
. . . . . . 7
⊢ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ↔ (𝑀‘𝑥):ℙ⟶ℕ0) |
8 | 5, 7 | sylibr 233 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ (ℕ0
↑m ℙ)) |
9 | | fzfi 13692 |
. . . . . . 7
⊢
(1...𝑥) ∈
Fin |
10 | | ffn 6600 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥):ℙ⟶ℕ0 →
(𝑀‘𝑥) Fn ℙ) |
11 | | elpreima 6935 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥) Fn ℙ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
12 | 5, 10, 11 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
13 | 3 | 1arithlem2 16625 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
14 | 13 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ)) |
15 | | prmz 16380 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
17 | | dvdsle 16019 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
18 | 15, 16, 17 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
19 | | pcelnn 16571 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
20 | 19 | ancoms 459 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
21 | | prmnn 16379 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
22 | | nnuz 12621 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
23 | 21, 22 | eleqtrdi 2849 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘1)) |
24 | | nnz 12342 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
25 | | elfz5 13248 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
26 | 23, 24, 25 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
27 | 18, 20, 26 | 3imtr4d 294 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
28 | 14, 27 | sylbid 239 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
29 | 28 | expimpd 454 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥))) |
30 | 12, 29 | sylbid 239 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥))) |
31 | 30 | ssrdv 3927 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) |
32 | | ssfi 8956 |
. . . . . . 7
⊢
(((1...𝑥) ∈ Fin
∧ (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
33 | 9, 31, 32 | sylancr 587 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
34 | | cnveq 5782 |
. . . . . . . . 9
⊢ (𝑒 = (𝑀‘𝑥) → ◡𝑒 = ◡(𝑀‘𝑥)) |
35 | 34 | imaeq1d 5968 |
. . . . . . . 8
⊢ (𝑒 = (𝑀‘𝑥) → (◡𝑒 “ ℕ) = (◡(𝑀‘𝑥) “ ℕ)) |
36 | 35 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑒 = (𝑀‘𝑥) → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
37 | | 1arith.2 |
. . . . . . 7
⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} |
38 | 36, 37 | elrab2 3627 |
. . . . . 6
⊢ ((𝑀‘𝑥) ∈ 𝑅 ↔ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ∧ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
39 | 8, 33, 38 | sylanbrc 583 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ 𝑅) |
40 | 39 | rgen 3074 |
. . . 4
⊢
∀𝑥 ∈
ℕ (𝑀‘𝑥) ∈ 𝑅 |
41 | | ffnfv 6992 |
. . . 4
⊢ (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅)) |
42 | 4, 40, 41 | mpbir2an 708 |
. . 3
⊢ 𝑀:ℕ⟶𝑅 |
43 | 13 | adantlr 712 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
44 | 3 | 1arithlem2 16625 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
45 | 44 | adantll 711 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
46 | 43, 45 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
47 | 46 | ralbidva 3111 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑞 ∈ ℙ
((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
48 | 3 | 1arithlem3 16626 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑀‘𝑦):ℙ⟶ℕ0) |
49 | | ffn 6600 |
. . . . . . . 8
⊢ ((𝑀‘𝑦):ℙ⟶ℕ0 →
(𝑀‘𝑦) Fn ℙ) |
50 | | eqfnfv 6909 |
. . . . . . . 8
⊢ (((𝑀‘𝑥) Fn ℙ ∧ (𝑀‘𝑦) Fn ℙ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
51 | 10, 49, 50 | syl2an 596 |
. . . . . . 7
⊢ (((𝑀‘𝑥):ℙ⟶ℕ0 ∧
(𝑀‘𝑦):ℙ⟶ℕ0) →
((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
52 | 5, 48, 51 | syl2an 596 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
53 | | nnnn0 12240 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
54 | | nnnn0 12240 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
55 | | pc11 16581 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
56 | 53, 54, 55 | syl2an 596 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
57 | 47, 52, 56 | 3bitr4d 311 |
. . . . 5
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ 𝑥 = 𝑦)) |
58 | 57 | biimpd 228 |
. . . 4
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)) |
59 | 58 | rgen2 3120 |
. . 3
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦) |
60 | | dff13 7128 |
. . 3
⊢ (𝑀:ℕ–1-1→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦))) |
61 | 42, 59, 60 | mpbir2an 708 |
. 2
⊢ 𝑀:ℕ–1-1→𝑅 |
62 | | eqid 2738 |
. . . . . 6
⊢ (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) |
63 | | cnveq 5782 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑓 → ◡𝑒 = ◡𝑓) |
64 | 63 | imaeq1d 5968 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑓 → (◡𝑒 “ ℕ) = (◡𝑓 “ ℕ)) |
65 | 64 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
66 | 65, 37 | elrab2 3627 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑅 ↔ (𝑓 ∈ (ℕ0
↑m ℙ) ∧ (◡𝑓 “ ℕ) ∈
Fin)) |
67 | 66 | simplbi 498 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → 𝑓 ∈ (ℕ0
↑m ℙ)) |
68 | 6, 1 | elmap 8659 |
. . . . . . . 8
⊢ (𝑓 ∈ (ℕ0
↑m ℙ) ↔ 𝑓:ℙ⟶ℕ0) |
69 | 67, 68 | sylib 217 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → 𝑓:ℙ⟶ℕ0) |
70 | 69 | ad2antrr 723 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑓:ℙ⟶ℕ0) |
71 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑦 ∈ ℝ) |
72 | | 0re 10977 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
73 | | ifcl 4504 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
74 | 71, 72, 73 | sylancl 586 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
75 | | max1 12919 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
76 | 72, 71, 75 | sylancr 587 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
77 | | flge0nn0 13540 |
. . . . . . . 8
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑦, 𝑦, 0)) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
78 | 74, 76, 77 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
79 | | nn0p1nn 12272 |
. . . . . . 7
⊢
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0 →
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
81 | 71 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ) |
82 | 80 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
83 | 82 | nnred 11988 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℝ) |
84 | 15 | ssriv 3925 |
. . . . . . . . . . . 12
⊢ ℙ
⊆ ℤ |
85 | | zssre 12326 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
86 | 84, 85 | sstri 3930 |
. . . . . . . . . . 11
⊢ ℙ
⊆ ℝ |
87 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ) |
88 | 86, 87 | sselid 3919 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ) |
89 | 74 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
90 | | max2 12921 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 𝑦
≤ if(0 ≤ 𝑦, 𝑦, 0)) |
91 | 72, 81, 90 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
92 | | flltp1 13520 |
. . . . . . . . . . . 12
⊢ (if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
93 | 89, 92 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
94 | 81, 89, 83, 91, 93 | lelttrd 11133 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
95 | | simprr 770 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞) |
96 | 81, 83, 88, 94, 95 | ltletrd 11135 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < 𝑞) |
97 | 81, 88 | ltnled 11122 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦)) |
98 | 96, 97 | mpbid 231 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ 𝑞 ≤ 𝑦) |
99 | 87 | biantrurd 533 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
100 | 70 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ0) |
101 | | ffn 6600 |
. . . . . . . . . . 11
⊢ (𝑓:ℙ⟶ℕ0 →
𝑓 Fn
ℙ) |
102 | | elpreima 6935 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ℙ → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
104 | 99, 103 | bitr4d 281 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ 𝑞 ∈ (◡𝑓 “ ℕ))) |
105 | | simplr 766 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
106 | | breq1 5077 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦)) |
107 | 106 | rspccv 3558 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(◡𝑓 “ ℕ)𝑘 ≤ 𝑦 → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
108 | 105, 107 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
109 | 104, 108 | sylbid 239 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ → 𝑞 ≤ 𝑦)) |
110 | 98, 109 | mtod 197 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ (𝑓‘𝑞) ∈ ℕ) |
111 | 100, 87 | ffvelrnd 6962 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) ∈
ℕ0) |
112 | | elnn0 12235 |
. . . . . . . . 9
⊢ ((𝑓‘𝑞) ∈ ℕ0 ↔ ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
113 | 111, 112 | sylib 217 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
114 | 113 | ord 861 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (¬ (𝑓‘𝑞) ∈ ℕ → (𝑓‘𝑞) = 0)) |
115 | 110, 114 | mpd 15 |
. . . . . 6
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) = 0) |
116 | 3, 62, 70, 80, 115 | 1arithlem4 16627 |
. . . . 5
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
117 | | cnvimass 5989 |
. . . . . . 7
⊢ (◡𝑓 “ ℕ) ⊆ dom 𝑓 |
118 | 69 | fdmd 6611 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 = ℙ) |
119 | 118, 86 | eqsstrdi 3975 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℝ) |
120 | 117, 119 | sstrid 3932 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ⊆
ℝ) |
121 | 66 | simprbi 497 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ∈
Fin) |
122 | | fimaxre2 11920 |
. . . . . 6
⊢ (((◡𝑓 “ ℕ) ⊆ ℝ ∧
(◡𝑓 “ ℕ) ∈ Fin) →
∃𝑦 ∈ ℝ
∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
123 | 120, 121,
122 | syl2anc 584 |
. . . . 5
⊢ (𝑓 ∈ 𝑅 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
124 | 116, 123 | r19.29a 3218 |
. . . 4
⊢ (𝑓 ∈ 𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
125 | 124 | rgen 3074 |
. . 3
⊢
∀𝑓 ∈
𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥) |
126 | | dffo3 6978 |
. . 3
⊢ (𝑀:ℕ–onto→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))) |
127 | 42, 125, 126 | mpbir2an 708 |
. 2
⊢ 𝑀:ℕ–onto→𝑅 |
128 | | df-f1o 6440 |
. 2
⊢ (𝑀:ℕ–1-1-onto→𝑅 ↔ (𝑀:ℕ–1-1→𝑅 ∧ 𝑀:ℕ–onto→𝑅)) |
129 | 61, 127, 128 | mpbir2an 708 |
1
⊢ 𝑀:ℕ–1-1-onto→𝑅 |