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