Step | Hyp | Ref
| Expression |
1 | | zex 11386 |
. . . . . . 7
⊢ ℤ
∈ V |
2 | | prmz 15389 |
. . . . . . . 8
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
3 | 2 | ssriv 3607 |
. . . . . . 7
⊢ ℙ
⊆ ℤ |
4 | 1, 3 | ssexi 4803 |
. . . . . 6
⊢ ℙ
∈ V |
5 | 4 | mptex 6486 |
. . . . 5
⊢ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)) ∈ V |
6 | | 1arith.1 |
. . . . 5
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) |
7 | 5, 6 | fnmpti 6022 |
. . . 4
⊢ 𝑀 Fn ℕ |
8 | 6 | 1arithlem3 15629 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥):ℙ⟶ℕ0) |
9 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
10 | 9, 4 | elmap 7886 |
. . . . . . 7
⊢ ((𝑀‘𝑥) ∈ (ℕ0
↑𝑚 ℙ) ↔ (𝑀‘𝑥):ℙ⟶ℕ0) |
11 | 8, 10 | sylibr 224 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ (ℕ0
↑𝑚 ℙ)) |
12 | | fzfi 12771 |
. . . . . . 7
⊢
(1...𝑥) ∈
Fin |
13 | | ffn 6045 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥):ℙ⟶ℕ0 →
(𝑀‘𝑥) Fn ℙ) |
14 | | elpreima 6337 |
. . . . . . . . . 10
⊢ ((𝑀‘𝑥) Fn ℙ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
15 | 8, 13, 14 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) ↔ (𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ))) |
16 | 6 | 1arithlem2 15628 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
17 | 16 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ ↔ (𝑞 pCnt 𝑥) ∈ ℕ)) |
18 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ) |
19 | | dvdsle 15032 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
20 | 2, 18, 19 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
21 | | pcelnn 15574 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℙ ∧ 𝑥 ∈ ℕ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
22 | 21 | ancoms 469 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ ↔ 𝑞 ∥ 𝑥)) |
23 | | prmnn 15388 |
. . . . . . . . . . . . . 14
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
24 | | nnuz 11723 |
. . . . . . . . . . . . . 14
⊢ ℕ =
(ℤ≥‘1) |
25 | 23, 24 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘1)) |
26 | | nnz 11399 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℤ) |
27 | | elfz5 12334 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝑥 ∈ ℤ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
28 | 25, 26, 27 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (𝑞 ∈ (1...𝑥) ↔ 𝑞 ≤ 𝑥)) |
29 | 20, 22, 28 | 3imtr4d 283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑞 pCnt 𝑥) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
30 | 17, 29 | sylbid 230 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℕ ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) ∈ ℕ → 𝑞 ∈ (1...𝑥))) |
31 | 30 | expimpd 629 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℕ → ((𝑞 ∈ ℙ ∧ ((𝑀‘𝑥)‘𝑞) ∈ ℕ) → 𝑞 ∈ (1...𝑥))) |
32 | 15, 31 | sylbid 230 |
. . . . . . . 8
⊢ (𝑥 ∈ ℕ → (𝑞 ∈ (◡(𝑀‘𝑥) “ ℕ) → 𝑞 ∈ (1...𝑥))) |
33 | 32 | ssrdv 3609 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) |
34 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...𝑥) ∈ Fin
∧ (◡(𝑀‘𝑥) “ ℕ) ⊆ (1...𝑥)) → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
35 | 12, 33, 34 | sylancr 695 |
. . . . . 6
⊢ (𝑥 ∈ ℕ → (◡(𝑀‘𝑥) “ ℕ) ∈
Fin) |
36 | | cnveq 5296 |
. . . . . . . . 9
⊢ (𝑒 = (𝑀‘𝑥) → ◡𝑒 = ◡(𝑀‘𝑥)) |
37 | 36 | imaeq1d 5465 |
. . . . . . . 8
⊢ (𝑒 = (𝑀‘𝑥) → (◡𝑒 “ ℕ) = (◡(𝑀‘𝑥) “ ℕ)) |
38 | 37 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑒 = (𝑀‘𝑥) → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
39 | | 1arith.2 |
. . . . . . 7
⊢ 𝑅 = {𝑒 ∈ (ℕ0
↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈
Fin} |
40 | 38, 39 | elrab2 3366 |
. . . . . 6
⊢ ((𝑀‘𝑥) ∈ 𝑅 ↔ ((𝑀‘𝑥) ∈ (ℕ0
↑𝑚 ℙ) ∧ (◡(𝑀‘𝑥) “ ℕ) ∈
Fin)) |
41 | 11, 35, 40 | sylanbrc 698 |
. . . . 5
⊢ (𝑥 ∈ ℕ → (𝑀‘𝑥) ∈ 𝑅) |
42 | 41 | rgen 2922 |
. . . 4
⊢
∀𝑥 ∈
ℕ (𝑀‘𝑥) ∈ 𝑅 |
43 | | ffnfv 6388 |
. . . 4
⊢ (𝑀:ℕ⟶𝑅 ↔ (𝑀 Fn ℕ ∧ ∀𝑥 ∈ ℕ (𝑀‘𝑥) ∈ 𝑅)) |
44 | 7, 42, 43 | mpbir2an 955 |
. . 3
⊢ 𝑀:ℕ⟶𝑅 |
45 | 16 | adantlr 751 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑥)‘𝑞) = (𝑞 pCnt 𝑥)) |
46 | 6 | 1arithlem2 15628 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
47 | 46 | adantll 750 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → ((𝑀‘𝑦)‘𝑞) = (𝑞 pCnt 𝑦)) |
48 | 45, 47 | eqeq12d 2637 |
. . . . . . 7
⊢ (((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) ∧ 𝑞 ∈ ℙ) → (((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
49 | 48 | ralbidva 2985 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) →
(∀𝑞 ∈ ℙ
((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞) ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
50 | 6 | 1arithlem3 15629 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑀‘𝑦):ℙ⟶ℕ0) |
51 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑀‘𝑦):ℙ⟶ℕ0 →
(𝑀‘𝑦) Fn ℙ) |
52 | | eqfnfv 6311 |
. . . . . . . 8
⊢ (((𝑀‘𝑥) Fn ℙ ∧ (𝑀‘𝑦) Fn ℙ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
53 | 13, 51, 52 | syl2an 494 |
. . . . . . 7
⊢ (((𝑀‘𝑥):ℙ⟶ℕ0 ∧
(𝑀‘𝑦):ℙ⟶ℕ0) →
((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
54 | 8, 50, 53 | syl2an 494 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ ∀𝑞 ∈ ℙ ((𝑀‘𝑥)‘𝑞) = ((𝑀‘𝑦)‘𝑞))) |
55 | | nnnn0 11299 |
. . . . . . 7
⊢ (𝑥 ∈ ℕ → 𝑥 ∈
ℕ0) |
56 | | nnnn0 11299 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
57 | | pc11 15584 |
. . . . . . 7
⊢ ((𝑥 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
58 | 55, 56, 57 | syl2an 494 |
. . . . . 6
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 = 𝑦 ↔ ∀𝑞 ∈ ℙ (𝑞 pCnt 𝑥) = (𝑞 pCnt 𝑦))) |
59 | 49, 54, 58 | 3bitr4d 300 |
. . . . 5
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) ↔ 𝑥 = 𝑦)) |
60 | 59 | biimpd 219 |
. . . 4
⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦)) |
61 | 60 | rgen2a 2977 |
. . 3
⊢
∀𝑥 ∈
ℕ ∀𝑦 ∈
ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦) |
62 | | dff13 6512 |
. . 3
⊢ (𝑀:ℕ–1-1→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑥 ∈ ℕ ∀𝑦 ∈ ℕ ((𝑀‘𝑥) = (𝑀‘𝑦) → 𝑥 = 𝑦))) |
63 | 44, 61, 62 | mpbir2an 955 |
. 2
⊢ 𝑀:ℕ–1-1→𝑅 |
64 | | eqid 2622 |
. . . . . 6
⊢ (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) = (𝑔 ∈ ℕ ↦ if(𝑔 ∈ ℙ, (𝑔↑(𝑓‘𝑔)), 1)) |
65 | | cnveq 5296 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝑓 → ◡𝑒 = ◡𝑓) |
66 | 65 | imaeq1d 5465 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝑓 → (◡𝑒 “ ℕ) = (◡𝑓 “ ℕ)) |
67 | 66 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑒 = 𝑓 → ((◡𝑒 “ ℕ) ∈ Fin ↔ (◡𝑓 “ ℕ) ∈
Fin)) |
68 | 67, 39 | elrab2 3366 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑅 ↔ (𝑓 ∈ (ℕ0
↑𝑚 ℙ) ∧ (◡𝑓 “ ℕ) ∈
Fin)) |
69 | 68 | simplbi 476 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → 𝑓 ∈ (ℕ0
↑𝑚 ℙ)) |
70 | 9, 4 | elmap 7886 |
. . . . . . . 8
⊢ (𝑓 ∈ (ℕ0
↑𝑚 ℙ) ↔ 𝑓:ℙ⟶ℕ0) |
71 | 69, 70 | sylib 208 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → 𝑓:ℙ⟶ℕ0) |
72 | 71 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑓:ℙ⟶ℕ0) |
73 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 𝑦 ∈ ℝ) |
74 | | 0re 10040 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
75 | | ifcl 4130 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧ 0 ∈
ℝ) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
76 | 73, 74, 75 | sylancl 694 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
77 | | max1 12016 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
78 | 74, 73, 77 | sylancr 695 |
. . . . . . . 8
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
79 | | flge0nn0 12621 |
. . . . . . . 8
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
𝑦, 𝑦, 0)) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
80 | 76, 78, 79 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → (⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈
ℕ0) |
81 | | nn0p1nn 11332 |
. . . . . . 7
⊢
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) ∈ ℕ0 →
((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
82 | 80, 81 | syl 17 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
83 | 73 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ∈ ℝ) |
84 | 82 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℕ) |
85 | 84 | nnred 11035 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ∈ ℝ) |
86 | | zssre 11384 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℝ |
87 | 3, 86 | sstri 3612 |
. . . . . . . . . . 11
⊢ ℙ
⊆ ℝ |
88 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℙ) |
89 | 87, 88 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑞 ∈ ℝ) |
90 | 76 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
91 | | max2 12018 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 𝑦
∈ ℝ) → 𝑦
≤ if(0 ≤ 𝑦, 𝑦, 0)) |
92 | 74, 83, 91 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
93 | | flltp1 12601 |
. . . . . . . . . . . 12
⊢ (if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
94 | 90, 93 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → if(0 ≤ 𝑦, 𝑦, 0) < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
95 | 83, 90, 85, 92, 94 | lelttrd 10195 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1)) |
96 | | simprr 796 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((⌊‘if(0 ≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞) |
97 | 83, 85, 89, 95, 96 | ltletrd 10197 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑦 < 𝑞) |
98 | 83, 89 | ltnled 10184 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑦 < 𝑞 ↔ ¬ 𝑞 ≤ 𝑦)) |
99 | 97, 98 | mpbid 222 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ 𝑞 ≤ 𝑦) |
100 | 88 | biantrurd 529 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
101 | 72 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → 𝑓:ℙ⟶ℕ0) |
102 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝑓:ℙ⟶ℕ0 →
𝑓 Fn
ℙ) |
103 | | elpreima 6337 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ℙ → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
104 | 101, 102,
103 | 3syl 18 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) ↔ (𝑞 ∈ ℙ ∧ (𝑓‘𝑞) ∈ ℕ))) |
105 | 100, 104 | bitr4d 271 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ↔ 𝑞 ∈ (◡𝑓 “ ℕ))) |
106 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
107 | | breq1 4656 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑞 → (𝑘 ≤ 𝑦 ↔ 𝑞 ≤ 𝑦)) |
108 | 107 | rspccv 3306 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
(◡𝑓 “ ℕ)𝑘 ≤ 𝑦 → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
109 | 106, 108 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑞 ∈ (◡𝑓 “ ℕ) → 𝑞 ≤ 𝑦)) |
110 | 105, 109 | sylbid 230 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ → 𝑞 ≤ 𝑦)) |
111 | 99, 110 | mtod 189 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ¬ (𝑓‘𝑞) ∈ ℕ) |
112 | 101, 88 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) ∈
ℕ0) |
113 | | elnn0 11294 |
. . . . . . . . 9
⊢ ((𝑓‘𝑞) ∈ ℕ0 ↔ ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
114 | 112, 113 | sylib 208 |
. . . . . . . 8
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → ((𝑓‘𝑞) ∈ ℕ ∨ (𝑓‘𝑞) = 0)) |
115 | 114 | ord 392 |
. . . . . . 7
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (¬ (𝑓‘𝑞) ∈ ℕ → (𝑓‘𝑞) = 0)) |
116 | 111, 115 | mpd 15 |
. . . . . 6
⊢ ((((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) ∧ (𝑞 ∈ ℙ ∧ ((⌊‘if(0
≤ 𝑦, 𝑦, 0)) + 1) ≤ 𝑞)) → (𝑓‘𝑞) = 0) |
117 | 6, 64, 72, 82, 116 | 1arithlem4 15630 |
. . . . 5
⊢ (((𝑓 ∈ 𝑅 ∧ 𝑦 ∈ ℝ) ∧ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
118 | | cnvimass 5485 |
. . . . . . 7
⊢ (◡𝑓 “ ℕ) ⊆ dom 𝑓 |
119 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝑓:ℙ⟶ℕ0 →
dom 𝑓 =
ℙ) |
120 | 71, 119 | syl 17 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 = ℙ) |
121 | 120, 87 | syl6eqss 3655 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑅 → dom 𝑓 ⊆ ℝ) |
122 | 118, 121 | syl5ss 3614 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ⊆
ℝ) |
123 | 68 | simprbi 480 |
. . . . . 6
⊢ (𝑓 ∈ 𝑅 → (◡𝑓 “ ℕ) ∈
Fin) |
124 | | fimaxre2 10969 |
. . . . . 6
⊢ (((◡𝑓 “ ℕ) ⊆ ℝ ∧
(◡𝑓 “ ℕ) ∈ Fin) →
∃𝑦 ∈ ℝ
∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
125 | 122, 123,
124 | syl2anc 693 |
. . . . 5
⊢ (𝑓 ∈ 𝑅 → ∃𝑦 ∈ ℝ ∀𝑘 ∈ (◡𝑓 “ ℕ)𝑘 ≤ 𝑦) |
126 | 117, 125 | r19.29a 3078 |
. . . 4
⊢ (𝑓 ∈ 𝑅 → ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥)) |
127 | 126 | rgen 2922 |
. . 3
⊢
∀𝑓 ∈
𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥) |
128 | | dffo3 6374 |
. . 3
⊢ (𝑀:ℕ–onto→𝑅 ↔ (𝑀:ℕ⟶𝑅 ∧ ∀𝑓 ∈ 𝑅 ∃𝑥 ∈ ℕ 𝑓 = (𝑀‘𝑥))) |
129 | 44, 127, 128 | mpbir2an 955 |
. 2
⊢ 𝑀:ℕ–onto→𝑅 |
130 | | df-f1o 5895 |
. 2
⊢ (𝑀:ℕ–1-1-onto→𝑅 ↔ (𝑀:ℕ–1-1→𝑅 ∧ 𝑀:ℕ–onto→𝑅)) |
131 | 63, 129, 130 | mpbir2an 955 |
1
⊢ 𝑀:ℕ–1-1-onto→𝑅 |