Metamath Proof Explorer

Theorem dnibndlem5

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

Ref Expression
Assertion dnibndlem5 ( 𝐴 ∈ ℝ → 0 < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
2 halfre ⊢ ( 1 / 2 ) ∈ ℝ
3 2 a1i ⊢ ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
4 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
5 1 3 4 syl2anc2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
6 flltp1 ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) < ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
7 5 6 syl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) < ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
8 ax-1cn ⊢ 1 ∈ ℂ
9 2halves ⊢ ( 1 ∈ ℂ → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
10 8 9 ax-mp ⊢ ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
11 10 eqcomi ⊢ 1 = ( ( 1 / 2 ) + ( 1 / 2 ) )
12 11 a1i ⊢ ( 𝐴 ∈ ℝ → 1 = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
13 12 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
14 reflcl ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
15 5 14 syl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
16 15 recnd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ )
17 3 recnd ⊢ ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℂ )
18 16 17 17 3jca ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) )
19 addass ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ) → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
20 18 19 syl ⊢ ( 𝐴 ∈ ℝ → ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
21 20 eqcomd ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
22 13 21 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) = ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
23 7 22 breqtrd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
24 15 3 jca ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) )
25 readdcl ⊢ ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ )
26 24 25 syl ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ∈ ℝ )
27 1 26 3 ltadd1d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ↔ ( 𝐴 + ( 1 / 2 ) ) < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) )
28 23 27 mpbird ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
29 1 26 posdifd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) ↔ 0 < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) ) )
30 28 29 mpbid ⊢ ( 𝐴 ∈ ℝ → 0 < ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) − 𝐴 ) )