Metamath Proof Explorer

Theorem pellexlem4

Description: Lemma for pellex . Invoking irrapx1 , we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014)

Ref Expression
Assertion pellexlem4 ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≈ ℕ )

Proof

Step Hyp Ref Expression
1 nnex ⊢ ℕ ∈ V
2 1 1 xpex ⊢ ( ℕ × ℕ ) ∈ V
3 opabssxp ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ⊆ ( ℕ × ℕ )
4 ssdomg ⊢ ( ( ℕ × ℕ ) ∈ V → ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ⊆ ( ℕ × ℕ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ( ℕ × ℕ ) ) )
5 2 3 4 mp2 ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ( ℕ × ℕ )
6 xpnnen ⊢ ( ℕ × ℕ ) ≈ ℕ
7 domentr ⊢ ( ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ( ℕ × ℕ ) ∧ ( ℕ × ℕ ) ≈ ℕ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ℕ )
8 5 6 7 mp2an ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ℕ
9 nnrp ⊢ ( 𝐷 ∈ ℕ → 𝐷 ∈ ℝ+ )
10 9 rpsqrtcld ⊢ ( 𝐷 ∈ ℕ → ( √ ‘ 𝐷 ) ∈ ℝ+ )
11 10 anim1i ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( ( √ ‘ 𝐷 ) ∈ ℝ+ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) )
12 eldif ⊢ ( ( √ ‘ 𝐷 ) ∈ ( ℝ+ ∖ ℚ ) ↔ ( ( √ ‘ 𝐷 ) ∈ ℝ+ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) )
13 11 12 sylibr ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ( √ ‘ 𝐷 ) ∈ ( ℝ+ ∖ ℚ ) )
14 irrapx1 ⊢ ( ( √ ‘ 𝐷 ) ∈ ( ℝ+ ∖ ℚ ) → { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } ≈ ℕ )
15 ensym ⊢ ( { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } ≈ ℕ → ℕ ≈ { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } )
16 13 14 15 3syl ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ℕ ≈ { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } )
17 pellexlem3 ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } )
18 endomtr ⊢ ( ( ℕ ≈ { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } ∧ { 𝑏 ∈ ℚ ∣ ( 0 < 𝑏 ∧ ( abs ‘ ( 𝑏 − ( √ ‘ 𝐷 ) ) ) < ( ( denom ‘ 𝑏 ) ↑ - 2 ) ) } ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) → ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } )
19 16 17 18 syl2anc ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } )
20 sbth ⊢ ( ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≼ ℕ ∧ ℕ ≼ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≈ ℕ )
21 8 19 20 sylancr ⊢ ( ( 𝐷 ∈ ℕ ∧ ¬ ( √ ‘ 𝐷 ) ∈ ℚ ) → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ≠ 0 ∧ ( abs ‘ ( ( 𝑦 ↑ 2 ) − ( 𝐷 · ( 𝑧 ↑ 2 ) ) ) ) < ( 1 + ( 2 · ( √ ‘ 𝐷 ) ) ) ) ) } ≈ ℕ )