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 syl5eq
 |-  ( ( |_ ` ( 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 syl5eq
 |-  ( ( |_ ` -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 )