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	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \approx ℕ$

Proof

Step	Hyp	Ref	Expression
1		nnex	$⊢ ℕ \in V$
2	1 1	xpex	$⊢ ℕ \times ℕ \in V$
3		opabssxp	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \subseteq ℕ \times ℕ$
4		ssdomg	$⊢ ℕ \times ℕ \in V \to (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \subseteq ℕ \times ℕ \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ (ℕ \times ℕ))$
5	2 3 4	mp2	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ (ℕ \times ℕ)$
6		xpnnen	$⊢ (ℕ \times ℕ) \approx ℕ$
7		domentr	$⊢ (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ (ℕ \times ℕ) \land (ℕ \times ℕ) \approx ℕ) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ ℕ$
8	5 6 7	mp2an	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ ℕ$
9		nnrp	$⊢ D \in ℕ \to D \in ℝ^{+}$
10	9	rpsqrtcld	$⊢ D \in ℕ \to \sqrt{D} \in ℝ^{+}$
11	10	anim1i	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (\sqrt{D} \in ℝ^{+} \land \neg \sqrt{D} \in ℚ)$
12		eldif	$⊢ \sqrt{D} \in (ℝ^{+} ∖ ℚ) \leftrightarrow (\sqrt{D} \in ℝ^{+} \land \neg \sqrt{D} \in ℚ)$
13	11 12	sylibr	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \sqrt{D} \in (ℝ^{+} ∖ ℚ)$
14		irrapx1	$⊢ \sqrt{D} \in (ℝ^{+} ∖ ℚ) \to \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\} \approx ℕ$
15		ensym	$⊢ \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\} \approx ℕ \to ℕ \approx \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\}$
16	13 14 15	3syl	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ℕ \approx \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\}$
17		pellexlem3	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}$
18		endomtr	$⊢ (ℕ \approx \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\} \land \{b \in ℚ \| (0 < b \land \|b - \sqrt{D}\| < {denom (b)}^{- 2})\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}) \to ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}$
19	16 17 18	syl2anc	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}$
20		sbth	$⊢ (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} ≼ ℕ \land ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\}) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \approx ℕ$
21	8 19 20	sylancr	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))\} \approx ℕ$

Metamath Proof Explorer

Theorem pellexlem4

Proof