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 A - A - 1 < A

Proof

Step Hyp Ref Expression
1 renegcl A A
2 reflcl A A
3 1 2 syl A A
4 3 recnd A A
5 ax-1cn 1
6 negdi A 1 A + 1 = - A + -1
7 4 5 6 sylancl A A + 1 = - A + -1
8 4 negcld A A
9 negsub A 1 - A + -1 = - A - 1
10 8 5 9 sylancl A - A + -1 = - A - 1
11 7 10 eqtr2d A - A - 1 = A + 1
12 peano2re A A + 1
13 3 12 syl A A + 1
14 flltp1 A A < A + 1
15 1 14 syl A A < A + 1
16 15 adantr A A + 1 A < A + 1
17 ltnegcon1 A A + 1 A < A + 1 A + 1 < A
18 16 17 mpbid A A + 1 A + 1 < A
19 13 18 mpdan A A + 1 < A
20 11 19 eqbrtrd A - A - 1 < A