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 32=132=2

Proof

Step Hyp Ref Expression
1 1re 1
2 3re 3
3 2 rehalfcli 32
4 2cn 2
5 4 mulid2i 12=2
6 2lt3 2<3
7 5 6 eqbrtri 12<3
8 2pos 0<2
9 2re 2
10 1 2 9 ltmuldivi 0<212<31<32
11 8 10 ax-mp 12<31<32
12 7 11 mpbi 1<32
13 1 3 12 ltleii 132
14 3lt4 3<4
15 2t2e4 22=4
16 14 15 breqtrri 3<22
17 9 8 pm3.2i 20<2
18 ltdivmul 3220<232<23<22
19 2 9 17 18 mp3an 32<23<22
20 16 19 mpbir 32<2
21 df-2 2=1+1
22 20 21 breqtri 32<1+1
23 1z 1
24 flbi 32132=113232<1+1
25 3 23 24 mp2an 32=113232<1+1
26 13 22 25 mpbir2an 32=1
27 9 renegcli 2
28 3 renegcli 32
29 3 9 ltnegi 32<22<32
30 20 29 mpbi 2<32
31 27 28 30 ltleii 232
32 4 negcli 2
33 ax-1cn 1
34 negdi2 21-2+1=--2-1
35 32 33 34 mp2an -2+1=--2-1
36 4 negnegi -2=2
37 36 oveq1i --2-1=21
38 35 37 eqtri -2+1=21
39 2m1e1 21=1
40 39 12 eqbrtri 21<32
41 38 40 eqbrtri -2+1<32
42 27 1 readdcli -2+1
43 42 3 ltnegcon1i -2+1<3232<-2+1
44 41 43 mpbi 32<-2+1
45 2z 2
46 znegcl 22
47 45 46 ax-mp 2
48 flbi 32232=223232<-2+1
49 28 47 48 mp2an 32=223232<-2+1
50 31 44 49 mpbir2an 32=2
51 26 50 pm3.2i 32=132=2