ex-ceil

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

Step	Hyp	Ref	Expression
1		ex-fl	$⊢ (⌊\frac{3}{2}⌋ = 1 \land ⌊- \frac{3}{2}⌋ = - 2)$
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}⌉ = - ⌊- (- \frac{3}{2})⌋$
6	4 5	ax-mp	$⊢ ⌈- \frac{3}{2}⌉ = - ⌊- (- \frac{3}{2})⌋$
7	3	recni	$⊢ \frac{3}{2} \in ℂ$
8	7	negnegi	$⊢ - (- \frac{3}{2}) = \frac{3}{2}$
9	8	eqcomi	$⊢ \frac{3}{2} = - (- \frac{3}{2})$
10	9	fveq2i	$⊢ ⌊\frac{3}{2}⌋ = ⌊- (- \frac{3}{2})⌋$
11	10	eqeq1i	$⊢ ⌊\frac{3}{2}⌋ = 1 \leftrightarrow ⌊- (- \frac{3}{2})⌋ = 1$
12	11	biimpi	$⊢ ⌊\frac{3}{2}⌋ = 1 \to ⌊- (- \frac{3}{2})⌋ = 1$
13	12	negeqd	$⊢ ⌊\frac{3}{2}⌋ = 1 \to - ⌊- (- \frac{3}{2})⌋ = - 1$
14	6 13	eqtrid	$⊢ ⌊\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	eqtrid	$⊢ ⌊- \frac{3}{2}⌋ = - 2 \to ⌈\frac{3}{2}⌉ = 2$
22	14 21	anim12ci	$⊢ (⌊\frac{3}{2}⌋ = 1 \land ⌊- \frac{3}{2}⌋ = - 2) \to (⌈\frac{3}{2}⌉ = 2 \land ⌈- \frac{3}{2}⌉ = - 1)$
23	1 22	ax-mp	$⊢ (⌈\frac{3}{2}⌉ = 2 \land ⌈- \frac{3}{2}⌉ = - 1)$

Metamath Proof Explorer