df-pell1234qr

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

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

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

Metamath Proof Explorer