Metamath Proof Explorer

Definition df-rmy

Description: Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy and rmxyval for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion df-rmy 
|- rmY = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crmy 
 |-  rmY
1 va 
 |-  a
2 cuz 
 |-  ZZ>=
3 c2 
 |-  2
4 3 2 cfv 
 |-  ( ZZ>= ` 2 )
5 vn 
 |-  n
6 cz 
 |-  ZZ
7 c2nd 
 |-  2nd
8 vb 
 |-  b
9 cn0 
 |-  NN0
10 9 6 cxp 
 |-  ( NN0 X. ZZ )
11 c1st 
 |-  1st
12 8 cv 
 |-  b
13 12 11 cfv 
 |-  ( 1st ` b )
14 caddc 
 |-  +
15 csqrt 
 |-  sqrt
16 1 cv 
 |-  a
17 cexp 
 |-  ^
18 16 3 17 co 
 |-  ( a ^ 2 )
19 cmin 
 |-  -
20 c1 
 |-  1
21 18 20 19 co 
 |-  ( ( a ^ 2 ) - 1 )
22 21 15 cfv 
 |-  ( sqrt ` ( ( a ^ 2 ) - 1 ) )
23 cmul 
 |-  x.
24 12 7 cfv 
 |-  ( 2nd ` b )
25 22 24 23 co 
 |-  ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) )
26 13 25 14 co 
 |-  ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) )
27 8 10 26 cmpt 
 |-  ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )
28 27 ccnv 
 |-  `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )
29 16 22 14 co 
 |-  ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) )
30 5 cv 
 |-  n
31 29 30 17 co 
 |-  ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n )
32 31 28 cfv 
 |-  ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) )
33 32 7 cfv 
 |-  ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) )
34 1 5 4 6 33 cmpo 
 |-  ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )
35 0 34 wceq 
 |-  rmY = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )