Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpell14qr 
 |-  Pell14QR
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 cz 
 |-  ZZ
11 5 cv 
 |-  y
12 7 cv 
 |-  z
13 caddc 
 |-  +
14 csqrt 
 |-  sqrt
15 1 cv 
 |-  x
16 15 14 cfv 
 |-  ( sqrt ` x )
17 cmul 
 |-  x.
18 9 cv 
 |-  w
19 16 18 17 co 
 |-  ( ( sqrt ` x ) x. w )
20 12 19 13 co 
 |-  ( z + ( ( sqrt ` x ) x. w ) )
21 11 20 wceq 
 |-  y = ( z + ( ( sqrt ` x ) x. w ) )
22 cexp 
 |-  ^
23 c2 
 |-  2
24 12 23 22 co 
 |-  ( z ^ 2 )
25 cmin 
 |-  -
26 18 23 22 co 
 |-  ( w ^ 2 )
27 15 26 17 co 
 |-  ( x x. ( w ^ 2 ) )
28 24 27 25 co 
 |-  ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) )
29 c1 
 |-  1
30 28 29 wceq 
 |-  ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1
31 21 30 wa 
 |-  ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
32 31 9 10 wrex 
 |-  E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
33 32 7 8 wrex 
 |-  E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
34 33 5 6 crab 
 |-  { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) }
35 1 4 34 cmpt 
 |-  ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
36 0 35 wceq 
 |-  Pell14QR = ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )