Metamath Proof Explorer


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 A A = A

Proof

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