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