Metamath Proof Explorer

Theorem irrapx1

Description: Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in vandenDries p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion irrapx1 ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ≈ ℕ )

Proof

Step Hyp Ref Expression
1 qnnen ⊢ ℚ ≈ ℕ
2 nnenom ⊢ ℕ ≈ ω
3 1 2 entri ⊢ ℚ ≈ ω
4 3 2 pm3.2i ⊢ ( ℚ ≈ ω ∧ ℕ ≈ ω )
5 ssrab2 ⊢ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℚ
6 qssre ⊢ ℚ ⊆ ℝ
7 5 6 sstri ⊢ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℝ
8 7 a1i ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℝ )
9 eldifi ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → 𝐴 ∈ ℝ+ )
10 9 rpred ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → 𝐴 ∈ ℝ )
11 eldifn ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → ¬ 𝐴 ∈ ℚ )
12 elrabi ⊢ ( 𝐴 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } → 𝐴 ∈ ℚ )
13 11 12 nsyl ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → ¬ 𝐴 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } )
14 irrapxlem6 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑏 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑏 − 𝐴 ) ) < 𝑎 )
15 9 14 sylan ⊢ ( ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) ∧ 𝑎 ∈ ℝ+ ) → ∃ 𝑏 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑏 − 𝐴 ) ) < 𝑎 )
16 15 ralrimiva ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑏 − 𝐴 ) ) < 𝑎 )
17 rencldnfi ⊢ ( ( ( { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℝ ∧ 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ) ∧ ∀ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ( abs ‘ ( 𝑏 − 𝐴 ) ) < 𝑎 ) → ¬ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ∈ Fin )
18 8 10 13 16 17 syl31anc ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → ¬ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ∈ Fin )
19 18 5 jctil ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → ( { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℚ ∧ ¬ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ∈ Fin ) )
20 ctbnfien ⊢ ( ( ( ℚ ≈ ω ∧ ℕ ≈ ω ) ∧ ( { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ⊆ ℚ ∧ ¬ { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ∈ Fin ) ) → { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ≈ ℕ )
21 4 19 20 sylancr ⊢ ( 𝐴 ∈ ( ℝ+ ∖ ℚ ) → { 𝑦 ∈ ℚ ∣ ( 0 < 𝑦 ∧ ( abs ‘ ( 𝑦 − 𝐴 ) ) < ( ( denom ‘ 𝑦 ) ↑ - 2 ) ) } ≈ ℕ )