# Metamath Proof Explorer

## 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↔⌊-\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)$