Step |
Hyp |
Ref |
Expression |
1 |
|
rpre |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) |
2 |
|
ppicl |
⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 ) |
3 |
1 2
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) ∈ ℕ0 ) |
4 |
3
|
nn0red |
⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) ∈ ℝ ) |
5 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) ∈ ℝ ) |
6 |
|
reflcl |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
7 |
1 6
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
8 |
7
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ ) |
9 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℝ ) |
10 |
|
fzfi |
⊢ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin |
11 |
|
inss1 |
⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) |
12 |
|
2eluzge1 |
⊢ 2 ∈ ( ℤ≥ ‘ 1 ) |
13 |
|
fzss1 |
⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
14 |
12 13
|
mp1i |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
15 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ ) |
16 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
17 |
15 16
|
eleqtrdi |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) ) |
18 |
|
eluzfz1 |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
19 |
17 18
|
syl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
20 |
|
1lt2 |
⊢ 1 < 2 |
21 |
|
1re |
⊢ 1 ∈ ℝ |
22 |
|
2re |
⊢ 2 ∈ ℝ |
23 |
21 22
|
ltnlei |
⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 ) |
24 |
20 23
|
mpbi |
⊢ ¬ 2 ≤ 1 |
25 |
|
elfzle1 |
⊢ ( 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) → 2 ≤ 1 ) |
26 |
24 25
|
mto |
⊢ ¬ 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) |
27 |
|
nelne1 |
⊢ ( ( 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ¬ 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) |
28 |
19 26 27
|
sylancl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) |
29 |
28
|
necomd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
30 |
|
df-pss |
⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ) |
31 |
14 29 30
|
sylanbrc |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
32 |
|
sspsstr |
⊢ ( ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
33 |
11 31 32
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
34 |
|
php3 |
⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
35 |
10 33 34
|
sylancr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
36 |
|
fzfi |
⊢ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin |
37 |
|
ssfi |
⊢ ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ) |
38 |
36 11 37
|
mp2an |
⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin |
39 |
|
hashsdom |
⊢ ( ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ) |
40 |
38 10 39
|
mp2an |
⊢ ( ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) |
41 |
35 40
|
sylibr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ) |
42 |
1
|
flcld |
⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
43 |
|
ppival2 |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) ) |
44 |
42 43
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) ) |
45 |
|
ppifl |
⊢ ( 𝐴 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) ) |
46 |
1 45
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) ) |
47 |
44 46
|
eqtr3d |
⊢ ( 𝐴 ∈ ℝ+ → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) = ( π ‘ 𝐴 ) ) |
48 |
47
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) = ( π ‘ 𝐴 ) ) |
49 |
|
rpge0 |
⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 ) |
50 |
|
flge0nn0 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ) |
51 |
1 49 50
|
syl2anc |
⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ) |
52 |
|
hashfz1 |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) ) |
53 |
51 52
|
syl |
⊢ ( 𝐴 ∈ ℝ+ → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) ) |
54 |
53
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) ) |
55 |
41 48 54
|
3brtr3d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) < ( ⌊ ‘ 𝐴 ) ) |
56 |
|
flle |
⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
57 |
9 56
|
syl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ) |
58 |
5 8 9 55 57
|
ltletrd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) < 𝐴 ) |
59 |
46
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) ) |
60 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ 𝐴 ) = 0 ) |
61 |
60
|
fveq2d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 0 ) ) |
62 |
|
2pos |
⊢ 0 < 2 |
63 |
|
0re |
⊢ 0 ∈ ℝ |
64 |
|
ppieq0 |
⊢ ( 0 ∈ ℝ → ( ( π ‘ 0 ) = 0 ↔ 0 < 2 ) ) |
65 |
63 64
|
ax-mp |
⊢ ( ( π ‘ 0 ) = 0 ↔ 0 < 2 ) |
66 |
62 65
|
mpbir |
⊢ ( π ‘ 0 ) = 0 |
67 |
61 66
|
eqtrdi |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = 0 ) |
68 |
59 67
|
eqtr3d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ 𝐴 ) = 0 ) |
69 |
|
rpgt0 |
⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 ) |
70 |
69
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → 0 < 𝐴 ) |
71 |
68 70
|
eqbrtrd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ 𝐴 ) < 𝐴 ) |
72 |
|
elnn0 |
⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ ∨ ( ⌊ ‘ 𝐴 ) = 0 ) ) |
73 |
51 72
|
sylib |
⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ 𝐴 ) ∈ ℕ ∨ ( ⌊ ‘ 𝐴 ) = 0 ) ) |
74 |
58 71 73
|
mpjaodan |
⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) < 𝐴 ) |