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