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	|- Pell1QR = ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpell1qr	|- Pell1QR
1		vx	|- x
2		cn	|- NN
3		csquarenn	|- []NN
4	2 3	cdif	|- ( NN \ []NN )
5		vy	|- y
6		cr	|- RR
7		vz	|- z
8		cn0	|- NN0
9		vw	|- w
10	5	cv	|- y
11	7	cv	|- z
12		caddc	|- +
13		csqrt	|- sqrt
14	1	cv	|- x
15	14 13	cfv	|- ( sqrt ` x )
16		cmul	|- x.
17	9	cv	|- w
18	15 17 16	co	|- ( ( sqrt ` x ) x. w )
19	11 18 12	co	|- ( z + ( ( sqrt ` x ) x. w ) )
20	10 19	wceq	|- y = ( z + ( ( sqrt ` x ) x. w ) )
21		cexp	|- ^
22		c2	|- 2
23	11 22 21	co	|- ( z ^ 2 )
24		cmin	|- -
25	17 22 21	co	|- ( w ^ 2 )
26	14 25 16	co	|- ( x x. ( w ^ 2 ) )
27	23 26 24	co	|- ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) )
28		c1	|- 1
29	27 28	wceq	|- ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1
30	20 29	wa	|- ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
31	30 9 8	wrex	|- E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
32	31 7 8	wrex	|- E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
33	32 5 6	crab	|- { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) }
34	1 4 33	cmpt	|- ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
35	0 34	wceq	|- Pell1QR = ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )