Theorem fleqceilz

Description: A real number is an integer iff its floor equals its ceiling. (Contributed by AV, 30-Nov-2018)

	Ref	Expression
Assertion	fleqceilz	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow ⌊A⌋=⌈A⌉\right)$$

Proof

Step	Hyp	Ref	Expression
1		flid	$$⊢A\in \mathbb{Z}\to ⌊A⌋=A$$
2		ceilid	$$⊢A\in \mathbb{Z}\to ⌈A⌉=A$$
3	1 2	eqtr4d	$$⊢A\in \mathbb{Z}\to ⌊A⌋=⌈A⌉$$
4		eqeq1	$$⊢⌊A⌋=A\to \left(⌊A⌋=⌈A⌉\leftrightarrow A=⌈A⌉\right)$$
5	4	adantr	$$⊢\left(⌊A⌋=A\wedge A\in ℝ\right)\to \left(⌊A⌋=⌈A⌉\leftrightarrow A=⌈A⌉\right)$$
6		ceilidz	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow ⌈A⌉=A\right)$$
7		eqcom	$$⊢⌈A⌉=A\leftrightarrow A=⌈A⌉$$
8	6 7	bitrdi	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow A=⌈A⌉\right)$$
9	8	biimprd	$$⊢A\in ℝ\to \left(A=⌈A⌉\to A\in \mathbb{Z}\right)$$
10	9	adantl	$$⊢\left(⌊A⌋=A\wedge A\in ℝ\right)\to \left(A=⌈A⌉\to A\in \mathbb{Z}\right)$$
11	5 10	sylbid	$$⊢\left(⌊A⌋=A\wedge A\in ℝ\right)\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)$$
12	11	ex	$$⊢⌊A⌋=A\to \left(A\in ℝ\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)$$
13		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
14		df-ne	$$⊢⌊A⌋\ne A\leftrightarrow \neg ⌊A⌋=A$$
15		necom	$$⊢⌊A⌋\ne A\leftrightarrow A\ne ⌊A⌋$$
16		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
17		id	$$⊢A\in ℝ\to A\in ℝ$$
18	16 17	ltlend	$$⊢A\in ℝ\to \left(⌊A⌋<A\leftrightarrow \left(⌊A⌋\le A\wedge A\ne ⌊A⌋\right)\right)$$
19		breq1	$$⊢⌊A⌋=⌈A⌉\to \left(⌊A⌋<A\leftrightarrow ⌈A⌉<A\right)$$
20	19	adantl	$$⊢\left(A\in ℝ\wedge ⌊A⌋=⌈A⌉\right)\to \left(⌊A⌋<A\leftrightarrow ⌈A⌉<A\right)$$
21		ceilge	$$⊢A\in ℝ\to A\le ⌈A⌉$$
22		ceilcl	$$⊢A\in ℝ\to ⌈A⌉\in \mathbb{Z}$$
23	22	zred	$$⊢A\in ℝ\to ⌈A⌉\in ℝ$$
24	17 23	lenltd	$$⊢A\in ℝ\to \left(A\le ⌈A⌉\leftrightarrow \neg ⌈A⌉<A\right)$$
25		pm2.21	$$⊢\neg ⌈A⌉<A\to \left(⌈A⌉<A\to A\in \mathbb{Z}\right)$$
26	24 25	syl6bi	$$⊢A\in ℝ\to \left(A\le ⌈A⌉\to \left(⌈A⌉<A\to A\in \mathbb{Z}\right)\right)$$
27	21 26	mpd	$$⊢A\in ℝ\to \left(⌈A⌉<A\to A\in \mathbb{Z}\right)$$
28	27	adantr	$$⊢\left(A\in ℝ\wedge ⌊A⌋=⌈A⌉\right)\to \left(⌈A⌉<A\to A\in \mathbb{Z}\right)$$
29	20 28	sylbid	$$⊢\left(A\in ℝ\wedge ⌊A⌋=⌈A⌉\right)\to \left(⌊A⌋<A\to A\in \mathbb{Z}\right)$$
30	29	ex	$$⊢A\in ℝ\to \left(⌊A⌋=⌈A⌉\to \left(⌊A⌋<A\to A\in \mathbb{Z}\right)\right)$$
31	30	com23	$$⊢A\in ℝ\to \left(⌊A⌋<A\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)$$
32	18 31	sylbird	$$⊢A\in ℝ\to \left(\left(⌊A⌋\le A\wedge A\ne ⌊A⌋\right)\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)$$
33	32	expd	$$⊢A\in ℝ\to \left(⌊A⌋\le A\to \left(A\ne ⌊A⌋\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)\right)$$
34	33	com3r	$$⊢A\ne ⌊A⌋\to \left(A\in ℝ\to \left(⌊A⌋\le A\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)\right)$$
35	15 34	sylbi	$$⊢⌊A⌋\ne A\to \left(A\in ℝ\to \left(⌊A⌋\le A\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)\right)$$
36	14 35	sylbir	$$⊢\neg ⌊A⌋=A\to \left(A\in ℝ\to \left(⌊A⌋\le A\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)\right)$$
37	13 36	mpdi	$$⊢\neg ⌊A⌋=A\to \left(A\in ℝ\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)\right)$$
38	12 37	pm2.61i	$$⊢A\in ℝ\to \left(⌊A⌋=⌈A⌉\to A\in \mathbb{Z}\right)$$
39	3 38	impbid2	$$⊢A\in ℝ\to \left(A\in \mathbb{Z}\leftrightarrow ⌊A⌋=⌈A⌉\right)$$