df-pell14qr

Description: Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014)

		Ref	Expression
	Assertion	df-pell14qr	$⊢ Pell14QR = (x \in (ℕ ∖ ◻_{ℕ}) ⟼ \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)\})$

Step	Hyp	Ref	Expression
0		cpell14qr	$class Pell14QR$
1		vx	$setvar x$
2		cn	$class ℕ$
3		csquarenn	$class ◻_{ℕ}$
4	2 3	cdif	$class (ℕ ∖ ◻_{ℕ})$
5		vy	$setvar y$
6		cr	$class ℝ$
7		vz	$setvar z$
8		cn0	$class ℕ_{0}$
9		vw	$setvar w$
10		cz	$class ℤ$
11	5	cv	$setvar y$
12	7	cv	$setvar z$
13		caddc	$class +$
14		csqrt	$class \sqrt$
15	1	cv	$setvar x$
16	15 14	cfv	$class \sqrt{x}$
17		cmul	$class \times$
18	9	cv	$setvar w$
19	16 18 17	co	$class \sqrt{x} w$
20	12 19 13	co	$class (z + \sqrt{x} w)$
21	11 20	wceq	$wff y = z + \sqrt{x} w$
22		cexp	$class^$
23		c2	$class 2$
24	12 23 22	co	$class z^{2}$
25		cmin	$class -$
26	18 23 22	co	$class w^{2}$
27	15 26 17	co	$class x w^{2}$
28	24 27 25	co	$class (z^{2} - x w^{2})$
29		c1	$class 1$
30	28 29	wceq	$wff z^{2} - x w^{2} = 1$
31	21 30	wa	$wff (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)$
32	31 9 10	wrex	$wff \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)$
33	32 7 8	wrex	$wff \exists z \in ℕ_{0} \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)$
34	33 5 6	crab	$class \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)\}$
35	1 4 34	cmpt	$class (x \in (ℕ ∖ ◻_{ℕ}) ⟼ \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)\})$
36	0 35	wceq	$wff Pell14QR = (x \in (ℕ ∖ ◻_{ℕ}) ⟼ \{y \in ℝ \| \exists z \in ℕ_{0} \exists w \in ℤ (y = z + \sqrt{x} w \land z^{2} - x w^{2} = 1)\})$

Metamath Proof Explorer