This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

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