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	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → 𝑎 ∈ ℚ )
2		simpr1	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → 0 < 𝑎 )
3		simpr3	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) )
4	2 3	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
5		breq2	⊢ ( 𝑦 = 𝑎 → ( 0 < 𝑦 ↔ 0 < 𝑎 ) )
6		fvoveq1	⊢ ( 𝑦 = 𝑎 → ( abs ‘ ( 𝑦 − 𝐴 ) ) = ( abs ‘ ( 𝑎 − 𝐴 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝑎 → ( denom ‘ 𝑦 ) = ( denom ‘ 𝑎 ) )
8	7	oveq1d	⊢ ( 𝑦 = 𝑎 → ( ( denom ‘ 𝑦 ) ↑ - 2 ) = ( ( denom ‘ 𝑎 ) ↑ - 2 ) )
9	6 8	breq12d	⊢ ( 𝑦 = 𝑎 → ( ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ↔ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
10	5 9	anbi12d	⊢ ( 𝑦 = 𝑎 → ( ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) ↔ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) )
11	10	elrab	⊢ ( 𝑎 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ↔ ( 𝑎 ∈ ℚ ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) )
12	1 4 11	sylanbrc	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → 𝑎 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } )
13		simpr2	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 )
14		fvoveq1	⊢ ( 𝑥 = 𝑎 → ( abs ‘ ( 𝑥 − 𝐴 ) ) = ( abs ‘ ( 𝑎 − 𝐴 ) ) )
15	14	breq1d	⊢ ( 𝑥 = 𝑎 → ( ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 ↔ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ) )
16	15	rspcev	⊢ ( ( 𝑎 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ) → ∃ 𝑥 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 )
17	12 13 16	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) ∧ 𝑎 ∈ ℚ ) ∧ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) ) → ∃ 𝑥 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 )
18		irrapxlem5	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℚ ( 0 < 𝑎 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < 𝐵 ∧ ( abs ‘ ( 𝑎 − 𝐴 ) ) < ( ( denom ‘ 𝑎 ) ↑ - 2 ) ) )
19	17 18	r19.29a	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ∃ 𝑥 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑥 − 𝐴 ) ) < 𝐵 )