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 \in ℝ^{+} \land B \in ℝ^{+}) \to \exists x \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \|x - A\| < B$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to a \in ℚ$
2		simpr1	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to 0 < a$
3		simpr3	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to \|a - A\| < {denom (a)}^{- 2}$
4	2 3	jca	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to (0 < a \land \|a - A\| < {denom (a)}^{- 2})$
5		breq2	$⊢ y = a \to (0 < y \leftrightarrow 0 < a)$
6		fvoveq1	$⊢ y = a \to \|y - A\| = \|a - A\|$
7		fveq2	$⊢ y = a \to denom (y) = denom (a)$
8	7	oveq1d	$⊢ y = a \to {denom (y)}^{- 2} = {denom (a)}^{- 2}$
9	6 8	breq12d	$⊢ y = a \to (\|y - A\| < {denom (y)}^{- 2} \leftrightarrow \|a - A\| < {denom (a)}^{- 2})$
10	5 9	anbi12d	$⊢ y = a \to ((0 < y \land \|y - A\| < {denom (y)}^{- 2}) \leftrightarrow (0 < a \land \|a - A\| < {denom (a)}^{- 2}))$
11	10	elrab	$⊢ a \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \leftrightarrow (a \in ℚ \land (0 < a \land \|a - A\| < {denom (a)}^{- 2}))$
12	1 4 11	sylanbrc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to a \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\}$
13		simpr2	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to \|a - A\| < B$
14		fvoveq1	$⊢ x = a \to \|x - A\| = \|a - A\|$
15	14	breq1d	$⊢ x = a \to (\|x - A\| < B \leftrightarrow \|a - A\| < B)$
16	15	rspcev	$⊢ (a \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \land \|a - A\| < B) \to \exists x \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \|x - A\| < B$
17	12 13 16	syl2anc	$⊢ (((A \in ℝ^{+} \land B \in ℝ^{+}) \land a \in ℚ) \land (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})) \to \exists x \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \|x - A\| < B$
18		irrapxlem5	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \exists a \in ℚ (0 < a \land \|a - A\| < B \land \|a - A\| < {denom (a)}^{- 2})$
19	17 18	r19.29a	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to \exists x \in \{y \in ℚ \| (0 < y \land \|y - A\| < {denom (y)}^{- 2})\} \|x - A\| < B$