# Metamath Proof Explorer

## Theorem rebtwnz

Description: There is a unique greatest integer less than or equal to a real number. Exercise 4 of Apostol p. 28. (Contributed by NM, 15-Nov-2004)

Ref Expression
Assertion rebtwnz ${⊢}{A}\in ℝ\to \exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)$

### Proof

Step Hyp Ref Expression
1 renegcl ${⊢}{A}\in ℝ\to -{A}\in ℝ$
2 zbtwnre ${⊢}-{A}\in ℝ\to \exists !{y}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le {y}\wedge {y}<-{A}+1\right)$
3 1 2 syl ${⊢}{A}\in ℝ\to \exists !{y}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le {y}\wedge {y}<-{A}+1\right)$
4 znegcl ${⊢}{x}\in ℤ\to -{x}\in ℤ$
5 znegcl ${⊢}{y}\in ℤ\to -{y}\in ℤ$
6 zcn ${⊢}{y}\in ℤ\to {y}\in ℂ$
7 zcn ${⊢}{x}\in ℤ\to {x}\in ℂ$
8 negcon2 ${⊢}\left({y}\in ℂ\wedge {x}\in ℂ\right)\to \left({y}=-{x}↔{x}=-{y}\right)$
9 6 7 8 syl2an ${⊢}\left({y}\in ℤ\wedge {x}\in ℤ\right)\to \left({y}=-{x}↔{x}=-{y}\right)$
10 5 9 reuhyp ${⊢}{y}\in ℤ\to \exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}{y}=-{x}$
11 breq2 ${⊢}{y}=-{x}\to \left(-{A}\le {y}↔-{A}\le -{x}\right)$
12 breq1 ${⊢}{y}=-{x}\to \left({y}<-{A}+1↔-{x}<-{A}+1\right)$
13 11 12 anbi12d ${⊢}{y}=-{x}\to \left(\left(-{A}\le {y}\wedge {y}<-{A}+1\right)↔\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)\right)$
14 4 10 13 reuxfr1 ${⊢}\exists !{y}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le {y}\wedge {y}<-{A}+1\right)↔\exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)$
15 zre ${⊢}{x}\in ℤ\to {x}\in ℝ$
16 leneg ${⊢}\left({x}\in ℝ\wedge {A}\in ℝ\right)\to \left({x}\le {A}↔-{A}\le -{x}\right)$
17 16 ancoms ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left({x}\le {A}↔-{A}\le -{x}\right)$
18 peano2rem ${⊢}{A}\in ℝ\to {A}-1\in ℝ$
19 ltneg ${⊢}\left({A}-1\in ℝ\wedge {x}\in ℝ\right)\to \left({A}-1<{x}↔-{x}<-\left({A}-1\right)\right)$
20 18 19 sylan ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left({A}-1<{x}↔-{x}<-\left({A}-1\right)\right)$
21 1re ${⊢}1\in ℝ$
22 ltsubadd ${⊢}\left({A}\in ℝ\wedge 1\in ℝ\wedge {x}\in ℝ\right)\to \left({A}-1<{x}↔{A}<{x}+1\right)$
23 21 22 mp3an2 ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left({A}-1<{x}↔{A}<{x}+1\right)$
24 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
25 ax-1cn ${⊢}1\in ℂ$
26 negsubdi ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to -\left({A}-1\right)=-{A}+1$
27 24 25 26 sylancl ${⊢}{A}\in ℝ\to -\left({A}-1\right)=-{A}+1$
28 27 adantr ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to -\left({A}-1\right)=-{A}+1$
29 28 breq2d ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left(-{x}<-\left({A}-1\right)↔-{x}<-{A}+1\right)$
30 20 23 29 3bitr3d ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left({A}<{x}+1↔-{x}<-{A}+1\right)$
31 17 30 anbi12d ${⊢}\left({A}\in ℝ\wedge {x}\in ℝ\right)\to \left(\left({x}\le {A}\wedge {A}<{x}+1\right)↔\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)\right)$
32 15 31 sylan2 ${⊢}\left({A}\in ℝ\wedge {x}\in ℤ\right)\to \left(\left({x}\le {A}\wedge {A}<{x}+1\right)↔\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)\right)$
33 32 bicomd ${⊢}\left({A}\in ℝ\wedge {x}\in ℤ\right)\to \left(\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)↔\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
34 33 reubidva ${⊢}{A}\in ℝ\to \left(\exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le -{x}\wedge -{x}<-{A}+1\right)↔\exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
35 14 34 syl5bb ${⊢}{A}\in ℝ\to \left(\exists !{y}\in ℤ\phantom{\rule{.4em}{0ex}}\left(-{A}\le {y}\wedge {y}<-{A}+1\right)↔\exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)\right)$
36 3 35 mpbid ${⊢}{A}\in ℝ\to \exists !{x}\in ℤ\phantom{\rule{.4em}{0ex}}\left({x}\le {A}\wedge {A}<{x}+1\right)$