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

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 lenlt ⊢ ( ( 2 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ ¬ 𝐴 < 2 ) )
4 chprpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ+ )
5 4 rpne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ≠ 0 )
6 5 ex ⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 → ( ψ ‘ 𝐴 ) ≠ 0 ) )
7 3 6 sylbird ⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 2 → ( ψ ‘ 𝐴 ) ≠ 0 ) )
8 7 necon4bd ⊢ ( 𝐴 ∈ ℝ → ( ( ψ ‘ 𝐴 ) = 0 → 𝐴 < 2 ) )
9 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
10 9 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
11 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → 1 ∈ ℝ )
12 2z ⊢ 2 ∈ ℤ
13 fllt ⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℤ ) → ( 𝐴 < 2 ↔ ( ⌊ ‘ 𝐴 ) < 2 ) )
14 12 13 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 2 ↔ ( ⌊ ‘ 𝐴 ) < 2 ) )
15 14 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) < 2 )
16 df-2 ⊢ 2 = ( 1 + 1 )
17 15 16 breqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) )
18 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
19 18 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
20 1z ⊢ 1 ∈ ℤ
21 zleltp1 ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) ) )
22 19 20 21 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ( ⌊ ‘ 𝐴 ) ≤ 1 ↔ ( ⌊ ‘ 𝐴 ) < ( 1 + 1 ) ) )
23 17 22 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ⌊ ‘ 𝐴 ) ≤ 1 )
24 chpwordi ⊢ ( ( ( ⌊ ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ≤ 1 ) → ( ψ ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( ψ ‘ 1 ) )
25 10 11 23 24 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ ( ⌊ ‘ 𝐴 ) ) ≤ ( ψ ‘ 1 ) )
26 chpfl ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ψ ‘ 𝐴 ) )
27 26 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ ( ⌊ ‘ 𝐴 ) ) = ( ψ ‘ 𝐴 ) )
28 chp1 ⊢ ( ψ ‘ 1 ) = 0
29 28 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ 1 ) = 0 )
30 25 27 29 3brtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ 𝐴 ) ≤ 0 )
31 chpge0 ⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ψ ‘ 𝐴 ) )
32 31 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → 0 ≤ ( ψ ‘ 𝐴 ) )
33 chpcl ⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) ∈ ℝ )
34 33 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ 𝐴 ) ∈ ℝ )
35 0re ⊢ 0 ∈ ℝ
36 letri3 ⊢ ( ( ( ψ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ψ ‘ 𝐴 ) = 0 ↔ ( ( ψ ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( ψ ‘ 𝐴 ) ) ) )
37 34 35 36 sylancl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ( ψ ‘ 𝐴 ) = 0 ↔ ( ( ψ ‘ 𝐴 ) ≤ 0 ∧ 0 ≤ ( ψ ‘ 𝐴 ) ) ) )
38 30 32 37 mpbir2and ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 2 ) → ( ψ ‘ 𝐴 ) = 0 )
39 38 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 2 → ( ψ ‘ 𝐴 ) = 0 ) )
40 8 39 impbid ⊢ ( 𝐴 ∈ ℝ → ( ( ψ ‘ 𝐴 ) = 0 ↔ 𝐴 < 2 ) )