Definition df-pell1qr

Description: Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014)

	Ref	Expression
Assertion	df-pell1qr	$$⊢\mathrm{Pell1QR}=\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼\left\{y\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpell1qr	$$class\mathrm{Pell1QR}$$
1		vx	$$setvarx$$
2		cn	$$class\mathbb{N}$$
3		csquarenn	$$class{◻}_{\mathbb{N}}$$
4	2 3	cdif	$$class\left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$
5		vy	$$setvary$$
6		cr	$$classℝ$$
7		vz	$$setvarz$$
8		cn0	$$class{\mathbb{N}}_0$$
9		vw	$$setvarw$$
10	5	cv	$$setvary$$
11	7	cv	$$setvarz$$
12		caddc	$$class+$$
13		csqrt	$$class\surd$$
14	1	cv	$$setvarx$$
15	14 13	cfv	$$class\sqrt{x}$$
16		cmul	$$class\times$$
17	9	cv	$$setvarw$$
18	15 17 16	co	$$class\sqrt{x}w$$
19	11 18 12	co	$$class\left(z+\sqrt{x}w\right)$$
20	10 19	wceq	$$wffy=z+\sqrt{x}w$$
21		cexp	$$class^$$
22		c2	$$class2$$
23	11 22 21	co	$$class{z}^2$$
24		cmin	$$class-$$
25	17 22 21	co	$$class{w}^2$$
26	14 25 16	co	$$classx{w}^2$$
27	23 26 24	co	$$class\left(z^2-x{w}^2\right)$$
28		c1	$$class1$$
29	27 28	wceq	$$wff{z}^2-x{w}^2=1$$
30	20 29	wa	$$wff\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)$$
31	30 9 8	wrex	$$wff\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)$$
32	31 7 8	wrex	$$wff\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)$$
33	32 5 6	crab	$$class\left\{y\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)\right\}$$
34	1 4 33	cmpt	$$class\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼\left\{y\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)\right\}\right)$$
35	0 34	wceq	$$wff\mathrm{Pell1QR}=\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼\left\{y\in ℝ|\exists z\in {\mathbb{N}}_0\exists w\in {\mathbb{N}}_0\left(y=z+\sqrt{x}w\wedge z^2-x{w}^2=1\right)\right\}\right)$$