Metamath Proof Explorer

Theorem dfceil2

Description: Alternative definition of the ceiling function using restricted iota. (Contributed by AV, 1-Dec-2018)

Ref Expression
Assertion dfceil2 
|- |^ = ( x e. RR |-> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-ceil 
 |-  |^ = ( x e. RR |-> -u ( |_ ` -u x ) )
2 zre 
 |-  ( z e. ZZ -> z e. RR )
3 lenegcon2 
 |-  ( ( x e. RR /\ z e. RR ) -> ( x <_ -u z <-> z <_ -u x ) )
4 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
5 4 anim1ci 
 |-  ( ( x e. RR /\ z e. RR ) -> ( z e. RR /\ ( x + 1 ) e. RR ) )
6 ltnegcon1 
 |-  ( ( z e. RR /\ ( x + 1 ) e. RR ) -> ( -u z < ( x + 1 ) <-> -u ( x + 1 ) < z ) )
7 5 6 syl 
 |-  ( ( x e. RR /\ z e. RR ) -> ( -u z < ( x + 1 ) <-> -u ( x + 1 ) < z ) )
8 recn 
 |-  ( x e. RR -> x e. CC )
9 1cnd 
 |-  ( x e. RR -> 1 e. CC )
10 8 9 negdid 
 |-  ( x e. RR -> -u ( x + 1 ) = ( -u x + -u 1 ) )
11 10 adantr 
 |-  ( ( x e. RR /\ z e. RR ) -> -u ( x + 1 ) = ( -u x + -u 1 ) )
12 11 breq1d 
 |-  ( ( x e. RR /\ z e. RR ) -> ( -u ( x + 1 ) < z <-> ( -u x + -u 1 ) < z ) )
13 renegcl 
 |-  ( x e. RR -> -u x e. RR )
14 13 adantr 
 |-  ( ( x e. RR /\ z e. RR ) -> -u x e. RR )
15 neg1rr 
 |-  -u 1 e. RR
16 15 a1i 
 |-  ( ( x e. RR /\ z e. RR ) -> -u 1 e. RR )
17 simpr 
 |-  ( ( x e. RR /\ z e. RR ) -> z e. RR )
18 14 16 17 ltaddsubd 
 |-  ( ( x e. RR /\ z e. RR ) -> ( ( -u x + -u 1 ) < z <-> -u x < ( z - -u 1 ) ) )
19 recn 
 |-  ( z e. RR -> z e. CC )
20 1cnd 
 |-  ( z e. RR -> 1 e. CC )
21 19 20 subnegd 
 |-  ( z e. RR -> ( z - -u 1 ) = ( z + 1 ) )
22 21 adantl 
 |-  ( ( x e. RR /\ z e. RR ) -> ( z - -u 1 ) = ( z + 1 ) )
23 22 breq2d 
 |-  ( ( x e. RR /\ z e. RR ) -> ( -u x < ( z - -u 1 ) <-> -u x < ( z + 1 ) ) )
24 18 23 bitrd 
 |-  ( ( x e. RR /\ z e. RR ) -> ( ( -u x + -u 1 ) < z <-> -u x < ( z + 1 ) ) )
25 7 12 24 3bitrd 
 |-  ( ( x e. RR /\ z e. RR ) -> ( -u z < ( x + 1 ) <-> -u x < ( z + 1 ) ) )
26 3 25 anbi12d 
 |-  ( ( x e. RR /\ z e. RR ) -> ( ( x <_ -u z /\ -u z < ( x + 1 ) ) <-> ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
27 2 26 sylan2 
 |-  ( ( x e. RR /\ z e. ZZ ) -> ( ( x <_ -u z /\ -u z < ( x + 1 ) ) <-> ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
28 27 riotabidva 
 |-  ( x e. RR -> ( iota_ z e. ZZ ( x <_ -u z /\ -u z < ( x + 1 ) ) ) = ( iota_ z e. ZZ ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
29 28 negeqd 
 |-  ( x e. RR -> -u ( iota_ z e. ZZ ( x <_ -u z /\ -u z < ( x + 1 ) ) ) = -u ( iota_ z e. ZZ ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
30 zbtwnre 
 |-  ( x e. RR -> E! y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) )
31 breq2 
 |-  ( y = -u z -> ( x <_ y <-> x <_ -u z ) )
32 breq1 
 |-  ( y = -u z -> ( y < ( x + 1 ) <-> -u z < ( x + 1 ) ) )
33 31 32 anbi12d 
 |-  ( y = -u z -> ( ( x <_ y /\ y < ( x + 1 ) ) <-> ( x <_ -u z /\ -u z < ( x + 1 ) ) ) )
34 33 zriotaneg 
 |-  ( E! y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) -> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) = -u ( iota_ z e. ZZ ( x <_ -u z /\ -u z < ( x + 1 ) ) ) )
35 30 34 syl 
 |-  ( x e. RR -> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) = -u ( iota_ z e. ZZ ( x <_ -u z /\ -u z < ( x + 1 ) ) ) )
36 flval 
 |-  ( -u x e. RR -> ( |_ ` -u x ) = ( iota_ z e. ZZ ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
37 13 36 syl 
 |-  ( x e. RR -> ( |_ ` -u x ) = ( iota_ z e. ZZ ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
38 37 negeqd 
 |-  ( x e. RR -> -u ( |_ ` -u x ) = -u ( iota_ z e. ZZ ( z <_ -u x /\ -u x < ( z + 1 ) ) ) )
39 29 35 38 3eqtr4rd 
 |-  ( x e. RR -> -u ( |_ ` -u x ) = ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )
40 39 mpteq2ia 
 |-  ( x e. RR |-> -u ( |_ ` -u x ) ) = ( x e. RR |-> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )
41 1 40 eqtri 
 |-  |^ = ( x e. RR |-> ( iota_ y e. ZZ ( x <_ y /\ y < ( x + 1 ) ) ) )