# 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 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𝑏 )
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 ) ) ) ↑ 𝑛 ) ) ) )