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 ∧ ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 )

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 3re 3 ∈ ℝ
3 2 rehalfcli ( 3 / 2 ) ∈ ℝ
4 2cn 2 ∈ ℂ
5 4 mulid2i ( 1 · 2 ) = 2
6 2lt3 2 < 3
7 5 6 eqbrtri ( 1 · 2 ) < 3
8 2pos 0 < 2
9 2re 2 ∈ ℝ
10 1 2 9 ltmuldivi ( 0 < 2 → ( ( 1 · 2 ) < 3 ↔ 1 < ( 3 / 2 ) ) )
11 8 10 ax-mp ( ( 1 · 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 · 2 ) = 4
16 14 15 breqtrri 3 < ( 2 · 2 )
17 9 8 pm3.2i ( 2 ∈ ℝ ∧ 0 < 2 )
18 ltdivmul ( ( 3 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 2 ) ) )
19 2 9 17 18 mp3an ( ( 3 / 2 ) < 2 ↔ 3 < ( 2 · 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 ∈ ℤ
24 flbi ( ( ( 3 / 2 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ ( 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 - 2 ∈ ℝ
28 3 renegcli - ( 3 / 2 ) ∈ ℝ
29 3 9 ltnegi ( ( 3 / 2 ) < 2 ↔ - 2 < - ( 3 / 2 ) )
30 20 29 mpbi - 2 < - ( 3 / 2 )
31 27 28 30 ltleii - 2 ≤ - ( 3 / 2 )
32 4 negcli - 2 ∈ ℂ
33 ax-1cn 1 ∈ ℂ
34 negdi2 ( ( - 2 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( - 2 + 1 ) = ( - - 2 − 1 ) )
35 32 33 34 mp2an - ( - 2 + 1 ) = ( - - 2 − 1 )
36 4 negnegi - - 2 = 2
37 36 oveq1i ( - - 2 − 1 ) = ( 2 − 1 )
38 35 37 eqtri - ( - 2 + 1 ) = ( 2 − 1 )
39 2m1e1 ( 2 − 1 ) = 1
40 39 12 eqbrtri ( 2 − 1 ) < ( 3 / 2 )
41 38 40 eqbrtri - ( - 2 + 1 ) < ( 3 / 2 )
42 27 1 readdcli ( - 2 + 1 ) ∈ ℝ
43 42 3 ltnegcon1i ( - ( - 2 + 1 ) < ( 3 / 2 ) ↔ - ( 3 / 2 ) < ( - 2 + 1 ) )
44 41 43 mpbi - ( 3 / 2 ) < ( - 2 + 1 )
45 2z 2 ∈ ℤ
46 znegcl ( 2 ∈ ℤ → - 2 ∈ ℤ )
47 45 46 ax-mp - 2 ∈ ℤ
48 flbi ( ( - ( 3 / 2 ) ∈ ℝ ∧ - 2 ∈ ℤ ) → ( ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 ↔ ( - 2 ≤ - ( 3 / 2 ) ∧ - ( 3 / 2 ) < ( - 2 + 1 ) ) ) )
49 28 47 48 mp2an ( ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 ↔ ( - 2 ≤ - ( 3 / 2 ) ∧ - ( 3 / 2 ) < ( - 2 + 1 ) ) )
50 31 44 49 mpbir2an ( ⌊ ‘ - ( 3 / 2 ) ) = - 2
51 26 50 pm3.2i ( ( ⌊ ‘ ( 3 / 2 ) ) = 1 ∧ ( ⌊ ‘ - ( 3 / 2 ) ) = - 2 )