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

Definition df-rmx 27090
Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 27101 and rmxyval 27103 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
Assertion
Ref Expression
df-rmx  |- Xrm  =  (
a  e.  ( ZZ>= ` 
2 ) ,  n  e.  ZZ  |->  ( 1st `  ( `' ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  (
( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) ) `  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n ) ) ) )
Distinct variable group:    n, a, b

Detailed syntax breakdown of Definition df-rmx
StepHypRef Expression
1 crmx 27088 . 2  class Xrm
2 va . . 3  set  a
3 vn . . 3  set  n
4 c2 9811 . . . 4  class  2
5 cuz 10246 . . . 4  class  ZZ>=
64, 5cfv 5271 . . 3  class  ( ZZ>= ` 
2 )
7 cz 10040 . . 3  class  ZZ
82cv 1631 . . . . . . 7  class  a
9 cexp 11120 . . . . . . . . . 10  class  ^
108, 4, 9co 5874 . . . . . . . . 9  class  ( a ^ 2 )
11 c1 8754 . . . . . . . . 9  class  1
12 cmin 9053 . . . . . . . . 9  class  -
1310, 11, 12co 5874 . . . . . . . 8  class  ( ( a ^ 2 )  -  1 )
14 csqr 11734 . . . . . . . 8  class  sqr
1513, 14cfv 5271 . . . . . . 7  class  ( sqr `  ( ( a ^
2 )  -  1 ) )
16 caddc 8756 . . . . . . 7  class  +
178, 15, 16co 5874 . . . . . 6  class  ( a  +  ( sqr `  (
( a ^ 2 )  -  1 ) ) )
183cv 1631 . . . . . 6  class  n
1917, 18, 9co 5874 . . . . 5  class  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n )
20 vb . . . . . . 7  set  b
21 cn0 9981 . . . . . . . 8  class  NN0
2221, 7cxp 4703 . . . . . . 7  class  ( NN0 
X.  ZZ )
2320cv 1631 . . . . . . . . 9  class  b
24 c1st 6136 . . . . . . . . 9  class  1st
2523, 24cfv 5271 . . . . . . . 8  class  ( 1st `  b )
26 c2nd 6137 . . . . . . . . . 10  class  2nd
2723, 26cfv 5271 . . . . . . . . 9  class  ( 2nd `  b )
28 cmul 8758 . . . . . . . . 9  class  x.
2915, 27, 28co 5874 . . . . . . . 8  class  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) )
3025, 29, 16co 5874 . . . . . . 7  class  ( ( 1st `  b )  +  ( ( sqr `  ( ( a ^
2 )  -  1 ) )  x.  ( 2nd `  b ) ) )
3120, 22, 30cmpt 4093 . . . . . 6  class  ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  ( ( a ^
2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) )
3231ccnv 4704 . . . . 5  class  `' ( b  e.  ( NN0 
X.  ZZ )  |->  ( ( 1st `  b
)  +  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) ) ) )
3319, 32cfv 5271 . . . 4  class  ( `' ( b  e.  ( NN0  X.  ZZ ) 
|->  ( ( 1st `  b
)  +  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) ) ) ) `
 ( ( a  +  ( sqr `  (
( a ^ 2 )  -  1 ) ) ) ^ n
) )
3433, 24cfv 5271 . . 3  class  ( 1st `  ( `' ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  ( ( a ^
2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) ) `  (
( a  +  ( sqr `  ( ( a ^ 2 )  -  1 ) ) ) ^ n ) ) )
352, 3, 6, 7, 34cmpt2 5876 . 2  class  ( a  e.  ( ZZ>= `  2
) ,  n  e.  ZZ  |->  ( 1st `  ( `' ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  (
( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) ) `  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n ) ) ) )
361, 35wceq 1632 1  wff Xrm  =  (
a  e.  ( ZZ>= ` 
2 ) ,  n  e.  ZZ  |->  ( 1st `  ( `' ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  (
( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) ) `  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  rmxfval  27092  frmx  27101
  Copyright terms: Public domain W3C validator