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∈ℝ→∃!x∈ℤx≤A∧A<x+1

Proof

Step Hyp Ref Expression
1 renegcl ⊢A∈ℝ→−A∈ℝ
2 zbtwnre ⊢−A∈ℝ→∃!y∈ℤ−A≤y∧y<-A+1
3 1 2 syl ⊢A∈ℝ→∃!y∈ℤ−A≤y∧y<-A+1
4 znegcl ⊢x∈ℤ→−x∈ℤ
5 znegcl ⊢y∈ℤ→−y∈ℤ
6 zcn ⊢y∈ℤ→y∈ℂ
7 zcn ⊢x∈ℤ→x∈ℂ
8 negcon2 ⊢y∈ℂ∧x∈ℂ→y=−x↔x=−y
9 6 7 8 syl2an ⊢y∈ℤ∧x∈ℤ→y=−x↔x=−y
10 5 9 reuhyp ⊢y∈ℤ→∃!x∈ℤy=−x
11 breq2 ⊢y=−x→−A≤y↔−A≤−x
12 breq1 ⊢y=−x→y<-A+1↔−x<-A+1
13 11 12 anbi12d ⊢y=−x→−A≤y∧y<-A+1↔−A≤−x∧−x<-A+1
14 4 10 13 reuxfr1 ⊢∃!y∈ℤ−A≤y∧y<-A+1↔∃!x∈ℤ−A≤−x∧−x<-A+1
15 zre ⊢x∈ℤ→x∈ℝ
16 leneg ⊢x∈ℝ∧A∈ℝ→x≤A↔−A≤−x
17 16 ancoms ⊢A∈ℝ∧x∈ℝ→x≤A↔−A≤−x
18 peano2rem ⊢A∈ℝ→A−1∈ℝ
19 ltneg ⊢A−1∈ℝ∧x∈ℝ→A−1<x↔−x<−A−1
20 18 19 sylan ⊢A∈ℝ∧x∈ℝ→A−1<x↔−x<−A−1
21 1re ⊢1∈ℝ
22 ltsubadd ⊢A∈ℝ∧1∈ℝ∧x∈ℝ→A−1<x↔A<x+1
23 21 22 mp3an2 ⊢A∈ℝ∧x∈ℝ→A−1<x↔A<x+1
24 recn ⊢A∈ℝ→A∈ℂ
25 ax-1cn ⊢1∈ℂ
26 negsubdi ⊢A∈ℂ∧1∈ℂ→−A−1=-A+1
27 24 25 26 sylancl ⊢A∈ℝ→−A−1=-A+1
28 27 adantr ⊢A∈ℝ∧x∈ℝ→−A−1=-A+1
29 28 breq2d ⊢A∈ℝ∧x∈ℝ→−x<−A−1↔−x<-A+1
30 20 23 29 3bitr3d ⊢A∈ℝ∧x∈ℝ→A<x+1↔−x<-A+1
31 17 30 anbi12d ⊢A∈ℝ∧x∈ℝ→x≤A∧A<x+1↔−A≤−x∧−x<-A+1
32 15 31 sylan2 ⊢A∈ℝ∧x∈ℤ→x≤A∧A<x+1↔−A≤−x∧−x<-A+1
33 32 bicomd ⊢A∈ℝ∧x∈ℤ→−A≤−x∧−x<-A+1↔x≤A∧A<x+1
34 33 reubidva ⊢A∈ℝ→∃!x∈ℤ−A≤−x∧−x<-A+1↔∃!x∈ℤx≤A∧A<x+1
35 14 34 syl5bb ⊢A∈ℝ→∃!y∈ℤ−A≤y∧y<-A+1↔∃!x∈ℤx≤A∧A<x+1
36 3 35 mpbid ⊢A∈ℝ→∃!x∈ℤx≤A∧A<x+1