This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℝ → ( ( θ ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 lenlt ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
4 chtrpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ+ )
5 4 rpne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ≠ 0 )
6 5 ex ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 → ( θ ‘ 𝐴 ) ≠ 0 ) )
7 3 6 sylbird ⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 2 → ( θ ‘ 𝐴 ) ≠ 0 ) )
8 7 necon4bd ⊢ ( 𝐴 ∈ ℝ → ( ( θ ‘ 𝐴 ) = 0 → 𝐴 < 2 ) )
9 chtlepsi ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( θ ‘ 𝐴 ) ≤ ( ψ ‘ 𝐴 ) )
11 chpeq0 ⊢ ( 𝐴 ∈ ℝ → ( ( ψ ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )
12 11 biimpar ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ 𝐴 ) = 0 )
13 10 12 breqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( θ ‘ 𝐴 ) ≤ 0 )
14 chtge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( θ ‘ 𝐴 ) )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → 0 ≤ ( θ ‘ 𝐴 ) )
16 chtcl ⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( θ ‘ 𝐴 ) ∈ ℝ )
18 0re ⊢ 0 ∈ ℝ
19 letri3 ⊢ ( ( ( θ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( θ ‘ 𝐴 ) = 0 ↔ ( ( θ ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( θ ‘ 𝐴 ) ) ) )
20 17 18 19 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ( θ ‘ 𝐴 ) = 0 ↔ ( ( θ ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( θ ‘ 𝐴 ) ) ) )
21 13 15 20 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( θ ‘ 𝐴 ) = 0 )
22 21 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 2 → ( θ ‘ 𝐴 ) = 0 ) )
23 8 22 impbid ⊢ ( 𝐴 ∈ ℝ → ( ( θ ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )