Description: Example for df-fl . Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ex-fl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1re | |
|
2 | 3re | |
|
3 | 2 | rehalfcli | |
4 | 2cn | |
|
5 | 4 | mulid2i | |
6 | 2lt3 | |
|
7 | 5 6 | eqbrtri | |
8 | 2pos | |
|
9 | 2re | |
|
10 | 1 2 9 | ltmuldivi | |
11 | 8 10 | ax-mp | |
12 | 7 11 | mpbi | |
13 | 1 3 12 | ltleii | |
14 | 3lt4 | |
|
15 | 2t2e4 | |
|
16 | 14 15 | breqtrri | |
17 | 9 8 | pm3.2i | |
18 | ltdivmul | |
|
19 | 2 9 17 18 | mp3an | |
20 | 16 19 | mpbir | |
21 | df-2 | |
|
22 | 20 21 | breqtri | |
23 | 1z | |
|
24 | flbi | |
|
25 | 3 23 24 | mp2an | |
26 | 13 22 25 | mpbir2an | |
27 | 9 | renegcli | |
28 | 3 | renegcli | |
29 | 3 9 | ltnegi | |
30 | 20 29 | mpbi | |
31 | 27 28 30 | ltleii | |
32 | 4 | negcli | |
33 | ax-1cn | |
|
34 | negdi2 | |
|
35 | 32 33 34 | mp2an | |
36 | 4 | negnegi | |
37 | 36 | oveq1i | |
38 | 35 37 | eqtri | |
39 | 2m1e1 | |
|
40 | 39 12 | eqbrtri | |
41 | 38 40 | eqbrtri | |
42 | 27 1 | readdcli | |
43 | 42 3 | ltnegcon1i | |
44 | 41 43 | mpbi | |
45 | 2z | |
|
46 | znegcl | |
|
47 | 45 46 | ax-mp | |
48 | flbi | |
|
49 | 28 47 48 | mp2an | |
50 | 31 44 49 | mpbir2an | |
51 | 26 50 | pm3.2i | |