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 biimtrdi ⊢ 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