This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )