Metamath Proof Explorer

Theorem chteq0

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

Ref Expression
Assertion chteq0 ⊢ 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 chtrpcl ⊢ 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 chtlepsi ⊢ A ∈ ℝ → θ ⁡ A ≤ ψ ⁡ A
10 9 adantr ⊢ A ∈ ℝ ∧ A < 2 → θ ⁡ A ≤ ψ ⁡ A
11 chpeq0 ⊢ A ∈ ℝ → ψ ⁡ A = 0 ↔ A < 2
12 11 biimpar ⊢ A ∈ ℝ ∧ A < 2 → ψ ⁡ A = 0
13 10 12 breqtrd ⊢ A ∈ ℝ ∧ A < 2 → θ ⁡ A ≤ 0
14 chtge0 ⊢ A ∈ ℝ → 0 ≤ θ ⁡ A
15 14 adantr ⊢ A ∈ ℝ ∧ A < 2 → 0 ≤ θ ⁡ A
16 chtcl ⊢ A ∈ ℝ → θ ⁡ A ∈ ℝ
17 16 adantr ⊢ A ∈ ℝ ∧ A < 2 → θ ⁡ A ∈ ℝ
18 0re ⊢ 0 ∈ ℝ
19 letri3 ⊢ θ ⁡ A ∈ ℝ ∧ 0 ∈ ℝ → θ ⁡ A = 0 ↔ θ ⁡ A ≤ 0 ∧ 0 ≤ θ ⁡ A
20 17 18 19 sylancl ⊢ A ∈ ℝ ∧ A < 2 → θ ⁡ A = 0 ↔ θ ⁡ A ≤ 0 ∧ 0 ≤ θ ⁡ A
21 13 15 20 mpbir2and ⊢ A ∈ ℝ ∧ A < 2 → θ ⁡ A = 0
22 21 ex ⊢ A ∈ ℝ → A < 2 → θ ⁡ A = 0
23 8 22 impbid ⊢ A ∈ ℝ → θ ⁡ A = 0 ↔ A < 2