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

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 3re ⊢ 3 ∈ ℝ
3 2 rehalfcli ⊢ ( 3 / 2 ) ∈ ℝ
4 2cn ⊢ 2 ∈ ℂ
5 4 mullidi ⊢ ( 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 )