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 ) )