Definition df-rmy 37467

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

Assertion

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

Distinct variable group:   n, a, b

Detailed syntax breakdown of Definition df-rmy

Step	Hyp	Ref	Expression
1		crmy 37465	. 2 class Yrm
2		va	. . 3 setvar a
3		vn	. . 3 setvar n
4		c2 11070	. . . 4 class 2
5		cuz 11687	. . . 4 class ZZ>=
6	4, 5	cfv 5888	. . 3 class ( ZZ>= ` 2 )
7		cz 11377	. . 3 class ZZ
8	2	cv 1482	. . . . . . 7 class a
9		cexp 12860	. . . . . . . . . 10 class ^
10	8, 4, 9	co 6650	. . . . . . . . 9 class ( a ^ 2 )
11		c1 9937	. . . . . . . . 9 class 1
12		cmin 10266	. . . . . . . . 9 class -
13	10, 11, 12	co 6650	. . . . . . . 8 class ( ( a ^ 2 ) - 1 )
14		csqrt 13973	. . . . . . . 8 class sqr
15	13, 14	cfv 5888	. . . . . . 7 class ( sqr ` ( ( a ^ 2 ) - 1 ) )
16		caddc 9939	. . . . . . 7 class +
17	8, 15, 16	co 6650	. . . . . 6 class ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) )
18	3	cv 1482	. . . . . 6 class n
19	17, 18, 9	co 6650	. . . . 5 class ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n )
20		vb	. . . . . . 7 setvar b
21		cn0 11292	. . . . . . . 8 class NN0
22	21, 7	cxp 5112	. . . . . . 7 class ( NN0 X. ZZ )
23	20	cv 1482	. . . . . . . . 9 class b
24		c1st 7166	. . . . . . . . 9 class 1st
25	23, 24	cfv 5888	. . . . . . . 8 class ( 1st ` b )
26		c2nd 7167	. . . . . . . . . 10 class 2nd
27	23, 26	cfv 5888	. . . . . . . . 9 class ( 2nd ` b )
28		cmul 9941	. . . . . . . . 9 class x.
29	15, 27, 28	co 6650	. . . . . . . 8 class ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) )
30	25, 29, 16	co 6650	. . . . . . 7 class ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) )
31	20, 22, 30	cmpt 4729	. . . . . 6 class ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )
32	31	ccnv 5113	. . . . 5 class `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) )
33	19, 32	cfv 5888	. . . 4 class ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) )
34	33, 26	cfv 5888	. . 3 class ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) )
35	2, 3, 6, 7, 34	cmpt2 6652	. 2 class ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )
36	1, 35	wceq 1483	1 wff Yrm = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )

This definition is referenced by:  rmyfval  37469  frmy  37479