# 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}\in ℝ\to \left(\underset{_}{\pi }\left({A}\right)=0↔{A}<2\right)$

### Proof

Step Hyp Ref Expression
1 2re ${⊢}2\in ℝ$
2 lenlt ${⊢}\left(2\in ℝ\wedge {A}\in ℝ\right)\to \left(2\le {A}↔¬{A}<2\right)$
3 1 2 mpan ${⊢}{A}\in ℝ\to \left(2\le {A}↔¬{A}<2\right)$
4 ppinncl ${⊢}\left({A}\in ℝ\wedge 2\le {A}\right)\to \underset{_}{\pi }\left({A}\right)\in ℕ$
5 4 nnne0d ${⊢}\left({A}\in ℝ\wedge 2\le {A}\right)\to \underset{_}{\pi }\left({A}\right)\ne 0$
6 5 ex ${⊢}{A}\in ℝ\to \left(2\le {A}\to \underset{_}{\pi }\left({A}\right)\ne 0\right)$
7 3 6 sylbird ${⊢}{A}\in ℝ\to \left(¬{A}<2\to \underset{_}{\pi }\left({A}\right)\ne 0\right)$
8 7 necon4bd ${⊢}{A}\in ℝ\to \left(\underset{_}{\pi }\left({A}\right)=0\to {A}<2\right)$
9 reflcl ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℝ$
10 9 adantr ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to ⌊{A}⌋\in ℝ$
11 1red ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to 1\in ℝ$
12 2z ${⊢}2\in ℤ$
13 fllt ${⊢}\left({A}\in ℝ\wedge 2\in ℤ\right)\to \left({A}<2↔⌊{A}⌋<2\right)$
14 12 13 mpan2 ${⊢}{A}\in ℝ\to \left({A}<2↔⌊{A}⌋<2\right)$
15 14 biimpa ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to ⌊{A}⌋<2$
16 df-2 ${⊢}2=1+1$
17 15 16 breqtrdi ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to ⌊{A}⌋<1+1$
18 flcl ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℤ$
19 18 adantr ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to ⌊{A}⌋\in ℤ$
20 1z ${⊢}1\in ℤ$
21 zleltp1 ${⊢}\left(⌊{A}⌋\in ℤ\wedge 1\in ℤ\right)\to \left(⌊{A}⌋\le 1↔⌊{A}⌋<1+1\right)$
22 19 20 21 sylancl ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \left(⌊{A}⌋\le 1↔⌊{A}⌋<1+1\right)$
23 17 22 mpbird ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to ⌊{A}⌋\le 1$
24 ppiwordi ${⊢}\left(⌊{A}⌋\in ℝ\wedge 1\in ℝ\wedge ⌊{A}⌋\le 1\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)\le \underset{_}{\pi }\left(1\right)$
25 10 11 23 24 syl3anc ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)\le \underset{_}{\pi }\left(1\right)$
26 ppifl ${⊢}{A}\in ℝ\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left({A}\right)$
27 26 adantr ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left({A}\right)$
28 ppi1 ${⊢}\underset{_}{\pi }\left(1\right)=0$
29 28 a1i ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left(1\right)=0$
30 25 27 29 3brtr3d ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left({A}\right)\le 0$
31 ppicl ${⊢}{A}\in ℝ\to \underset{_}{\pi }\left({A}\right)\in {ℕ}_{0}$
32 31 adantr ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left({A}\right)\in {ℕ}_{0}$
33 nn0le0eq0 ${⊢}\underset{_}{\pi }\left({A}\right)\in {ℕ}_{0}\to \left(\underset{_}{\pi }\left({A}\right)\le 0↔\underset{_}{\pi }\left({A}\right)=0\right)$
34 32 33 syl ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \left(\underset{_}{\pi }\left({A}\right)\le 0↔\underset{_}{\pi }\left({A}\right)=0\right)$
35 30 34 mpbid ${⊢}\left({A}\in ℝ\wedge {A}<2\right)\to \underset{_}{\pi }\left({A}\right)=0$
36 35 ex ${⊢}{A}\in ℝ\to \left({A}<2\to \underset{_}{\pi }\left({A}\right)=0\right)$
37 8 36 impbid ${⊢}{A}\in ℝ\to \left(\underset{_}{\pi }\left({A}\right)=0↔{A}<2\right)$