This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ppieq0

Description: The prime-counting function ppi is zero iff its argument is less than 2 . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion ppieq0 ( 𝐴 ∈ ℝ → ( ( π ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 lenlt ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
4 ppinncl ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ∈ ℕ )
5 4 nnne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( π ‘ 𝐴 ) ≠ 0 )
6 5 ex ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 → ( π ‘ 𝐴 ) ≠ 0 ) )
7 3 6 sylbird ⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 2 → ( π ‘ 𝐴 ) ≠ 0 ) )
8 7 necon4bd ⊢ ( 𝐴 ∈ ℝ → ( ( π ‘ 𝐴 ) = 0 → 𝐴 < 2 ) )
9 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
10 9 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
11 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → 1 ∈ ℝ )
12 2z ⊢ 2 ∈ ℤ
13 fllt ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℤ ) → ( 𝐴 < 2 ↔ ( ⌊ ‘ 𝐴 ) < 2 ) )
14 12 13 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 2 ↔ ( ⌊ ‘ 𝐴 ) < 2 ) )
15 14 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) < 2 )
16 df-2 ⊢ 2 = ( 1 + 1 )
17 15 16 breqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) )
18 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
19 18 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
20 1z ⊢ 1 ∈ ℤ
21 zleltp1 ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) ) )
22 19 20 21 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) ) )
23 17 22 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ≤ 1 )
24 ppiwordi ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ≤ 1 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( π ‘ 1 ) )
25 10 11 23 24 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( π ‘ 1 ) )
26 ppifl ⊢ ( 𝐴 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) )
27 26 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) )
28 ppi1 ⊢ ( π ‘ 1 ) = 0
29 28 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ 1 ) = 0 )
30 25 27 29 3brtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ 𝐴 ) ≤ 0 )
31 ppicl ⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 )
32 31 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ 𝐴 ) ∈ ℕ0 )
33 nn0le0eq0 ⊢ ( ( π ‘ 𝐴 ) ∈ ℕ0 → ( ( π ‘ 𝐴 ) ≤ 0 ↔ ( π ‘ 𝐴 ) = 0 ) )
34 32 33 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ( π ‘ 𝐴 ) ≤ 0 ↔ ( π ‘ 𝐴 ) = 0 ) )
35 30 34 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( π ‘ 𝐴 ) = 0 )
36 35 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 2 → ( π ‘ 𝐴 ) = 0 ) )
37 8 36 impbid ⊢ ( 𝐴 ∈ ℝ → ( ( π ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )