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	⊢ Yrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2nd ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crmy	⊢ Yrm
1		va	⊢ 𝑎
2		cuz	⊢ ℤ≥
3		c2	⊢ 2
4	3 2	cfv	⊢ ( ℤ≥ ‘ 2 )
5		vn	⊢ 𝑛
6		cz	⊢ ℤ
7		c2nd	⊢ 2nd
8		vb	⊢ 𝑏
9		cn0	⊢ ℕ0
10	9 6	cxp	⊢ ( ℕ0 × ℤ )
11		c1st	⊢ 1st
12	8	cv	⊢ 𝑏
13	12 11	cfv	⊢ ( 1st ‘ 𝑏 )
14		caddc	⊢ +
15		csqrt	⊢ √
16	1	cv	⊢ 𝑎
17		cexp	⊢ ↑
18	16 3 17	co	⊢ ( 𝑎 ↑ 2 )
19		cmin	⊢ −
20		c1	⊢ 1
21	18 20 19	co	⊢ ( ( 𝑎 ↑ 2 ) − 1 )
22	21 15	cfv	⊢ ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) )
23		cmul	⊢ ·
24	12 7	cfv	⊢ ( 2nd ‘ 𝑏 )
25	22 24 23	co	⊢ ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) )
26	13 25 14	co	⊢ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) )
27	8 10 26	cmpt	⊢ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) )
28	27	ccnv	⊢ ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) )
29	16 22 14	co	⊢ ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) )
30	5	cv	⊢ 𝑛
31	29 30 17	co	⊢ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 )
32	31 28	cfv	⊢ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) )
33	32 7	cfv	⊢ ( 2nd ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) )
34	1 5 4 6 33	cmpo	⊢ ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2nd ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )
35	0 34	wceq	⊢ Yrm = ( 𝑎 ∈ ( ℤ≥ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2nd ‘ ( ◡ ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )