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\leftrightarrow 1<\frac{3}{2}\right)$$
11	8 10	ax-mp	$$⊢1\cdot 2<3\leftrightarrow 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\leftrightarrow 3<2\cdot 2\right)$$
19	2 9 17 18	mp3an	$$⊢\frac{3}{2}<2\leftrightarrow 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 \mathbb{Z}$$
24		flbi	$$⊢\left(\frac{3}{2}\in ℝ\wedge 1\in \mathbb{Z}\right)\to \left(⌊\frac{3}{2}⌋=1\leftrightarrow \left(1\le \frac{3}{2}\wedge \frac{3}{2}<1+1\right)\right)$$
25	3 23 24	mp2an	$$⊢⌊\frac{3}{2}⌋=1\leftrightarrow \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\leftrightarrow -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}\leftrightarrow -\frac{3}{2}<-2+1$$
44	41 43	mpbi	$$⊢-\frac{3}{2}<-2+1$$
45		2z	$$⊢2\in \mathbb{Z}$$
46		znegcl	$$⊢2\in \mathbb{Z}\to -2\in \mathbb{Z}$$
47	45 46	ax-mp	$$⊢-2\in \mathbb{Z}$$
48		flbi	$$⊢\left(-\frac{3}{2}\in ℝ\wedge -2\in \mathbb{Z}\right)\to \left(⌊-\frac{3}{2}⌋=-2\leftrightarrow \left(-2\le -\frac{3}{2}\wedge -\frac{3}{2}<-2+1\right)\right)$$
49	28 47 48	mp2an	$$⊢⌊-\frac{3}{2}⌋=-2\leftrightarrow \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)$$