Proof of Theorem ppiltx
Step | Hyp | Ref
| Expression |
1 | | rpre 12619 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ 𝐴 ∈
ℝ) |
2 | | ppicl 26040 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(π‘𝐴)
∈ ℕ0) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) ∈
ℕ0) |
4 | 3 | nn0red 12176 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) ∈ ℝ) |
5 | 4 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) ∈ ℝ) |
6 | | reflcl 13396 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ∈
ℝ) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℝ) |
8 | 7 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈ ℝ) |
9 | 1 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → 𝐴
∈ ℝ) |
10 | | fzfi 13572 |
. . . . . 6
⊢
(1...(⌊‘𝐴)) ∈ Fin |
11 | | inss1 4158 |
. . . . . . 7
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴)) |
12 | | 2eluzge1 12515 |
. . . . . . . . 9
⊢ 2 ∈
(ℤ≥‘1) |
13 | | fzss1 13176 |
. . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘1) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
14 | 12, 13 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
15 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈ ℕ) |
16 | | nnuz 12502 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
17 | 15, 16 | eleqtrdi 2849 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ∈
(ℤ≥‘1)) |
18 | | eluzfz1 13144 |
. . . . . . . . . . 11
⊢
((⌊‘𝐴)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝐴))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → 1 ∈ (1...(⌊‘𝐴))) |
20 | | 1lt2 12026 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
21 | | 1re 10858 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
22 | | 2re 11929 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
23 | 21, 22 | ltnlei 10978 |
. . . . . . . . . . . 12
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
24 | 20, 23 | mpbi 233 |
. . . . . . . . . . 11
⊢ ¬ 2
≤ 1 |
25 | | elfzle1 13140 |
. . . . . . . . . . 11
⊢ (1 ∈
(2...(⌊‘𝐴))
→ 2 ≤ 1) |
26 | 24, 25 | mto 200 |
. . . . . . . . . 10
⊢ ¬ 1
∈ (2...(⌊‘𝐴)) |
27 | | nelne1 3039 |
. . . . . . . . . 10
⊢ ((1
∈ (1...(⌊‘𝐴)) ∧ ¬ 1 ∈
(2...(⌊‘𝐴)))
→ (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴))) |
28 | 19, 26, 27 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴))) |
29 | 28 | necomd 2997 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ≠ (1...(⌊‘𝐴))) |
30 | | df-pss 3900 |
. . . . . . . 8
⊢
((2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴)) ↔
((2...(⌊‘𝐴))
⊆ (1...(⌊‘𝐴)) ∧ (2...(⌊‘𝐴)) ≠
(1...(⌊‘𝐴)))) |
31 | 14, 29, 30 | sylanbrc 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴))) |
32 | | sspsstr 4035 |
. . . . . . 7
⊢
((((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴))
∧ (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴))) →
((2...(⌊‘𝐴))
∩ ℙ) ⊊ (1...(⌊‘𝐴))) |
33 | 11, 31, 32 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ⊊
(1...(⌊‘𝐴))) |
34 | | php3 8855 |
. . . . . 6
⊢
(((1...(⌊‘𝐴)) ∈ Fin ∧
((2...(⌊‘𝐴))
∩ ℙ) ⊊ (1...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
35 | 10, 33, 34 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
36 | | fzfi 13572 |
. . . . . . 7
⊢
(2...(⌊‘𝐴)) ∈ Fin |
37 | | ssfi 8874 |
. . . . . . 7
⊢
(((2...(⌊‘𝐴)) ∈ Fin ∧
((2...(⌊‘𝐴))
∩ ℙ) ⊆ (2...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ∈
Fin) |
38 | 36, 11, 37 | mp2an 692 |
. . . . . 6
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ∈
Fin |
39 | | hashsdom 13976 |
. . . . . 6
⊢
((((2...(⌊‘𝐴)) ∩ ℙ) ∈ Fin ∧
(1...(⌊‘𝐴))
∈ Fin) → ((♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴)))) |
40 | 38, 10, 39 | mp2an 692 |
. . . . 5
⊢
((♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺
(1...(⌊‘𝐴))) |
41 | 35, 40 | sylibr 237 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) <
(♯‘(1...(⌊‘𝐴)))) |
42 | 1 | flcld 13398 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℤ) |
43 | | ppival2 26037 |
. . . . . . 7
⊢
((⌊‘𝐴)
∈ ℤ → (π‘(⌊‘𝐴)) =
(♯‘((2...(⌊‘𝐴)) ∩ ℙ))) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (π‘(⌊‘𝐴)) =
(♯‘((2...(⌊‘𝐴)) ∩ ℙ))) |
45 | | ppifl 26069 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(π‘(⌊‘𝐴)) = (π‘𝐴)) |
46 | 1, 45 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (π‘(⌊‘𝐴)) = (π‘𝐴)) |
47 | 44, 46 | eqtr3d 2780 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) =
(π‘𝐴)) |
48 | 47 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘((2...(⌊‘𝐴)) ∩ ℙ)) =
(π‘𝐴)) |
49 | | rpge0 12624 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ+
→ 0 ≤ 𝐴) |
50 | | flge0nn0 13420 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(⌊‘𝐴) ∈
ℕ0) |
51 | 1, 49, 50 | syl2anc 587 |
. . . . . 6
⊢ (𝐴 ∈ ℝ+
→ (⌊‘𝐴)
∈ ℕ0) |
52 | | hashfz1 13940 |
. . . . . 6
⊢
((⌊‘𝐴)
∈ ℕ0 → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ+
→ (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
54 | 53 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (♯‘(1...(⌊‘𝐴))) = (⌊‘𝐴)) |
55 | 41, 48, 54 | 3brtr3d 5099 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) < (⌊‘𝐴)) |
56 | | flle 13399 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(⌊‘𝐴) ≤
𝐴) |
57 | 9, 56 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (⌊‘𝐴) ≤ 𝐴) |
58 | 5, 8, 9, 55, 57 | ltletrd 11017 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴)
∈ ℕ) → (π‘𝐴) < 𝐴) |
59 | 46 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = (π‘𝐴)) |
60 | | simpr 488 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (⌊‘𝐴)
= 0) |
61 | 60 | fveq2d 6740 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = (π‘0)) |
62 | | 2pos 11958 |
. . . . . 6
⊢ 0 <
2 |
63 | | 0re 10860 |
. . . . . . 7
⊢ 0 ∈
ℝ |
64 | | ppieq0 26085 |
. . . . . . 7
⊢ (0 ∈
ℝ → ((π‘0) = 0 ↔ 0 < 2)) |
65 | 63, 64 | ax-mp 5 |
. . . . . 6
⊢
((π‘0) = 0 ↔ 0 < 2) |
66 | 62, 65 | mpbir 234 |
. . . . 5
⊢
(π‘0) = 0 |
67 | 61, 66 | eqtrdi 2795 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘(⌊‘𝐴)) = 0) |
68 | 59, 67 | eqtr3d 2780 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘𝐴) = 0) |
69 | | rpgt0 12623 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ 0 < 𝐴) |
70 | 69 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → 0 < 𝐴) |
71 | 68, 70 | eqbrtrd 5090 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ (⌊‘𝐴) =
0) → (π‘𝐴) < 𝐴) |
72 | | elnn0 12117 |
. . 3
⊢
((⌊‘𝐴)
∈ ℕ0 ↔ ((⌊‘𝐴) ∈ ℕ ∨ (⌊‘𝐴) = 0)) |
73 | 51, 72 | sylib 221 |
. 2
⊢ (𝐴 ∈ ℝ+
→ ((⌊‘𝐴)
∈ ℕ ∨ (⌊‘𝐴) = 0)) |
74 | 58, 71, 73 | mpjaodan 959 |
1
⊢ (𝐴 ∈ ℝ+
→ (π‘𝐴) < 𝐴) |