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 ⊢ A ∈ ℝ → π _ ⁡ A = 0 ↔ A < 2

Proof

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