# Metamath Proof Explorer

## Theorem rmyfval

Description: Value of the Y sequence. Not used after rmxyval is proved. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmyfval ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) = ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )

### Proof

Step Hyp Ref Expression
1 oveq1 ( 𝑎 = 𝐴 → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
2 1 fvoveq1d ( 𝑎 = 𝐴 → ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
3 2 oveq1d ( 𝑎 = 𝐴 → ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) )
4 3 oveq2d ( 𝑎 = 𝐴 → ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) = ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) )
5 4 mpteq2dv ( 𝑎 = 𝐴 → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) )
6 5 cnveqd ( 𝑎 = 𝐴 ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) )
7 6 adantr ( ( 𝑎 = 𝐴𝑛 = 𝑁 ) → ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) )
8 id ( 𝑎 = 𝐴𝑎 = 𝐴 )
9 8 2 oveq12d ( 𝑎 = 𝐴 → ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
10 id ( 𝑛 = 𝑁𝑛 = 𝑁 )
11 9 10 oveqan12d ( ( 𝑎 = 𝐴𝑛 = 𝑁 ) → ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) = ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) )
12 7 11 fveq12d ( ( 𝑎 = 𝐴𝑛 = 𝑁 ) → ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) = ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) )
13 12 fveq2d ( ( 𝑎 = 𝐴𝑛 = 𝑁 ) → ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) = ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )
14 df-rmy Yrm = ( 𝑎 ∈ ( ℤ ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) )
15 fvex ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ∈ V
16 13 14 15 ovmpoa ( ( 𝐴 ∈ ( ℤ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Yrm 𝑁 ) = ( 2nd ‘ ( ( 𝑏 ∈ ( ℕ0 × ℤ ) ↦ ( ( 1st𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2nd𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) )