Metamath Proof Explorer

Definition 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 e. ( NN \ []NN ) |-> { y e. RR | E. z e. ZZ 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 cpell1234qr 
 |-  Pell1234QR
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 cz 
 |-  ZZ
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. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
32 31 7 8 wrex 
 |-  E. z e. ZZ E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 )
33 32 5 6 crab 
 |-  { y e. RR | E. z e. ZZ E. w e. ZZ ( 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. ZZ E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
35 0 34 wceq 
 |-  Pell1234QR = ( x e. ( NN \ []NN ) |-> { y e. RR | E. z e. ZZ E. w e. ZZ ( y = ( z + ( ( sqrt ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )