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 ) ) ) )