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 )