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

Definition df-rmy 26988
Description: Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 26999 and rmxyval 27000 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
Assertion
Ref Expression
df-rmy  |- Yrm  =  (
a  e.  ( ZZ>= ` 
2 ) ,  n  e.  ZZ  |->  ( 2nd `  ( `' ( 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-rmy
StepHypRef Expression
1 crmy 26986 . 2  class Yrm
2 va . . 3  set  a
3 vn . . 3  set  n
4 c2 9795 . . . 4  class  2
5 cuz 10230 . . . 4  class  ZZ>=
64, 5cfv 5255 . . 3  class  ( ZZ>= ` 
2 )
7 cz 10024 . . 3  class  ZZ
82cv 1622 . . . . . . 7  class  a
9 cexp 11104 . . . . . . . . . 10  class  ^
108, 4, 9co 5858 . . . . . . . . 9  class  ( a ^ 2 )
11 c1 8738 . . . . . . . . 9  class  1
12 cmin 9037 . . . . . . . . 9  class  -
1310, 11, 12co 5858 . . . . . . . 8  class  ( ( a ^ 2 )  -  1 )
14 csqr 11718 . . . . . . . 8  class  sqr
1513, 14cfv 5255 . . . . . . 7  class  ( sqr `  ( ( a ^
2 )  -  1 ) )
16 caddc 8740 . . . . . . 7  class  +
178, 15, 16co 5858 . . . . . 6  class  ( a  +  ( sqr `  (
( a ^ 2 )  -  1 ) ) )
183cv 1622 . . . . . 6  class  n
1917, 18, 9co 5858 . . . . 5  class  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n )
20 vb . . . . . . 7  set  b
21 cn0 9965 . . . . . . . 8  class  NN0
2221, 7cxp 4687 . . . . . . 7  class  ( NN0 
X.  ZZ )
2320cv 1622 . . . . . . . . 9  class  b
24 c1st 6120 . . . . . . . . 9  class  1st
2523, 24cfv 5255 . . . . . . . 8  class  ( 1st `  b )
26 c2nd 6121 . . . . . . . . . 10  class  2nd
2723, 26cfv 5255 . . . . . . . . 9  class  ( 2nd `  b )
28 cmul 8742 . . . . . . . . 9  class  x.
2915, 27, 28co 5858 . . . . . . . 8  class  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) )
3025, 29, 16co 5858 . . . . . . 7  class  ( ( 1st `  b )  +  ( ( sqr `  ( ( a ^
2 )  -  1 ) )  x.  ( 2nd `  b ) ) )
3120, 22, 30cmpt 4077 . . . . . 6  class  ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  ( ( a ^
2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) )
3231ccnv 4688 . . . . 5  class  `' ( b  e.  ( NN0 
X.  ZZ )  |->  ( ( 1st `  b
)  +  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) ) ) )
3319, 32cfv 5255 . . . 4  class  ( `' ( b  e.  ( NN0  X.  ZZ ) 
|->  ( ( 1st `  b
)  +  ( ( sqr `  ( ( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b
) ) ) ) `
 ( ( a  +  ( sqr `  (
( a ^ 2 )  -  1 ) ) ) ^ n
) )
3433, 26cfv 5255 . . 3  class  ( 2nd `  ( `' ( 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 5860 . 2  class  ( a  e.  ( ZZ>= `  2
) ,  n  e.  ZZ  |->  ( 2nd `  ( `' ( b  e.  ( NN0  X.  ZZ )  |->  ( ( 1st `  b )  +  ( ( sqr `  (
( a ^ 2 )  -  1 ) )  x.  ( 2nd `  b ) ) ) ) `  ( ( a  +  ( sqr `  ( ( a ^
2 )  -  1 ) ) ) ^
n ) ) ) )
361, 35wceq 1623 1  wff Yrm  =  (
a  e.  ( ZZ>= ` 
2 ) ,  n  e.  ZZ  |->  ( 2nd `  ( `' ( 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:  rmyfval  26990  frmy  26999
  Copyright terms: Public domain W3C validator