# 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 )`
` |-  +`
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 ) ) ) )`