Metamath Proof Explorer

Definition df-rmx

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

Ref Expression
Assertion df-rmx 
|- rmX = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 1st ` ( `' ( 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 crmx 
 |-  rmX
1 va 
 |-  a
2 cuz 
 |-  ZZ>=
3 c2 
 |-  2
4 3 2 cfv 
 |-  ( ZZ>= ` 2 )
5 vn 
 |-  n
6 cz 
 |-  ZZ
7 c1st 
 |-  1st
8 vb 
 |-  b
9 cn0 
 |-  NN0
10 9 6 cxp 
 |-  ( NN0 X. ZZ )
11 8 cv 
 |-  b
12 11 7 cfv 
 |-  ( 1st ` b )
13 caddc 
 |-  +
14 csqrt 
 |-  sqrt
15 1 cv 
 |-  a
16 cexp 
 |-  ^
17 15 3 16 co 
 |-  ( a ^ 2 )
18 cmin 
 |-  -
19 c1 
 |-  1
20 17 19 18 co 
 |-  ( ( a ^ 2 ) - 1 )
21 20 14 cfv 
 |-  ( sqrt ` ( ( a ^ 2 ) - 1 ) )
22 cmul 
 |-  x.
23 c2nd 
 |-  2nd
24 11 23 cfv 
 |-  ( 2nd ` b )
25 21 24 22 co 
 |-  ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) )
26 12 25 13 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 15 21 13 co 
 |-  ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) )
30 5 cv 
 |-  n
31 29 30 16 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 
 |-  ( 1st ` ( `' ( 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 |-> ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )
35 0 34 wceq 
 |-  rmX = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )