Step | Hyp | Ref
| Expression |
1 | | prmex 16118 |
. . . . . 6
⊢ ℙ
∈ V |
2 | 1 | mptex 6996 |
. . . . 5
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V |
3 | | 1arith.1 |
. . . . 5
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
4 | 2, 3 | fnmpti 6480 |
. . . 4
⊢ 𝑀 Fn ℕ |
5 | 3 | 1arithlem3 16361 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥):ℙ⟶ℕ0) |
6 | | nn0ex 11982 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
7 | 6, 1 | elmap 8481 |
. . . . . . 7
⊢ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ↔ (𝑀‘𝑥):ℙ⟶ℕ0) |
8 | 5, 7 | sylibr 237 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ (ℕ0
↑m ℙ)) |
9 | | fzfi 13431 |
. . . . . . 7
⊢
(1...𝑥) ∈
Fin |
10 | | ffn 6504 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥):ℙ⟶ℕ0 →
(𝑀‘𝑥) Fn ℙ) |
11 | | elpreima 6835 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥) Fn ℙ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
12 | 5, 10, 11 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
13 | 3 | 1arithlem2 16360 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
14 | 13 | eleq1d 2817 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ)) |
15 | | prmz 16116 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
16 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
17 | | dvdsle 15755 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
18 | 15, 16, 17 | syl2anr 600 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
19 | | pcelnn 16306 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
20 | 19 | ancoms 462 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
21 | | prmnn 16115 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
22 | | nnuz 12363 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
23 | 21, 22 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘1)) |
24 | | nnz 12085 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
25 | | elfz5 12990 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
26 | 23, 24, 25 | syl2anr 600 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
27 | 18, 20, 26 | 3imtr4d 297 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
28 | 14, 27 | sylbid 243 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
29 | 28 | expimpd 457 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥))) |
30 | 12, 29 | sylbid 243 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥))) |
31 | 30 | ssrdv 3883 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) |
32 | | ssfi 8772 |
. . . . . . 7
⊢
(((1...𝑥) ∈ Fin
∧ (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
33 | 9, 31, 32 | sylancr 590 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
34 | | cnveq 5716 |
. . . . . . . . 9
⊢ (𝑒 = (𝑀‘𝑥) → ◡𝑒 = ◡(𝑀‘𝑥)) |
35 | 34 | imaeq1d 5902 |
. . . . . . . 8
⊢ (𝑒 = (𝑀‘𝑥) → (◡𝑒 “ ℕ) = (◡(𝑀‘𝑥) “ ℕ)) |
36 | 35 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑒 = (𝑀‘𝑥) → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
37 | | 1arith.2 |
. . . . . . 7
⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑m ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} |
38 | 36, 37 | elrab2 3591 |
. . . . . 6
⊢ ((𝑀‘𝑥) ∈ 𝑅 ↔ ((𝑀‘𝑥) ∈ (ℕ0
↑m ℙ) ∧ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
39 | 8, 33, 38 | sylanbrc 586 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ 𝑅) |
40 | 39 | rgen 3063 |
. . . 4
⊢
∀𝑥 ∈
ℕ (𝑀‘𝑥) ∈ 𝑅 |
41 | | ffnfv 6892 |
. . . 4
⊢ (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅)) |
42 | 4, 40, 41 | mpbir2an 711 |
. . 3
⊢ 𝑀:ℕ⟶𝑅 |
43 | 13 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
44 | 3 | 1arithlem2 16360 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
45 | 44 | adantll 714 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
46 | 43, 45 | eqeq12d 2754 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
47 | 46 | ralbidva 3108 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑞 ∈ ℙ
((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
48 | 3 | 1arithlem3 16361 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑀‘𝑦):ℙ⟶ℕ0) |
49 | | ffn 6504 |
. . . . . . . 8
⊢ ((𝑀‘𝑦):ℙ⟶ℕ0 →
(𝑀‘𝑦) Fn ℙ) |
50 | | eqfnfv 6809 |
. . . . . . . 8
⊢ (((𝑀‘𝑥) Fn ℙ ∧ (𝑀‘𝑦) Fn ℙ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
51 | 10, 49, 50 | syl2an 599 |
. . . . . . 7
⊢ (((𝑀‘𝑥):ℙ⟶ℕ0 ∧
(𝑀‘𝑦):ℙ⟶ℕ0) →
((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
52 | 5, 48, 51 | syl2an 599 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
53 | | nnnn0 11983 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
54 | | nnnn0 11983 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
55 | | pc11 16316 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
56 | 53, 54, 55 | syl2an 599 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
57 | 47, 52, 56 | 3bitr4d 314 |
. . . . 5
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ 𝑥 = 𝑦)) |
58 | 57 | biimpd 232 |
. . . 4
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)) |
59 | 58 | rgen2 3115 |
. . 3
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦) |
60 | | dff13 7024 |
. . 3
⊢ (𝑀:ℕ–1-1→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦))) |
61 | 42, 59, 60 | mpbir2an 711 |
. 2
⊢ 𝑀:ℕ–1-1→𝑅 |
62 | | eqid 2738 |
. . . . . 6
⊢ (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) |
63 | | cnveq 5716 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑓 → ◡𝑒 = ◡𝑓) |
64 | 63 | imaeq1d 5902 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑓 → (◡𝑒 “ ℕ) = (◡𝑓 “ ℕ)) |
65 | 64 | eleq1d 2817 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
66 | 65, 37 | elrab2 3591 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑅 ↔ (𝑓 ∈ (ℕ0
↑m ℙ) ∧ (◡𝑓 “ ℕ) ∈
Fin)) |
67 | 66 | simplbi 501 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → 𝑓 ∈ (ℕ0
↑m ℙ)) |
68 | 6, 1 | elmap 8481 |
. . . . . . . 8
⊢ (𝑓 ∈ (ℕ0
↑m ℙ) ↔ 𝑓:ℙ⟶ℕ0) |
69 | 67, 68 | sylib 221 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → 𝑓:ℙ⟶ℕ0) |
70 | 69 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑓:ℙ⟶ℕ0) |
71 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑦 ∈ ℝ) |
72 | | 0re 10721 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
73 | | ifcl 4459 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
74 | 71, 72, 73 | sylancl 589 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
75 | | max1 12661 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
76 | 72, 71, 75 | sylancr 590 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
77 | | flge0nn0 13281 |
. . . . . . . 8
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑦, 𝑦, 0)) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
78 | 74, 76, 77 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
79 | | nn0p1nn 12015 |
. . . . . . 7
⊢
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0 →
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
80 | 78, 79 | syl 17 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
81 | 71 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ) |
82 | 80 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
83 | 82 | nnred 11731 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℝ) |
84 | 15 | ssriv 3881 |
. . . . . . . . . . . 12
⊢ ℙ
⊆ ℤ |
85 | | zssre 12069 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
86 | 84, 85 | sstri 3886 |
. . . . . . . . . . 11
⊢ ℙ
⊆ ℝ |
87 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ) |
88 | 86, 87 | sseldi 3875 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ) |
89 | 74 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
90 | | max2 12663 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 𝑦
≤ if(0 ≤ 𝑦, 𝑦, 0)) |
91 | 72, 81, 90 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
92 | | flltp1 13261 |
. . . . . . . . . . . 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 10876 |
. . . . . . . . . 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 10878 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < 𝑞) |
97 | 81, 88 | ltnled 10865 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦)) |
98 | 96, 97 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ 𝑞 ≤ 𝑦) |
99 | 87 | biantrurd 536 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
100 | 70 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ0) |
101 | | ffn 6504 |
. . . . . . . . . . 11
⊢ (𝑓:ℙ⟶ℕ0 →
𝑓 Fn
ℙ) |
102 | | elpreima 6835 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ℙ → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
104 | 99, 103 | bitr4d 285 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ 𝑞 ∈ (◡𝑓 “ ℕ))) |
105 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
106 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦)) |
107 | 106 | rspccv 3523 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(◡𝑓 “ ℕ)𝑘 ≤ 𝑦 → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
108 | 105, 107 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
109 | 104, 108 | sylbid 243 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ → 𝑞 ≤ 𝑦)) |
110 | 98, 109 | mtod 201 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ (𝑓‘𝑞) ∈ ℕ) |
111 | 100, 87 | ffvelrnd 6862 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) ∈
ℕ0) |
112 | | elnn0 11978 |
. . . . . . . . 9
⊢ ((𝑓‘𝑞) ∈ ℕ0 ↔ ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
113 | 111, 112 | sylib 221 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
114 | 113 | ord 863 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (¬ (𝑓‘𝑞) ∈ ℕ → (𝑓‘𝑞) = 0)) |
115 | 110, 114 | mpd 15 |
. . . . . 6
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) = 0) |
116 | 3, 62, 70, 80, 115 | 1arithlem4 16362 |
. . . . 5
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
117 | | cnvimass 5923 |
. . . . . . 7
⊢ (◡𝑓 “ ℕ) ⊆ dom 𝑓 |
118 | 69 | fdmd 6515 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 = ℙ) |
119 | 118, 86 | eqsstrdi 3931 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℝ) |
120 | 117, 119 | sstrid 3888 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ⊆
ℝ) |
121 | 66 | simprbi 500 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ∈
Fin) |
122 | | fimaxre2 11663 |
. . . . . 6
⊢ (((◡𝑓 “ ℕ) ⊆ ℝ ∧
(◡𝑓 “ ℕ) ∈ Fin) →
∃𝑦 ∈ ℝ
∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
123 | 120, 121,
122 | syl2anc 587 |
. . . . 5
⊢ (𝑓 ∈ 𝑅 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
124 | 116, 123 | r19.29a 3199 |
. . . 4
⊢ (𝑓 ∈ 𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
125 | 124 | rgen 3063 |
. . 3
⊢
∀𝑓 ∈
𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥) |
126 | | dffo3 6878 |
. . 3
⊢ (𝑀:ℕ–onto→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))) |
127 | 42, 125, 126 | mpbir2an 711 |
. 2
⊢ 𝑀:ℕ–onto→𝑅 |
128 | | df-f1o 6346 |
. 2
⊢ (𝑀:ℕ–1-1-onto→𝑅 ↔ (𝑀:ℕ–1-1→𝑅 ∧ 𝑀:ℕ–onto→𝑅)) |
129 | 61, 127, 128 | mpbir2an 711 |
1
⊢ 𝑀:ℕ–1-1-onto→𝑅 |