Metamath Proof Explorer

Theorem zbtwnre

Description: There is a unique integer between a real number and the number plus one. Exercise 5 of Apostol p. 28. (Contributed by NM, 13-Nov-2004)

Ref Expression
Assertion zbtwnre ⊢A∈ℝ→∃!x∈ℤA≤x∧x<A+1

Proof

Step Hyp Ref Expression
1 zmin ⊢A∈ℝ→∃!x∈ℤA≤x∧∀y∈ℤA≤y→x≤y
2 zre ⊢y∈ℤ→y∈ℝ
3 zre ⊢x∈ℤ→x∈ℝ
4 peano2rem ⊢x∈ℝ→x−1∈ℝ
5 3 4 syl ⊢x∈ℤ→x−1∈ℝ
6 ltletr ⊢x−1∈ℝ∧A∈ℝ∧y∈ℝ→x−1<A∧A≤y→x−1<y
7 5 6 syl3an1 ⊢x∈ℤ∧A∈ℝ∧y∈ℝ→x−1<A∧A≤y→x−1<y
8 7 3expa ⊢x∈ℤ∧A∈ℝ∧y∈ℝ→x−1<A∧A≤y→x−1<y
9 2 8 sylan2 ⊢x∈ℤ∧A∈ℝ∧y∈ℤ→x−1<A∧A≤y→x−1<y
10 zlem1lt ⊢x∈ℤ∧y∈ℤ→x≤y↔x−1<y
11 10 adantlr ⊢x∈ℤ∧A∈ℝ∧y∈ℤ→x≤y↔x−1<y
12 9 11 sylibrd ⊢x∈ℤ∧A∈ℝ∧y∈ℤ→x−1<A∧A≤y→x≤y
13 12 exp4b ⊢x∈ℤ∧A∈ℝ→y∈ℤ→x−1<A→A≤y→x≤y
14 13 com23 ⊢x∈ℤ∧A∈ℝ→x−1<A→y∈ℤ→A≤y→x≤y
15 14 ralrimdv ⊢x∈ℤ∧A∈ℝ→x−1<A→∀y∈ℤA≤y→x≤y
16 5 ltnrd ⊢x∈ℤ→¬x−1<x−1
17 peano2zm ⊢x∈ℤ→x−1∈ℤ
18 zlem1lt ⊢x∈ℤ∧x−1∈ℤ→x≤x−1↔x−1<x−1
19 17 18 mpdan ⊢x∈ℤ→x≤x−1↔x−1<x−1
20 16 19 mtbird ⊢x∈ℤ→¬x≤x−1
21 20 ad2antrr ⊢x∈ℤ∧A∈ℝ∧∀y∈ℤA≤y→x≤y→¬x≤x−1
22 lenlt ⊢A∈ℝ∧x−1∈ℝ→A≤x−1↔¬x−1<A
23 5 22 sylan2 ⊢A∈ℝ∧x∈ℤ→A≤x−1↔¬x−1<A
24 23 ancoms ⊢x∈ℤ∧A∈ℝ→A≤x−1↔¬x−1<A
25 24 adantr ⊢x∈ℤ∧A∈ℝ∧∀y∈ℤA≤y→x≤y→A≤x−1↔¬x−1<A
26 breq2 ⊢y=x−1→A≤y↔A≤x−1
27 breq2 ⊢y=x−1→x≤y↔x≤x−1
28 26 27 imbi12d ⊢y=x−1→A≤y→x≤y↔A≤x−1→x≤x−1
29 28 rspcv ⊢x−1∈ℤ→∀y∈ℤA≤y→x≤y→A≤x−1→x≤x−1
30 17 29 syl ⊢x∈ℤ→∀y∈ℤA≤y→x≤y→A≤x−1→x≤x−1
31 30 imp ⊢x∈ℤ∧∀y∈ℤA≤y→x≤y→A≤x−1→x≤x−1
32 31 adantlr ⊢x∈ℤ∧A∈ℝ∧∀y∈ℤA≤y→x≤y→A≤x−1→x≤x−1
33 25 32 sylbird ⊢x∈ℤ∧A∈ℝ∧∀y∈ℤA≤y→x≤y→¬x−1<A→x≤x−1
34 21 33 mt3d ⊢x∈ℤ∧A∈ℝ∧∀y∈ℤA≤y→x≤y→x−1<A
35 34 ex ⊢x∈ℤ∧A∈ℝ→∀y∈ℤA≤y→x≤y→x−1<A
36 15 35 impbid ⊢x∈ℤ∧A∈ℝ→x−1<A↔∀y∈ℤA≤y→x≤y
37 1re ⊢1∈ℝ
38 ltsubadd ⊢x∈ℝ∧1∈ℝ∧A∈ℝ→x−1<A↔x<A+1
39 37 38 mp3an2 ⊢x∈ℝ∧A∈ℝ→x−1<A↔x<A+1
40 3 39 sylan ⊢x∈ℤ∧A∈ℝ→x−1<A↔x<A+1
41 36 40 bitr3d ⊢x∈ℤ∧A∈ℝ→∀y∈ℤA≤y→x≤y↔x<A+1
42 41 ancoms ⊢A∈ℝ∧x∈ℤ→∀y∈ℤA≤y→x≤y↔x<A+1
43 42 anbi2d ⊢A∈ℝ∧x∈ℤ→A≤x∧∀y∈ℤA≤y→x≤y↔A≤x∧x<A+1
44 43 reubidva ⊢A∈ℝ→∃!x∈ℤA≤x∧∀y∈ℤA≤y→x≤y↔∃!x∈ℤA≤x∧x<A+1
45 1 44 mpbid ⊢A∈ℝ→∃!x∈ℤA≤x∧x<A+1