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 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℚ 0 < x → A < x → A = 0

Proof

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