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	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flid	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = 𝐴 )
2		ceilid	⊢ ( 𝐴 ∈ ℤ → ( ⌈ ‘ 𝐴 ) = 𝐴 )
3	1 2	eqtr4d	⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) )
4		eqeq1	⊢ ( ( ⌊ ‘ 𝐴 ) = 𝐴 → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ↔ 𝐴 = ( ⌈ ‘ 𝐴 ) ) )
5	4	adantr	⊢ ( ( ( ⌊ ‘ 𝐴 ) = 𝐴 ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ↔ 𝐴 = ( ⌈ ‘ 𝐴 ) ) )
6		ceilidz	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ ( ⌈ ‘ 𝐴 ) = 𝐴 ) )
7		eqcom	⊢ ( ( ⌈ ‘ 𝐴 ) = 𝐴 ↔ 𝐴 = ( ⌈ ‘ 𝐴 ) )
8	6 7	bitrdi	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ 𝐴 = ( ⌈ ‘ 𝐴 ) ) )
9	8	biimprd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) )
10	9	adantl	⊢ ( ( ( ⌊ ‘ 𝐴 ) = 𝐴 ∧ 𝐴 ∈ ℝ ) → ( 𝐴 = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) )
11	5 10	sylbid	⊢ ( ( ( ⌊ ‘ 𝐴 ) = 𝐴 ∧ 𝐴 ∈ ℝ ) → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) )
12	11	ex	⊢ ( ( ⌊ ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) )
13		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
14		df-ne	⊢ ( ( ⌊ ‘ 𝐴 ) ≠ 𝐴 ↔ ¬ ( ⌊ ‘ 𝐴 ) = 𝐴 )
15		necom	⊢ ( ( ⌊ ‘ 𝐴 ) ≠ 𝐴 ↔ 𝐴 ≠ ( ⌊ ‘ 𝐴 ) )
16		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
17		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
18	16 17	ltlend	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) < 𝐴 ↔ ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 ≠ ( ⌊ ‘ 𝐴 ) ) ) )
19		breq1	⊢ ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) < 𝐴 ↔ ( ⌈ ‘ 𝐴 ) < 𝐴 ) )
20	19	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ) → ( ( ⌊ ‘ 𝐴 ) < 𝐴 ↔ ( ⌈ ‘ 𝐴 ) < 𝐴 ) )
21		ceilge	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( ⌈ ‘ 𝐴 ) )
22		ceilcl	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℤ )
23	22	zred	⊢ ( 𝐴 ∈ ℝ → ( ⌈ ‘ 𝐴 ) ∈ ℝ )
24	17 23	lenltd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ ( ⌈ ‘ 𝐴 ) ↔ ¬ ( ⌈ ‘ 𝐴 ) < 𝐴 ) )
25		pm2.21	⊢ ( ¬ ( ⌈ ‘ 𝐴 ) < 𝐴 → ( ( ⌈ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) )
26	24 25	biimtrdi	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ ( ⌈ ‘ 𝐴 ) → ( ( ⌈ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) ) )
27	21 26	mpd	⊢ ( 𝐴 ∈ ℝ → ( ( ⌈ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) )
28	27	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ) → ( ( ⌈ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) )
29	20 28	sylbid	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ) → ( ( ⌊ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) )
30	29	ex	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) < 𝐴 → 𝐴 ∈ ℤ ) ) )
31	30	com23	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) < 𝐴 → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) )
32	18 31	sylbird	⊢ ( 𝐴 ∈ ℝ → ( ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 ∧ 𝐴 ≠ ( ⌊ ‘ 𝐴 ) ) → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) )
33	32	expd	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 → ( 𝐴 ≠ ( ⌊ ‘ 𝐴 ) → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) ) )
34	33	com3r	⊢ ( 𝐴 ≠ ( ⌊ ‘ 𝐴 ) → ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) ) )
35	15 34	sylbi	⊢ ( ( ⌊ ‘ 𝐴 ) ≠ 𝐴 → ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) ) )
36	14 35	sylbir	⊢ ( ¬ ( ⌊ ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ≤ 𝐴 → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) ) )
37	13 36	mpdi	⊢ ( ¬ ( ⌊ ‘ 𝐴 ) = 𝐴 → ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) ) )
38	12 37	pm2.61i	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) → 𝐴 ∈ ℤ ) )
39	3 38	impbid2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℤ ↔ ( ⌊ ‘ 𝐴 ) = ( ⌈ ‘ 𝐴 ) ) )