This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-ceil

Description: Example for df-ceil . (Contributed by AV, 4-Sep-2021)

Ref Expression
Assertion ex-ceil 
|- ( ( |^ ` ( 3 / 2 ) ) = 2 /\ ( |^ ` -u ( 3 / 2 ) ) = -u 1 )

Proof

Step Hyp Ref Expression
1 ex-fl 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 /\ ( |_ ` -u ( 3 / 2 ) ) = -u 2 )
2 3re 
 |-  3 e. RR
3 2 rehalfcli 
 |-  ( 3 / 2 ) e. RR
4 3 renegcli 
 |-  -u ( 3 / 2 ) e. RR
5 ceilval 
 |-  ( -u ( 3 / 2 ) e. RR -> ( |^ ` -u ( 3 / 2 ) ) = -u ( |_ ` -u -u ( 3 / 2 ) ) )
6 4 5 ax-mp 
 |-  ( |^ ` -u ( 3 / 2 ) ) = -u ( |_ ` -u -u ( 3 / 2 ) )
7 3 recni 
 |-  ( 3 / 2 ) e. CC
8 7 negnegi 
 |-  -u -u ( 3 / 2 ) = ( 3 / 2 )
9 8 eqcomi 
 |-  ( 3 / 2 ) = -u -u ( 3 / 2 )
10 9 fveq2i 
 |-  ( |_ ` ( 3 / 2 ) ) = ( |_ ` -u -u ( 3 / 2 ) )
11 10 eqeq1i 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 <-> ( |_ ` -u -u ( 3 / 2 ) ) = 1 )
12 11 biimpi 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 -> ( |_ ` -u -u ( 3 / 2 ) ) = 1 )
13 12 negeqd 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 -> -u ( |_ ` -u -u ( 3 / 2 ) ) = -u 1 )
14 6 13 eqtrid 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 -> ( |^ ` -u ( 3 / 2 ) ) = -u 1 )
15 ceilval 
 |-  ( ( 3 / 2 ) e. RR -> ( |^ ` ( 3 / 2 ) ) = -u ( |_ ` -u ( 3 / 2 ) ) )
16 3 15 ax-mp 
 |-  ( |^ ` ( 3 / 2 ) ) = -u ( |_ ` -u ( 3 / 2 ) )
17 negeq 
 |-  ( ( |_ ` -u ( 3 / 2 ) ) = -u 2 -> -u ( |_ ` -u ( 3 / 2 ) ) = -u -u 2 )
18 2cn 
 |-  2 e. CC
19 18 negnegi 
 |-  -u -u 2 = 2
20 17 19 eqtrdi 
 |-  ( ( |_ ` -u ( 3 / 2 ) ) = -u 2 -> -u ( |_ ` -u ( 3 / 2 ) ) = 2 )
21 16 20 eqtrid 
 |-  ( ( |_ ` -u ( 3 / 2 ) ) = -u 2 -> ( |^ ` ( 3 / 2 ) ) = 2 )
22 14 21 anim12ci 
 |-  ( ( ( |_ ` ( 3 / 2 ) ) = 1 /\ ( |_ ` -u ( 3 / 2 ) ) = -u 2 ) -> ( ( |^ ` ( 3 / 2 ) ) = 2 /\ ( |^ ` -u ( 3 / 2 ) ) = -u 1 ) )
23 1 22 ax-mp 
 |-  ( ( |^ ` ( 3 / 2 ) ) = 2 /\ ( |^ ` -u ( 3 / 2 ) ) = -u 1 )