| Step | Hyp | Ref
| Expression |
| 1 | | prmex 16714 |
. . . . . 6
⊢ ℙ
∈ V |
| 2 | 1 | mptex 7243 |
. . . . 5
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V |
| 3 | | 1arith.1 |
. . . . 5
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
| 4 | 2, 3 | fnmpti 6711 |
. . . 4
⊢ 𝑀 Fn ℕ |
| 5 | 3 | 1arithlem3 16963 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥):ℙ⟶ℕ0) |
| 6 | | nn0ex 12532 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
| 7 | 6, 1 | elmap 8911 |
. . . . . . 7
⊢ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ↔ (𝑀‘𝑥):ℙ⟶ℕ0) |
| 8 | 5, 7 | sylibr 234 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ (ℕ0
↑m ℙ)) |
| 9 | | fzfi 14013 |
. . . . . . 7
⊢
(1...𝑥) ∈
Fin |
| 10 | | ffn 6736 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥):ℙ⟶ℕ0 →
(𝑀‘𝑥) Fn ℙ) |
| 11 | | elpreima 7078 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥) Fn ℙ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
| 12 | 5, 10, 11 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
| 13 | 3 | 1arithlem2 16962 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
| 14 | 13 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ)) |
| 15 | | prmz 16712 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
| 16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
| 17 | | dvdsle 16347 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
| 18 | 15, 16, 17 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
| 19 | | pcelnn 16908 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
| 20 | 19 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
| 21 | | prmnn 16711 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
| 22 | | nnuz 12921 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
| 23 | 21, 22 | eleqtrdi 2851 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘1)) |
| 24 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
| 25 | | elfz5 13556 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
| 26 | 23, 24, 25 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
| 27 | 18, 20, 26 | 3imtr4d 294 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
| 28 | 14, 27 | sylbid 240 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
| 29 | 28 | expimpd 453 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥))) |
| 30 | 12, 29 | sylbid 240 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥))) |
| 31 | 30 | ssrdv 3989 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) |
| 32 | | ssfi 9213 |
. . . . . . 7
⊢
(((1...𝑥) ∈ Fin
∧ (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
| 33 | 9, 31, 32 | sylancr 587 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
| 34 | | cnveq 5884 |
. . . . . . . . 9
⊢ (𝑒 = (𝑀‘𝑥) → ◡𝑒 = ◡(𝑀‘𝑥)) |
| 35 | 34 | imaeq1d 6077 |
. . . . . . . 8
⊢ (𝑒 = (𝑀‘𝑥) → (◡𝑒 “ ℕ) = (◡(𝑀‘𝑥) “ ℕ)) |
| 36 | 35 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑒 = (𝑀‘𝑥) → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
| 37 | | 1arith.2 |
. . . . . . 7
⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} |
| 38 | 36, 37 | elrab2 3695 |
. . . . . 6
⊢ ((𝑀‘𝑥) ∈ 𝑅 ↔ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ∧ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
| 39 | 8, 33, 38 | sylanbrc 583 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ 𝑅) |
| 40 | 39 | rgen 3063 |
. . . 4
⊢
∀𝑥 ∈
ℕ (𝑀‘𝑥) ∈ 𝑅 |
| 41 | | ffnfv 7139 |
. . . 4
⊢ (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅)) |
| 42 | 4, 40, 41 | mpbir2an 711 |
. . 3
⊢ 𝑀:ℕ⟶𝑅 |
| 43 | 13 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
| 44 | 3 | 1arithlem2 16962 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
| 45 | 44 | adantll 714 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
| 46 | 43, 45 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
| 47 | 46 | ralbidva 3176 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑞 ∈ ℙ
((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
| 48 | 3 | 1arithlem3 16963 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑀‘𝑦):ℙ⟶ℕ0) |
| 49 | | ffn 6736 |
. . . . . . . 8
⊢ ((𝑀‘𝑦):ℙ⟶ℕ0 →
(𝑀‘𝑦) Fn ℙ) |
| 50 | | eqfnfv 7051 |
. . . . . . . 8
⊢ (((𝑀‘𝑥) Fn ℙ ∧ (𝑀‘𝑦) Fn ℙ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
| 51 | 10, 49, 50 | syl2an 596 |
. . . . . . 7
⊢ (((𝑀‘𝑥):ℙ⟶ℕ0 ∧
(𝑀‘𝑦):ℙ⟶ℕ0) →
((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
| 52 | 5, 48, 51 | syl2an 596 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
| 53 | | nnnn0 12533 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
| 54 | | nnnn0 12533 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
| 55 | | pc11 16918 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
| 56 | 53, 54, 55 | syl2an 596 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
| 57 | 47, 52, 56 | 3bitr4d 311 |
. . . . 5
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ 𝑥 = 𝑦)) |
| 58 | 57 | biimpd 229 |
. . . 4
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)) |
| 59 | 58 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦) |
| 60 | | dff13 7275 |
. . 3
⊢ (𝑀:ℕ–1-1→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦))) |
| 61 | 42, 59, 60 | mpbir2an 711 |
. 2
⊢ 𝑀:ℕ–1-1→𝑅 |
| 62 | | eqid 2737 |
. . . . . 6
⊢ (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) |
| 63 | | cnveq 5884 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑓 → ◡𝑒 = ◡𝑓) |
| 64 | 63 | imaeq1d 6077 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑓 → (◡𝑒 “ ℕ) = (◡𝑓 “ ℕ)) |
| 65 | 64 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
| 66 | 65, 37 | elrab2 3695 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑅 ↔ (𝑓 ∈ (ℕ0
↑m ℙ) ∧ (◡𝑓 “ ℕ) ∈
Fin)) |
| 67 | 66 | simplbi 497 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → 𝑓 ∈ (ℕ0
↑m ℙ)) |
| 68 | 6, 1 | elmap 8911 |
. . . . . . . 8
⊢ (𝑓 ∈ (ℕ0
↑m ℙ) ↔ 𝑓:ℙ⟶ℕ0) |
| 69 | 67, 68 | sylib 218 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → 𝑓:ℙ⟶ℕ0) |
| 70 | 69 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑓:ℙ⟶ℕ0) |
| 71 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑦 ∈ ℝ) |
| 72 | | 0re 11263 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
| 73 | | ifcl 4571 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
| 74 | 71, 72, 73 | sylancl 586 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
| 75 | | max1 13227 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 76 | 72, 71, 75 | sylancr 587 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 77 | | flge0nn0 13860 |
. . . . . . . 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 12565 |
. . . . . . 7
⊢
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0 →
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
| 80 | 78, 79 | syl 17 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
| 81 | 71 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ) |
| 82 | 80 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
| 83 | 82 | nnred 12281 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℝ) |
| 84 | 15 | ssriv 3987 |
. . . . . . . . . . . 12
⊢ ℙ
⊆ ℤ |
| 85 | | zssre 12620 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
| 86 | 84, 85 | sstri 3993 |
. . . . . . . . . . 11
⊢ ℙ
⊆ ℝ |
| 87 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ) |
| 88 | 86, 87 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ) |
| 89 | 74 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
| 90 | | max2 13229 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 𝑦
≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 91 | 72, 81, 90 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 92 | | flltp1 13840 |
. . . . . . . . . . . 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 11419 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
| 95 | | simprr 773 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞) |
| 96 | 81, 83, 88, 94, 95 | ltletrd 11421 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < 𝑞) |
| 97 | 81, 88 | ltnled 11408 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦)) |
| 98 | 96, 97 | mpbid 232 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ 𝑞 ≤ 𝑦) |
| 99 | 87 | biantrurd 532 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
| 100 | 70 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ0) |
| 101 | | ffn 6736 |
. . . . . . . . . . 11
⊢ (𝑓:ℙ⟶ℕ0 →
𝑓 Fn
ℙ) |
| 102 | | elpreima 7078 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ℙ → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
| 103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
| 104 | 99, 103 | bitr4d 282 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ 𝑞 ∈ (◡𝑓 “ ℕ))) |
| 105 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
| 106 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦)) |
| 107 | 106 | rspccv 3619 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(◡𝑓 “ ℕ)𝑘 ≤ 𝑦 → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
| 108 | 105, 107 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
| 109 | 104, 108 | sylbid 240 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ → 𝑞 ≤ 𝑦)) |
| 110 | 98, 109 | mtod 198 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ (𝑓‘𝑞) ∈ ℕ) |
| 111 | 100, 87 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) ∈
ℕ0) |
| 112 | | elnn0 12528 |
. . . . . . . . 9
⊢ ((𝑓‘𝑞) ∈ ℕ0 ↔ ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
| 113 | 111, 112 | sylib 218 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
| 114 | 113 | ord 865 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (¬ (𝑓‘𝑞) ∈ ℕ → (𝑓‘𝑞) = 0)) |
| 115 | 110, 114 | mpd 15 |
. . . . . 6
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) = 0) |
| 116 | 3, 62, 70, 80, 115 | 1arithlem4 16964 |
. . . . 5
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
| 117 | | cnvimass 6100 |
. . . . . . 7
⊢ (◡𝑓 “ ℕ) ⊆ dom 𝑓 |
| 118 | 69 | fdmd 6746 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 = ℙ) |
| 119 | 118, 86 | eqsstrdi 4028 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℝ) |
| 120 | 117, 119 | sstrid 3995 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ⊆
ℝ) |
| 121 | 66 | simprbi 496 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ∈
Fin) |
| 122 | | fimaxre2 12213 |
. . . . . 6
⊢ (((◡𝑓 “ ℕ) ⊆ ℝ ∧
(◡𝑓 “ ℕ) ∈ Fin) →
∃𝑦 ∈ ℝ
∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
| 123 | 120, 121,
122 | syl2anc 584 |
. . . . 5
⊢ (𝑓 ∈ 𝑅 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
| 124 | 116, 123 | r19.29a 3162 |
. . . 4
⊢ (𝑓 ∈ 𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
| 125 | 124 | rgen 3063 |
. . 3
⊢
∀𝑓 ∈
𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥) |
| 126 | | dffo3 7122 |
. . 3
⊢ (𝑀:ℕ–onto→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))) |
| 127 | 42, 125, 126 | mpbir2an 711 |
. 2
⊢ 𝑀:ℕ–onto→𝑅 |
| 128 | | df-f1o 6568 |
. 2
⊢ (𝑀:ℕ–1-1-onto→𝑅 ↔ (𝑀:ℕ–1-1→𝑅 ∧ 𝑀:ℕ–onto→𝑅)) |
| 129 | 61, 127, 128 | mpbir2an 711 |
1
⊢ 𝑀:ℕ–1-1-onto→𝑅 |