pellexlem5

Description: Lemma for pellex . Invoking fiphp3d , we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014)

		Ref	Expression
	Assertion	pellexlem5	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists x \in ℤ (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ)$

Proof

Step	Hyp	Ref	Expression
1		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 ℕ$
2		fzfi	$⊢ (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \in Fin$
3		diffi	$⊢ (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \in Fin \to (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\} \in Fin$
4	2 3	mp1i	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\} \in Fin$
5		elopab	$⊢ a \in \{⟨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}))\} \leftrightarrow \exists y \exists z (a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))$
6		fveq2	$⊢ a = ⟨y, z⟩ \to 1^{st} (a) = 1^{st} (⟨y, z⟩)$
7	6	oveq1d	$⊢ a = ⟨y, z⟩ \to {1^{st} (a)}^{2} = {1^{st} (⟨y, z⟩)}^{2}$
8		fveq2	$⊢ a = ⟨y, z⟩ \to 2^{nd} (a) = 2^{nd} (⟨y, z⟩)$
9	8	oveq1d	$⊢ a = ⟨y, z⟩ \to {2^{nd} (a)}^{2} = {2^{nd} (⟨y, z⟩)}^{2}$
10	9	oveq2d	$⊢ a = ⟨y, z⟩ \to D {2^{nd} (a)}^{2} = D {2^{nd} (⟨y, z⟩)}^{2}$
11	7 10	oveq12d	$⊢ a = ⟨y, z⟩ \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = {1^{st} (⟨y, z⟩)}^{2} - D {2^{nd} (⟨y, z⟩)}^{2}$
12		vex	$⊢ y \in V$
13		vex	$⊢ z \in V$
14	12 13	op1st	$⊢ 1^{st} (⟨y, z⟩) = y$
15	14	oveq1i	$⊢ {1^{st} (⟨y, z⟩)}^{2} = y^{2}$
16	12 13	op2nd	$⊢ 2^{nd} (⟨y, z⟩) = z$
17	16	oveq1i	$⊢ {2^{nd} (⟨y, z⟩)}^{2} = z^{2}$
18	17	oveq2i	$⊢ D {2^{nd} (⟨y, z⟩)}^{2} = D z^{2}$
19	15 18	oveq12i	$⊢ {1^{st} (⟨y, z⟩)}^{2} - D {2^{nd} (⟨y, z⟩)}^{2} = y^{2} - D z^{2}$
20	11 19	eqtrdi	$⊢ a = ⟨y, z⟩ \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = y^{2} - D z^{2}$
21	20	ad2antrl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = y^{2} - D z^{2}$
22		simprrl	$⊢ (D \in ℕ \land (a = ⟨y, z⟩ \land ((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 \in ℕ \land z \in ℕ)$
23		simpl	$⊢ (D \in ℕ \land (a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to D \in ℕ$
24		simprr	$⊢ ((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^{2} - D z^{2}\| < 1 + 2 \sqrt{D}$
25	24	ad2antll	$⊢ (D \in ℕ \land (a = ⟨y, z⟩ \land ((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^{2} - D z^{2}\| < 1 + 2 \sqrt{D}$
26		nnz	$⊢ y \in ℕ \to y \in ℤ$
27	26	ad2antrr	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to y \in ℤ$
28		zsqcl	$⊢ y \in ℤ \to y^{2} \in ℤ$
29	27 28	syl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to y^{2} \in ℤ$
30		nnz	$⊢ D \in ℕ \to D \in ℤ$
31	30	ad2antrl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to D \in ℤ$
32		simplr	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to z \in ℕ$
33	32	nnzd	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to z \in ℤ$
34		zsqcl	$⊢ z \in ℤ \to z^{2} \in ℤ$
35	33 34	syl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to z^{2} \in ℤ$
36	31 35	zmulcld	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to D z^{2} \in ℤ$
37	29 36	zsubcld	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to y^{2} - D z^{2} \in ℤ$
38		1re	$⊢ 1 \in ℝ$
39		2re	$⊢ 2 \in ℝ$
40		nnre	$⊢ D \in ℕ \to D \in ℝ$
41	40	ad2antrl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to D \in ℝ$
42		nnnn0	$⊢ D \in ℕ \to D \in ℕ_{0}$
43	42	ad2antrl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to D \in ℕ_{0}$
44	43	nn0ge0d	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to 0 \leq D$
45	41 44	resqrtcld	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \sqrt{D} \in ℝ$
46		remulcl	$⊢ (2 \in ℝ \land \sqrt{D} \in ℝ) \to 2 \sqrt{D} \in ℝ$
47	39 45 46	sylancr	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to 2 \sqrt{D} \in ℝ$
48		readdcl	$⊢ (1 \in ℝ \land 2 \sqrt{D} \in ℝ) \to 1 + 2 \sqrt{D} \in ℝ$
49	38 47 48	sylancr	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to 1 + 2 \sqrt{D} \in ℝ$
50	49	flcld	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to ⌊1 + 2 \sqrt{D}⌋ \in ℤ$
51	50	znegcld	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to - ⌊1 + 2 \sqrt{D}⌋ \in ℤ$
52	37	zred	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to y^{2} - D z^{2} \in ℝ$
53	50	zred	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to ⌊1 + 2 \sqrt{D}⌋ \in ℝ$
54		nn0abscl	$⊢ y^{2} - D z^{2} \in ℤ \to \|y^{2} - D z^{2}\| \in ℕ_{0}$
55	37 54	syl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| \in ℕ_{0}$
56	55	nn0zd	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| \in ℤ$
57	56	zred	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| \in ℝ$
58		peano2re	$⊢ ⌊1 + 2 \sqrt{D}⌋ \in ℝ \to ⌊1 + 2 \sqrt{D}⌋ + 1 \in ℝ$
59	53 58	syl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to ⌊1 + 2 \sqrt{D}⌋ + 1 \in ℝ$
60		simprr	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}$
61		flltp1	$⊢ 1 + 2 \sqrt{D} \in ℝ \to 1 + 2 \sqrt{D} < ⌊1 + 2 \sqrt{D}⌋ + 1$
62	49 61	syl	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to 1 + 2 \sqrt{D} < ⌊1 + 2 \sqrt{D}⌋ + 1$
63	57 49 59 60 62	lttrd	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| < ⌊1 + 2 \sqrt{D}⌋ + 1$
64		zleltp1	$⊢ (\|y^{2} - D z^{2}\| \in ℤ \land ⌊1 + 2 \sqrt{D}⌋ \in ℤ) \to (\|y^{2} - D z^{2}\| \leq ⌊1 + 2 \sqrt{D}⌋ \leftrightarrow \|y^{2} - D z^{2}\| < ⌊1 + 2 \sqrt{D}⌋ + 1)$
65	56 50 64	syl2anc	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to (\|y^{2} - D z^{2}\| \leq ⌊1 + 2 \sqrt{D}⌋ \leftrightarrow \|y^{2} - D z^{2}\| < ⌊1 + 2 \sqrt{D}⌋ + 1)$
66	63 65	mpbird	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to \|y^{2} - D z^{2}\| \leq ⌊1 + 2 \sqrt{D}⌋$
67		absle	$⊢ (y^{2} - D z^{2} \in ℝ \land ⌊1 + 2 \sqrt{D}⌋ \in ℝ) \to (\|y^{2} - D z^{2}\| \leq ⌊1 + 2 \sqrt{D}⌋ \leftrightarrow (- ⌊1 + 2 \sqrt{D}⌋ \leq y^{2} - D z^{2} \land y^{2} - D z^{2} \leq ⌊1 + 2 \sqrt{D}⌋))$
68	67	biimpa	$⊢ ((y^{2} - D z^{2} \in ℝ \land ⌊1 + 2 \sqrt{D}⌋ \in ℝ) \land \|y^{2} - D z^{2}\| \leq ⌊1 + 2 \sqrt{D}⌋) \to (- ⌊1 + 2 \sqrt{D}⌋ \leq y^{2} - D z^{2} \land y^{2} - D z^{2} \leq ⌊1 + 2 \sqrt{D}⌋)$
69	52 53 66 68	syl21anc	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to (- ⌊1 + 2 \sqrt{D}⌋ \leq y^{2} - D z^{2} \land y^{2} - D z^{2} \leq ⌊1 + 2 \sqrt{D}⌋)$
70		elfz	$⊢ (y^{2} - D z^{2} \in ℤ \land - ⌊1 + 2 \sqrt{D}⌋ \in ℤ \land ⌊1 + 2 \sqrt{D}⌋ \in ℤ) \to (y^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \leftrightarrow (- ⌊1 + 2 \sqrt{D}⌋ \leq y^{2} - D z^{2} \land y^{2} - D z^{2} \leq ⌊1 + 2 \sqrt{D}⌋))$
71	70	biimpar	$⊢ ((y^{2} - D z^{2} \in ℤ \land - ⌊1 + 2 \sqrt{D}⌋ \in ℤ \land ⌊1 + 2 \sqrt{D}⌋ \in ℤ) \land (- ⌊1 + 2 \sqrt{D}⌋ \leq y^{2} - D z^{2} \land y^{2} - D z^{2} \leq ⌊1 + 2 \sqrt{D}⌋)) \to y^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋)$
72	37 51 50 69 71	syl31anc	$⊢ ((y \in ℕ \land z \in ℕ) \land (D \in ℕ \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})) \to y^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋)$
73	22 23 25 72	syl12anc	$⊢ (D \in ℕ \land (a = ⟨y, z⟩ \land ((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^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋)$
74	73	adantlr	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a = ⟨y, z⟩ \land ((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^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋)$
75		simprl	$⊢ ((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^{2} - D z^{2} \neq 0$
76	75	ad2antll	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a = ⟨y, z⟩ \land ((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^{2} - D z^{2} \neq 0$
77		eldifsn	$⊢ y^{2} - D z^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \leftrightarrow (y^{2} - D z^{2} \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \land y^{2} - D z^{2} \neq 0)$
78	74 76 77	sylanbrc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a = ⟨y, z⟩ \land ((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^{2} - D z^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\})$
79	21 78	eqeltrd	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\})$
80	79	ex	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))) \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}))$
81	80	exlimdvv	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (\exists y \exists z (a = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))) \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}))$
82	5 81	biimtrid	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (a \in \{⟨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 {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}))$
83	82	imp	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land a \in \{⟨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 {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\})$
84	1 4 83	fiphp3d	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ$
85		eldif	$⊢ x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \leftrightarrow (x \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \land \neg x \in \{0\})$
86		elfzelz	$⊢ x \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \to x \in ℤ$
87		simp2	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land x \in ℤ \land \neg x \in \{0\}) \to x \in ℤ$
88		velsn	$⊢ x \in \{0\} \leftrightarrow x = 0$
89	88	biimpri	$⊢ x = 0 \to x \in \{0\}$
90	89	necon3bi	$⊢ \neg x \in \{0\} \to x \neq 0$
91	90	3ad2ant3	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land x \in ℤ \land \neg x \in \{0\}) \to x \neq 0$
92	87 91	jca	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land x \in ℤ \land \neg x \in \{0\}) \to (x \in ℤ \land x \neq 0)$
93	92	3exp	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (x \in ℤ \to (\neg x \in \{0\} \to (x \in ℤ \land x \neq 0)))$
94	86 93	syl5	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (x \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \to (\neg x \in \{0\} \to (x \in ℤ \land x \neq 0)))$
95	94	impd	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((x \in (- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) \land \neg x \in \{0\}) \to (x \in ℤ \land x \neq 0))$
96	85 95	biimtrid	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \to (x \in ℤ \land x \neq 0))$
97		simp2l	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to x \in ℤ$
98		simp2r	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to x \neq 0$
99		nnex	$⊢ ℕ \in V$
100	99 99	xpex	$⊢ ℕ \times ℕ \in V$
101		opabssxp	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \subseteq ℕ \times ℕ$
102		ssdomg	$⊢ ℕ \times ℕ \in V \to (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \subseteq ℕ \times ℕ \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ (ℕ \times ℕ))$
103	100 101 102	mp2	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ (ℕ \times ℕ)$
104		xpnnen	$⊢ (ℕ \times ℕ) \approx ℕ$
105		domentr	$⊢ (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ (ℕ \times ℕ) \land (ℕ \times ℕ) \approx ℕ) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ ℕ$
106	103 104 105	mp2an	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ ℕ$
107		ensym	$⊢ \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ \to ℕ \approx \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\}$
108	107	3ad2ant3	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to ℕ \approx \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\}$
109	100 101	ssexi	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \in V$
110		fveq2	$⊢ a = b \to 1^{st} (a) = 1^{st} (b)$
111	110	oveq1d	$⊢ a = b \to {1^{st} (a)}^{2} = {1^{st} (b)}^{2}$
112		fveq2	$⊢ a = b \to 2^{nd} (a) = 2^{nd} (b)$
113	112	oveq1d	$⊢ a = b \to {2^{nd} (a)}^{2} = {2^{nd} (b)}^{2}$
114	113	oveq2d	$⊢ a = b \to D {2^{nd} (a)}^{2} = D {2^{nd} (b)}^{2}$
115	111 114	oveq12d	$⊢ a = b \to {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2}$
116	115	eqeq1d	$⊢ a = b \to ({1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x \leftrightarrow {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x)$
117	116	elrab	$⊢ b \in \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \leftrightarrow (b \in \{⟨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 {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x)$
118		simprl	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to b = ⟨y, z⟩$
119		simprrl	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((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 \in ℕ \land z \in ℕ)$
120		fveq2	$⊢ b = ⟨y, z⟩ \to 1^{st} (b) = 1^{st} (⟨y, z⟩)$
121	120	oveq1d	$⊢ b = ⟨y, z⟩ \to {1^{st} (b)}^{2} = {1^{st} (⟨y, z⟩)}^{2}$
122		fveq2	$⊢ b = ⟨y, z⟩ \to 2^{nd} (b) = 2^{nd} (⟨y, z⟩)$
123	122	oveq1d	$⊢ b = ⟨y, z⟩ \to {2^{nd} (b)}^{2} = {2^{nd} (⟨y, z⟩)}^{2}$
124	123	oveq2d	$⊢ b = ⟨y, z⟩ \to D {2^{nd} (b)}^{2} = D {2^{nd} (⟨y, z⟩)}^{2}$
125	121 124	oveq12d	$⊢ b = ⟨y, z⟩ \to {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = {1^{st} (⟨y, z⟩)}^{2} - D {2^{nd} (⟨y, z⟩)}^{2}$
126	125 19	eqtr2di	$⊢ b = ⟨y, z⟩ \to y^{2} - D z^{2} = {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2}$
127	126	ad2antrl	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((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^{2} - D z^{2} = {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2}$
128		simplr	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x$
129	127 128	eqtrd	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((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^{2} - D z^{2} = x$
130	118 119 129	jca32	$⊢ ((((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \land (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))) \to (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x))$
131	130	ex	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \to ((b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))) \to (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)))$
132	131	2eximdv	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \to (\exists y \exists z (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D}))) \to \exists y \exists z (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)))$
133		elopab	$⊢ b \in \{⟨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}))\} \leftrightarrow \exists y \exists z (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land (y^{2} - D z^{2} \neq 0 \land \|y^{2} - D z^{2}\| < 1 + 2 \sqrt{D})))$
134		elopab	$⊢ b \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \leftrightarrow \exists y \exists z (b = ⟨y, z⟩ \land ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x))$
135	132 133 134	3imtr4g	$⊢ (((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \land {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \to (b \in \{⟨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 b \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\})$
136	135	expimpd	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \to (({1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x \land b \in \{⟨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 b \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\})$
137	136	ancomsd	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \to ((b \in \{⟨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 {1^{st} (b)}^{2} - D {2^{nd} (b)}^{2} = x) \to b \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\})$
138	117 137	biimtrid	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \to (b \in \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \to b \in \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\})$
139	138	ssrdv	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0)) \to \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \subseteq \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}$
140	139	3adant3	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \subseteq \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}$
141		ssdomg	$⊢ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \in V \to (\{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \subseteq \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \to \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\})$
142	109 140 141	mpsyl	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}$
143		endomtr	$⊢ (ℕ \approx \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}) \to ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}$
144	108 142 143	syl2anc	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}$
145		sbth	$⊢ (\{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} ≼ ℕ \land ℕ ≼ \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\}) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ$
146	106 144 145	sylancr	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ$
147	97 98 146	jca32	$⊢ ((D \in ℕ \land \neg \sqrt{D} \in ℚ) \land (x \in ℤ \land x \neq 0) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to (x \in ℤ \land (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ))$
148	147	3exp	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((x \in ℤ \land x \neq 0) \to (\{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ \to (x \in ℤ \land (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ))))$
149	96 148	syld	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \to (\{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ \to (x \in ℤ \land (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ))))$
150	149	impd	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to ((x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \land \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ) \to (x \in ℤ \land (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ)))$
151	150	reximdv2	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to (\exists x \in ((- ⌊1 + 2 \sqrt{D}⌋ \dots ⌊1 + 2 \sqrt{D}⌋) ∖ \{0\}) \{a \in \{⟨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}))\} \| {1^{st} (a)}^{2} - D {2^{nd} (a)}^{2} = x\} \approx ℕ \to \exists x \in ℤ (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ))$
152	84 151	mpd	$⊢ (D \in ℕ \land \neg \sqrt{D} \in ℚ) \to \exists x \in ℤ (x \neq 0 \land \{⟨y, z⟩ \| ((y \in ℕ \land z \in ℕ) \land y^{2} - D z^{2} = x)\} \approx ℕ)$

Metamath Proof Explorer

Theorem pellexlem5

Proof