Theorem ex-ceil

Description: Example for df-ceil . (Contributed by AV, 4-Sep-2021)

	Ref	Expression
Assertion	ex-ceil	$$⊢\left(⌈\frac{3}{2}⌉=2\wedge ⌈-\frac{3}{2}⌉=-1\right)$$

Proof

Step	Hyp	Ref	Expression
1		ex-fl	$$⊢\left(⌊\frac{3}{2}⌋=1\wedge ⌊-\frac{3}{2}⌋=-2\right)$$
2		3re	$$⊢3\in ℝ$$
3	2	rehalfcli	$$⊢\frac{3}{2}\in ℝ$$
4	3	renegcli	$$⊢-\frac{3}{2}\in ℝ$$
5		ceilval	$$⊢-\frac{3}{2}\in ℝ\to ⌈-\frac{3}{2}⌉=-⌊-\left(-\frac{3}{2}\right)⌋$$
6	4 5	ax-mp	$$⊢⌈-\frac{3}{2}⌉=-⌊-\left(-\frac{3}{2}\right)⌋$$
7	3	recni	$$⊢\frac{3}{2}\in ℂ$$
8	7	negnegi	$$⊢-\left(-\frac{3}{2}\right)=\frac{3}{2}$$
9	8	eqcomi	$$⊢\frac{3}{2}=-\left(-\frac{3}{2}\right)$$
10	9	fveq2i	$$⊢⌊\frac{3}{2}⌋=⌊-\left(-\frac{3}{2}\right)⌋$$
11	10	eqeq1i	$$⊢⌊\frac{3}{2}⌋=1\leftrightarrow ⌊-\left(-\frac{3}{2}\right)⌋=1$$
12	11	biimpi	$$⊢⌊\frac{3}{2}⌋=1\to ⌊-\left(-\frac{3}{2}\right)⌋=1$$
13	12	negeqd	$$⊢⌊\frac{3}{2}⌋=1\to -⌊-\left(-\frac{3}{2}\right)⌋=-1$$
14	6 13	syl5eq	$$⊢⌊\frac{3}{2}⌋=1\to ⌈-\frac{3}{2}⌉=-1$$
15		ceilval	$$⊢\frac{3}{2}\in ℝ\to ⌈\frac{3}{2}⌉=-⌊-\frac{3}{2}⌋$$
16	3 15	ax-mp	$$⊢⌈\frac{3}{2}⌉=-⌊-\frac{3}{2}⌋$$
17		negeq	$$⊢⌊-\frac{3}{2}⌋=-2\to -⌊-\frac{3}{2}⌋=--2$$
18		2cn	$$⊢2\in ℂ$$
19	18	negnegi	$$⊢--2=2$$
20	17 19	eqtrdi	$$⊢⌊-\frac{3}{2}⌋=-2\to -⌊-\frac{3}{2}⌋=2$$
21	16 20	syl5eq	$$⊢⌊-\frac{3}{2}⌋=-2\to ⌈\frac{3}{2}⌉=2$$
22	14 21	anim12ci	$$⊢\left(⌊\frac{3}{2}⌋=1\wedge ⌊-\frac{3}{2}⌋=-2\right)\to \left(⌈\frac{3}{2}⌉=2\wedge ⌈-\frac{3}{2}⌉=-1\right)$$
23	1 22	ax-mp	$$⊢\left(⌈\frac{3}{2}⌉=2\wedge ⌈-\frac{3}{2}⌉=-1\right)$$