Metamath Proof Explorer

Theorem chpeq0

Description: The second Chebyshev function is zero iff its argument is less than 2 . (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Assertion chpeq0 ⊢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 chprpcl ⊢A∈ℝ∧2≤A→ψ⁡A∈ℝ+
5 4 rpne0d ⊢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 chpwordi ⊢A∈ℝ∧1∈ℝ∧A≤1→ψ⁡A≤ψ⁡1
25 10 11 23 24 syl3anc ⊢A∈ℝ∧A<2→ψ⁡A≤ψ⁡1
26 chpfl ⊢A∈ℝ→ψ⁡A=ψ⁡A
27 26 adantr ⊢A∈ℝ∧A<2→ψ⁡A=ψ⁡A
28 chp1 ⊢ψ⁡1=0
29 28 a1i ⊢A∈ℝ∧A<2→ψ⁡1=0
30 25 27 29 3brtr3d ⊢A∈ℝ∧A<2→ψ⁡A≤0
31 chpge0 ⊢A∈ℝ→0≤ψ⁡A
32 31 adantr ⊢A∈ℝ∧A<2→0≤ψ⁡A
33 chpcl ⊢A∈ℝ→ψ⁡A∈ℝ
34 33 adantr ⊢A∈ℝ∧A<2→ψ⁡A∈ℝ
35 0re ⊢0∈ℝ
36 letri3 ⊢ψ⁡A∈ℝ∧0∈ℝ→ψ⁡A=0↔ψ⁡A≤0∧0≤ψ⁡A
37 34 35 36 sylancl ⊢A∈ℝ∧A<2→ψ⁡A=0↔ψ⁡A≤0∧0≤ψ⁡A
38 30 32 37 mpbir2and ⊢A∈ℝ∧A<2→ψ⁡A=0
39 38 ex ⊢A∈ℝ→A<2→ψ⁡A=0
40 8 39 impbid ⊢A∈ℝ→ψ⁡A=0↔A<2