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 ${⊢}\left(⌊\frac{3}{2}⌋=1\wedge ⌊-\frac{3}{2}⌋=-2\right)$

Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 3re ${⊢}3\in ℝ$
3 2 rehalfcli ${⊢}\frac{3}{2}\in ℝ$
4 2cn ${⊢}2\in ℂ$
5 4 mulid2i ${⊢}1\cdot 2=2$
6 2lt3 ${⊢}2<3$
7 5 6 eqbrtri ${⊢}1\cdot 2<3$
8 2pos ${⊢}0<2$
9 2re ${⊢}2\in ℝ$
10 1 2 9 ltmuldivi ${⊢}0<2\to \left(1\cdot 2<3↔1<\frac{3}{2}\right)$
11 8 10 ax-mp ${⊢}1\cdot 2<3↔1<\frac{3}{2}$
12 7 11 mpbi ${⊢}1<\frac{3}{2}$
13 1 3 12 ltleii ${⊢}1\le \frac{3}{2}$
14 3lt4 ${⊢}3<4$
15 2t2e4 ${⊢}2\cdot 2=4$
16 14 15 breqtrri ${⊢}3<2\cdot 2$
17 9 8 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
18 ltdivmul ${⊢}\left(3\in ℝ\wedge 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{3}{2}<2↔3<2\cdot 2\right)$
19 2 9 17 18 mp3an ${⊢}\frac{3}{2}<2↔3<2\cdot 2$
20 16 19 mpbir ${⊢}\frac{3}{2}<2$
21 df-2 ${⊢}2=1+1$
22 20 21 breqtri ${⊢}\frac{3}{2}<1+1$
23 1z ${⊢}1\in ℤ$
24 flbi ${⊢}\left(\frac{3}{2}\in ℝ\wedge 1\in ℤ\right)\to \left(⌊\frac{3}{2}⌋=1↔\left(1\le \frac{3}{2}\wedge \frac{3}{2}<1+1\right)\right)$
25 3 23 24 mp2an ${⊢}⌊\frac{3}{2}⌋=1↔\left(1\le \frac{3}{2}\wedge \frac{3}{2}<1+1\right)$
26 13 22 25 mpbir2an ${⊢}⌊\frac{3}{2}⌋=1$
27 9 renegcli ${⊢}-2\in ℝ$
28 3 renegcli ${⊢}-\frac{3}{2}\in ℝ$
29 3 9 ltnegi ${⊢}\frac{3}{2}<2↔-2<-\frac{3}{2}$
30 20 29 mpbi ${⊢}-2<-\frac{3}{2}$
31 27 28 30 ltleii ${⊢}-2\le -\frac{3}{2}$
32 4 negcli ${⊢}-2\in ℂ$
33 ax-1cn ${⊢}1\in ℂ$
34 negdi2 ${⊢}\left(-2\in ℂ\wedge 1\in ℂ\right)\to -\left(-2+1\right)=--2-1$
35 32 33 34 mp2an ${⊢}-\left(-2+1\right)=--2-1$
36 4 negnegi ${⊢}--2=2$
37 36 oveq1i ${⊢}--2-1=2-1$
38 35 37 eqtri ${⊢}-\left(-2+1\right)=2-1$
39 2m1e1 ${⊢}2-1=1$
40 39 12 eqbrtri ${⊢}2-1<\frac{3}{2}$
41 38 40 eqbrtri ${⊢}-\left(-2+1\right)<\frac{3}{2}$
42 27 1 readdcli ${⊢}-2+1\in ℝ$
43 42 3 ltnegcon1i ${⊢}-\left(-2+1\right)<\frac{3}{2}↔-\frac{3}{2}<-2+1$
44 41 43 mpbi ${⊢}-\frac{3}{2}<-2+1$
45 2z ${⊢}2\in ℤ$
46 znegcl ${⊢}2\in ℤ\to -2\in ℤ$
47 45 46 ax-mp ${⊢}-2\in ℤ$
48 flbi ${⊢}\left(-\frac{3}{2}\in ℝ\wedge -2\in ℤ\right)\to \left(⌊-\frac{3}{2}⌋=-2↔\left(-2\le -\frac{3}{2}\wedge -\frac{3}{2}<-2+1\right)\right)$
49 28 47 48 mp2an ${⊢}⌊-\frac{3}{2}⌋=-2↔\left(-2\le -\frac{3}{2}\wedge -\frac{3}{2}<-2+1\right)$
50 31 44 49 mpbir2an ${⊢}⌊-\frac{3}{2}⌋=-2$
51 26 50 pm3.2i ${⊢}\left(⌊\frac{3}{2}⌋=1\wedge ⌊-\frac{3}{2}⌋=-2\right)$