Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pell14qr Structured version   Unicode version

Definition df-pell14qr 26908
Description: Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
Assertion
Ref Expression
df-pell14qr  |- Pell14QR  =  ( x  e.  ( NN 
\NN )  |->  { y  e.  RR  |  E. z  e.  NN0  E. w  e.  ZZ  ( 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-pell14qr
StepHypRef Expression
1 cpell14qr 26904 . 2  class Pell14QR
2 vx . . 3  set  x
3 cn 10002 . . . 4  class  NN
4 csquarenn 26901 . . . 4  classNN
53, 4cdif 3319 . . 3  class  ( NN 
\NN )
6 vy . . . . . . . . 9  set  y
76cv 1652 . . . . . . . 8  class  y
8 vz . . . . . . . . . 10  set  z
98cv 1652 . . . . . . . . 9  class  z
102cv 1652 . . . . . . . . . . 11  class  x
11 csqr 12040 . . . . . . . . . . 11  class  sqr
1210, 11cfv 5456 . . . . . . . . . 10  class  ( sqr `  x )
13 vw . . . . . . . . . . 11  set  w
1413cv 1652 . . . . . . . . . 10  class  w
15 cmul 8997 . . . . . . . . . 10  class  x.
1612, 14, 15co 6083 . . . . . . . . 9  class  ( ( sqr `  x )  x.  w )
17 caddc 8995 . . . . . . . . 9  class  +
189, 16, 17co 6083 . . . . . . . 8  class  ( z  +  ( ( sqr `  x )  x.  w
) )
197, 18wceq 1653 . . . . . . 7  wff  y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )
20 c2 10051 . . . . . . . . . 10  class  2
21 cexp 11384 . . . . . . . . . 10  class  ^
229, 20, 21co 6083 . . . . . . . . 9  class  ( z ^ 2 )
2314, 20, 21co 6083 . . . . . . . . . 10  class  ( w ^ 2 )
2410, 23, 15co 6083 . . . . . . . . 9  class  ( x  x.  ( w ^
2 ) )
25 cmin 9293 . . . . . . . . 9  class  -
2622, 24, 25co 6083 . . . . . . . 8  class  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )
27 c1 8993 . . . . . . . 8  class  1
2826, 27wceq 1653 . . . . . . 7  wff  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1
2919, 28wa 360 . . . . . 6  wff  ( y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )  /\  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1 )
30 cz 10284 . . . . . 6  class  ZZ
3129, 13, 30wrex 2708 . . . . 5  wff  E. w  e.  ZZ  ( y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )  /\  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1 )
32 cn0 10223 . . . . 5  class  NN0
3331, 8, 32wrex 2708 . . . 4  wff  E. z  e.  NN0  E. w  e.  ZZ  ( y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )  /\  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1 )
34 cr 8991 . . . 4  class  RR
3533, 6, 34crab 2711 . . 3  class  { y  e.  RR  |  E. z  e.  NN0  E. w  e.  ZZ  ( y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )  /\  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1 ) }
362, 5, 35cmpt 4268 . 2  class  ( x  e.  ( NN  \NN )  |->  { y  e.  RR  |  E. z  e.  NN0  E. w  e.  ZZ  (
y  =  ( z  +  ( ( sqr `  x )  x.  w
) )  /\  (
( z ^ 2 )  -  ( x  x.  ( w ^
2 ) ) )  =  1 ) } )
371, 36wceq 1653 1  wff Pell14QR  =  ( x  e.  ( NN 
\NN )  |->  { y  e.  RR  |  E. z  e.  NN0  E. w  e.  ZZ  ( y  =  ( z  +  ( ( sqr `  x
)  x.  w ) )  /\  ( ( z ^ 2 )  -  ( x  x.  ( w ^ 2 ) ) )  =  1 ) } )
Colors of variables: wff set class
This definition is referenced by:  pell14qrval  26913
  Copyright terms: Public domain W3C validator