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