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

Metamath Proof Explorer

Theorem ex-fl

Description: Example for df-fl . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 3re 
 |-  3 e. RR
3 2 rehalfcli 
 |-  ( 3 / 2 ) e. RR
4 2cn 
 |-  2 e. CC
5 4 mullidi 
 |-  ( 1 x. 2 ) = 2
6 2lt3 
 |-  2 < 3
7 5 6 eqbrtri 
 |-  ( 1 x. 2 ) < 3
8 2pos 
 |-  0 < 2
9 2re 
 |-  2 e. RR
10 1 2 9 ltmuldivi 
 |-  ( 0 < 2 -> ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) ) )
11 8 10 ax-mp 
 |-  ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) )
12 7 11 mpbi 
 |-  1 < ( 3 / 2 )
13 1 3 12 ltleii 
 |-  1 <_ ( 3 / 2 )
14 3lt4 
 |-  3 < 4
15 2t2e4 
 |-  ( 2 x. 2 ) = 4
16 14 15 breqtrri 
 |-  3 < ( 2 x. 2 )
17 9 8 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
18 ltdivmul 
 |-  ( ( 3 e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 3 / 2 ) < 2 <-> 3 < ( 2 x. 2 ) ) )
19 2 9 17 18 mp3an 
 |-  ( ( 3 / 2 ) < 2 <-> 3 < ( 2 x. 2 ) )
20 16 19 mpbir 
 |-  ( 3 / 2 ) < 2
21 df-2 
 |-  2 = ( 1 + 1 )
22 20 21 breqtri 
 |-  ( 3 / 2 ) < ( 1 + 1 )
23 1z 
 |-  1 e. ZZ
24 flbi 
 |-  ( ( ( 3 / 2 ) e. RR /\ 1 e. ZZ ) -> ( ( |_ ` ( 3 / 2 ) ) = 1 <-> ( 1 <_ ( 3 / 2 ) /\ ( 3 / 2 ) < ( 1 + 1 ) ) ) )
25 3 23 24 mp2an 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 <-> ( 1 <_ ( 3 / 2 ) /\ ( 3 / 2 ) < ( 1 + 1 ) ) )
26 13 22 25 mpbir2an 
 |-  ( |_ ` ( 3 / 2 ) ) = 1
27 9 renegcli 
 |-  -u 2 e. RR
28 3 renegcli 
 |-  -u ( 3 / 2 ) e. RR
29 3 9 ltnegi 
 |-  ( ( 3 / 2 ) < 2 <-> -u 2 < -u ( 3 / 2 ) )
30 20 29 mpbi 
 |-  -u 2 < -u ( 3 / 2 )
31 27 28 30 ltleii 
 |-  -u 2 <_ -u ( 3 / 2 )
32 4 negcli 
 |-  -u 2 e. CC
33 ax-1cn 
 |-  1 e. CC
34 negdi2 
 |-  ( ( -u 2 e. CC /\ 1 e. CC ) -> -u ( -u 2 + 1 ) = ( -u -u 2 - 1 ) )
35 32 33 34 mp2an 
 |-  -u ( -u 2 + 1 ) = ( -u -u 2 - 1 )
36 4 negnegi 
 |-  -u -u 2 = 2
37 36 oveq1i 
 |-  ( -u -u 2 - 1 ) = ( 2 - 1 )
38 35 37 eqtri 
 |-  -u ( -u 2 + 1 ) = ( 2 - 1 )
39 2m1e1 
 |-  ( 2 - 1 ) = 1
40 39 12 eqbrtri 
 |-  ( 2 - 1 ) < ( 3 / 2 )
41 38 40 eqbrtri 
 |-  -u ( -u 2 + 1 ) < ( 3 / 2 )
42 27 1 readdcli 
 |-  ( -u 2 + 1 ) e. RR
43 42 3 ltnegcon1i 
 |-  ( -u ( -u 2 + 1 ) < ( 3 / 2 ) <-> -u ( 3 / 2 ) < ( -u 2 + 1 ) )
44 41 43 mpbi 
 |-  -u ( 3 / 2 ) < ( -u 2 + 1 )
45 2z 
 |-  2 e. ZZ
46 znegcl 
 |-  ( 2 e. ZZ -> -u 2 e. ZZ )
47 45 46 ax-mp 
 |-  -u 2 e. ZZ
48 flbi 
 |-  ( ( -u ( 3 / 2 ) e. RR /\ -u 2 e. ZZ ) -> ( ( |_ ` -u ( 3 / 2 ) ) = -u 2 <-> ( -u 2 <_ -u ( 3 / 2 ) /\ -u ( 3 / 2 ) < ( -u 2 + 1 ) ) ) )
49 28 47 48 mp2an 
 |-  ( ( |_ ` -u ( 3 / 2 ) ) = -u 2 <-> ( -u 2 <_ -u ( 3 / 2 ) /\ -u ( 3 / 2 ) < ( -u 2 + 1 ) ) )
50 31 44 49 mpbir2an 
 |-  ( |_ ` -u ( 3 / 2 ) ) = -u 2
51 26 50 pm3.2i 
 |-  ( ( |_ ` ( 3 / 2 ) ) = 1 /\ ( |_ ` -u ( 3 / 2 ) ) = -u 2 )