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 ) |