Definition df-pell1qr 37406

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.)

Assertion

Ref	Expression
df-pell1qr	|- Pell1QR = ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )

Distinct variable group:   x, y, z, w

Detailed syntax breakdown of Definition df-pell1qr

Step	Hyp	Ref	Expression
1		cpell1qr 37401	. 2 class Pell1QR
2		vx	. . 3 setvar x
3		cn 11020	. . . 4 class NN
4		csquarenn 37400	. . . 4 class ◻NN
5	3, 4	cdif 3571	. . 3 class ( NN \ ◻NN )
6		vy	. . . . . . . . 9 setvar y
7	6	cv 1482	. . . . . . . 8 class y
8		vz	. . . . . . . . . 10 setvar z
9	8	cv 1482	. . . . . . . . 9 class z
10	2	cv 1482	. . . . . . . . . . 11 class x
11		csqrt 13973	. . . . . . . . . . 11 class sqr
12	10, 11	cfv 5888	. . . . . . . . . 10 class ( sqr ` x )
13		vw	. . . . . . . . . . 11 setvar w
14	13	cv 1482	. . . . . . . . . 10 class w
15		cmul 9941	. . . . . . . . . 10 class x.
16	12, 14, 15	co 6650	. . . . . . . . 9 class ( ( sqr ` x ) x. w )
17		caddc 9939	. . . . . . . . 9 class +
18	9, 16, 17	co 6650	. . . . . . . 8 class ( z + ( ( sqr ` x ) x. w ) )
19	7, 18	wceq 1483	. . . . . . 7 wff y = ( z + ( ( sqr ` x ) x. w ) )
20		c2 11070	. . . . . . . . . 10 class 2
21		cexp 12860	. . . . . . . . . 10 class ^
22	9, 20, 21	co 6650	. . . . . . . . 9 class ( z ^ 2 )
23	14, 20, 21	co 6650	. . . . . . . . . 10 class ( w ^ 2 )
24	10, 23, 15	co 6650	. . . . . . . . 9 class ( x x. ( w ^ 2 ) )
25		cmin 10266	. . . . . . . . 9 class -
26	22, 24, 25	co 6650	. . . . . . . 8 class ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) )
27		c1 9937	. . . . . . . 8 class 1
28	26, 27	wceq 1483	. . . . . . 7 wff ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1
29	19, 28	wa 384	. . . . . 6 wff ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
30		cn0 11292	. . . . . 6 class NN0
31	29, 13, 30	wrex 2913	. . . . 5 wff E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
32	31, 8, 30	wrex 2913	. . . 4 wff E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
33		cr 9935	. . . 4 class RR
34	32, 6, 33	crab 2916	. . 3 class { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) }
35	2, 5, 34	cmpt 4729	. 2 class ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
36	1, 35	wceq 1483	1 wff Pell1QR = ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )

This definition is referenced by:  pell1qrval  37410