Metamath Proof Explorer

Theorem irrapxlem6

Description: Lemma for irrapx1 . Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion irrapxlem6 ⊢ A ∈ ℝ + ∧ B ∈ ℝ + → ∃ x ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 x − A < B

Proof

Step Hyp Ref Expression
1 simplr ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → a ∈ ℚ
2 simpr1 ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → 0 < a
3 simpr3 ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → a − A < denom ⁡ a − 2
4 2 3 jca ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → 0 < a ∧ a − A < denom ⁡ a − 2
5 breq2 ⊢ y = a → 0 < y ↔ 0 < a
6 fvoveq1 ⊢ y = a → y − A = a − A
7 fveq2 ⊢ y = a → denom ⁡ y = denom ⁡ a
8 7 oveq1d ⊢ y = a → denom ⁡ y − 2 = denom ⁡ a − 2
9 6 8 breq12d ⊢ y = a → y − A < denom ⁡ y − 2 ↔ a − A < denom ⁡ a − 2
10 5 9 anbi12d ⊢ y = a → 0 < y ∧ y − A < denom ⁡ y − 2 ↔ 0 < a ∧ a − A < denom ⁡ a − 2
11 10 elrab ⊢ a ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 ↔ a ∈ ℚ ∧ 0 < a ∧ a − A < denom ⁡ a − 2
12 1 4 11 sylanbrc ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → a ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2
13 simpr2 ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → a − A < B
14 fvoveq1 ⊢ x = a → x − A = a − A
15 14 breq1d ⊢ x = a → x − A < B ↔ a − A < B
16 15 rspcev ⊢ a ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 ∧ a − A < B → ∃ x ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 x − A < B
17 12 13 16 syl2anc ⊢ A ∈ ℝ + ∧ B ∈ ℝ + ∧ a ∈ ℚ ∧ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2 → ∃ x ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 x − A < B
18 irrapxlem5 ⊢ A ∈ ℝ + ∧ B ∈ ℝ + → ∃ a ∈ ℚ 0 < a ∧ a − A < B ∧ a − A < denom ⁡ a − 2
19 17 18 r19.29a ⊢ A ∈ ℝ + ∧ B ∈ ℝ + → ∃ x ∈ y ∈ ℚ | 0 < y ∧ y − A < denom ⁡ y − 2 x − A < B