Metamath Proof Explorer

Theorem dnibndlem10

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibndlem10.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dnibndlem10.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dnibndlem10.3 ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) )
Assertion dnibndlem10 ( 𝜑 → 1 ≤ ( 𝐵 − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dnibndlem10.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dnibndlem10.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dnibndlem10.3 ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ≤ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) )
4 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
5 halfre ⊢ ( 1 / 2 ) ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
7 2 6 readdcld ⊢ ( 𝜑 → ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ )
8 reflcl ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ )
10 9 6 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
11 resubcl ⊢ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
12 10 11 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ )
13 1 6 readdcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
14 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
15 13 14 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
16 15 6 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ )
17 12 16 jca ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ ) )
18 resubcl ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) ∈ ℝ )
19 17 18 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) ∈ ℝ )
20 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
21 15 recnd ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
22 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
23 6 recnd ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
24 21 22 23 addsubassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 2 − ( 1 / 2 ) ) ) )
25 24 oveq1d ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 2 − ( 1 / 2 ) ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
26 22 23 subcld ⊢ ( 𝜑 → ( 2 − ( 1 / 2 ) ) ∈ ℂ )
27 21 26 23 pnpcand ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 2 − ( 1 / 2 ) ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = ( ( 2 − ( 1 / 2 ) ) − ( 1 / 2 ) ) )
28 22 23 23 subsub4d ⊢ ( 𝜑 → ( ( 2 − ( 1 / 2 ) ) − ( 1 / 2 ) ) = ( 2 − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
29 ax-1cn ⊢ 1 ∈ ℂ
30 2halves ⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
31 29 30 ax-mp ⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
32 31 a1i ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
33 32 oveq2d ⊢ ( 𝜑 → ( 2 − ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( 2 − 1 ) )
34 2m1e1 ⊢ ( 2 − 1 ) = 1
35 34 a1i ⊢ ( 𝜑 → ( 2 − 1 ) = 1 )
36 28 33 35 3eqtrd ⊢ ( 𝜑 → ( ( 2 − ( 1 / 2 ) ) − ( 1 / 2 ) ) = 1 )
37 25 27 36 3eqtrd ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) = 1 )
38 37 eqcomd ⊢ ( 𝜑 → 1 = ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
39 2re ⊢ 2 ∈ ℝ
40 39 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
41 15 40 readdcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ∈ ℝ )
42 41 6 jca ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
43 resubcl ⊢ ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) ∈ ℝ )
44 42 43 syl ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) ∈ ℝ )
45 41 9 6 3 lesub1dd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) )
46 44 12 16 45 lesub1dd ⊢ ( 𝜑 → ( ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 2 ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) ≤ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
47 38 46 eqbrtrd ⊢ ( 𝜑 → 1 ≤ ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) )
48 flle ⊢ ( ( 𝐵 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) )
49 7 48 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) )
50 9 6 2 lesubaddd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ≤ 𝐵 ↔ ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) ≤ ( 𝐵 + ( 1 / 2 ) ) ) )
51 49 50 mpbird ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) ≤ 𝐵 )
52 fllep1 ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
53 13 52 syl ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
54 21 23 23 addassd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
55 32 oveq2d ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
56 54 55 eqtrd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
57 56 eqcomd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
58 53 57 breqtrd ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
59 1 16 6 leadd1d ⊢ ( 𝜑 → ( 𝐴 ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ↔ ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) )
60 58 59 mpbird ⊢ ( 𝜑 → 𝐴 ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
61 12 1 2 16 51 60 le2subd ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐵 + ( 1 / 2 ) ) ) − ( 1 / 2 ) ) − ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ) ≤ ( 𝐵 − 𝐴 ) )
62 4 19 20 47 61 letrd ⊢ ( 𝜑 → 1 ≤ ( 𝐵 − 𝐴 ) )