Theorem qsqueeze

Description: If a nonnegative real is less than any positive rational, it is zero. (Contributed by NM, 6-Feb-2007)

	Ref	Expression
Assertion	qsqueeze	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 = 0 )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		ltnle	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 ↔ ¬ 𝐴 ≤ 0 ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ¬ 𝐴 ≤ 0 ) )
4		qbtwnre	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) )
5	1 4	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) )
6	5	ex	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) ) )
7		qre	⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
8		ltnsym	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 < 𝑥 → ¬ 𝑥 < 𝐴 ) )
9	8	con2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑥 < 𝐴 → ¬ 𝐴 < 𝑥 ) )
10	7 9	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℚ ) → ( 𝑥 < 𝐴 → ¬ 𝐴 < 𝑥 ) )
11	10	anim2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℚ ) → ( ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) → ( 0 < 𝑥 ∧ ¬ 𝐴 < 𝑥 ) ) )
12	11	reximdva	⊢ ( 𝐴 ∈ ℝ → ( ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ 𝑥 < 𝐴 ) → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ¬ 𝐴 < 𝑥 ) ) )
13	6 12	syld	⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ¬ 𝐴 < 𝑥 ) ) )
14	3 13	sylbird	⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ≤ 0 → ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ¬ 𝐴 < 𝑥 ) ) )
15		rexanali	⊢ ( ∃ 𝑥 ∈ ℚ ( 0 < 𝑥 ∧ ¬ 𝐴 < 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) )
16	14 15	imbitrdi	⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ≤ 0 → ¬ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) )
17	16	con4d	⊢ ( 𝐴 ∈ ℝ → ( ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) → 𝐴 ≤ 0 ) )
18	17	imp	⊢ ( ( 𝐴 ∈ ℝ ∧ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 ≤ 0 )
19	18	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 ≤ 0 )
20		letri3	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
21	1 20	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 = 0 ↔ ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐴 ) ) )
22	21	rbaibd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 = 0 ↔ 𝐴 ≤ 0 ) )
23	22	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → ( 𝐴 = 0 ↔ 𝐴 ≤ 0 ) )
24	19 23	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ ∀ 𝑥 ∈ ℚ ( 0 < 𝑥 → 𝐴 < 𝑥 ) ) → 𝐴 = 0 )