Step 
Hyp 
Ref 
Expression 
1 

oveq1 
⊢ ( 𝑎 = 𝐴 → ( 𝑎 ↑ 2 ) = ( 𝐴 ↑ 2 ) ) 
2 
1

fvoveq1d 
⊢ ( 𝑎 = 𝐴 → ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) = ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) 
3 
2

oveq1d 
⊢ ( 𝑎 = 𝐴 → ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) = ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) 
4 
3

oveq2d 
⊢ ( 𝑎 = 𝐴 → ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) = ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) 
5 
4

mpteq2dv 
⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) = ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ) 
6 
5

cnveqd 
⊢ ( 𝑎 = 𝐴 → ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) = ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ) 
7 
6

adantr 
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) = ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ) 
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} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) = ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) 
13 
12

fveq2d 
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑛 = 𝑁 ) → ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) = ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) 
14 

dfrmy 
⊢ Y_{rm} = ( 𝑎 ∈ ( ℤ_{≥} ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) ) 
15 

fvex 
⊢ ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ∈ V 
16 
13 14 15

ovmpoa 
⊢ ( ( 𝐴 ∈ ( ℤ_{≥} ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 Y_{rm} 𝑁 ) = ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ) ) ) 