Metamath Proof Explorer

Theorem ceim1l

Description: One less than the ceiling of a real number is strictly less than that number. (Contributed by Jeff Hankins, 10-Jun-2007)

Ref Expression
Assertion ceim1l ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
2 reflcl ⊢ ( - 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
3 1 2 syl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℝ )
4 3 recnd ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ - 𝐴 ) ∈ ℂ )
5 ax-1cn ⊢ 1 ∈ ℂ
6 negdi ⊢ ( ( ( ⌊ ‘ - 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( ⌊ ‘ - 𝐴 ) + 1 ) = ( - ( ⌊ ‘ - 𝐴 ) + - 1 ) )
7 4 5 6 sylancl ⊢ ( 𝐴 ∈ ℝ → - ( ( ⌊ ‘ - 𝐴 ) + 1 ) = ( - ( ⌊ ‘ - 𝐴 ) + - 1 ) )
8 4 negcld ⊢ ( 𝐴 ∈ ℝ → - ( ⌊ ‘ - 𝐴 ) ∈ ℂ )
9 negsub ⊢ ( ( - ( ⌊ ‘ - 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( - ( ⌊ ‘ - 𝐴 ) + - 1 ) = ( - ( ⌊ ‘ - 𝐴 ) − 1 ) )
10 8 5 9 sylancl ⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) + - 1 ) = ( - ( ⌊ ‘ - 𝐴 ) − 1 ) )
11 7 10 eqtr2d ⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) = - ( ( ⌊ ‘ - 𝐴 ) + 1 ) )
12 peano2re ⊢ ( ( ⌊ ‘ - 𝐴 ) ∈ ℝ → ( ( ⌊ ‘ - 𝐴 ) + 1 ) ∈ ℝ )
13 3 12 syl ⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ - 𝐴 ) + 1 ) ∈ ℝ )
14 flltp1 ⊢ ( - 𝐴 ∈ ℝ → - 𝐴 < ( ( ⌊ ‘ - 𝐴 ) + 1 ) )
15 1 14 syl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 < ( ( ⌊ ‘ - 𝐴 ) + 1 ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ⌊ ‘ - 𝐴 ) + 1 ) ∈ ℝ ) → - 𝐴 < ( ( ⌊ ‘ - 𝐴 ) + 1 ) )
17 ltnegcon1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ⌊ ‘ - 𝐴 ) + 1 ) ∈ ℝ ) → ( - 𝐴 < ( ( ⌊ ‘ - 𝐴 ) + 1 ) ↔ - ( ( ⌊ ‘ - 𝐴 ) + 1 ) < 𝐴 ) )
18 16 17 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( ⌊ ‘ - 𝐴 ) + 1 ) ∈ ℝ ) → - ( ( ⌊ ‘ - 𝐴 ) + 1 ) < 𝐴 )
19 13 18 mpdan ⊢ ( 𝐴 ∈ ℝ → - ( ( ⌊ ‘ - 𝐴 ) + 1 ) < 𝐴 )
20 11 19 eqbrtrd ⊢ ( 𝐴 ∈ ℝ → ( - ( ⌊ ‘ - 𝐴 ) − 1 ) < 𝐴 )