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	⊢ ( 𝐴 ∈ ℝ → ∃! 𝑥 ∈ ℤ ( 𝐴 ≤ 𝑥 ∧ 𝑥 < ( 𝐴 + 1 ) ) )

Proof

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