Step 
Hyp 
Ref 
Expression 
0 

crmy 
⊢ Y_{rm} 
1 

va 
⊢ 𝑎 
2 

cuz 
⊢ ℤ_{≥} 
3 

c2 
⊢ 2 
4 
3 2

cfv 
⊢ ( ℤ_{≥} ‘ 2 ) 
5 

vn 
⊢ 𝑛 
6 

cz 
⊢ ℤ 
7 

c2nd 
⊢ 2^{nd} 
8 

vb 
⊢ 𝑏 
9 

cn0 
⊢ ℕ_{0} 
10 
9 6

cxp 
⊢ ( ℕ_{0} × ℤ ) 
11 

c1st 
⊢ 1^{st} 
12 
8

cv 
⊢ 𝑏 
13 
12 11

cfv 
⊢ ( 1^{st} ‘ 𝑏 ) 
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 
⊢ ( 2^{nd} ‘ 𝑏 ) 
25 
22 24 23

co 
⊢ ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) 
26 
13 25 14

co 
⊢ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) 
27 
8 10 26

cmpt 
⊢ ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) 
28 
27

ccnv 
⊢ ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) 
29 
16 22 14

co 
⊢ ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) 
30 
5

cv 
⊢ 𝑛 
31 
29 30 17

co 
⊢ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) 
32 
31 28

cfv 
⊢ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) 
33 
32 7

cfv 
⊢ ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) 
34 
1 5 4 6 33

cmpo 
⊢ ( 𝑎 ∈ ( ℤ_{≥} ‘ 2 ) , 𝑛 ∈ ℤ ↦ ( 2^{nd} ‘ ( ^{◡} ( 𝑏 ∈ ( ℕ_{0} × ℤ ) ↦ ( ( 1^{st} ‘ 𝑏 ) + ( ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) · ( 2^{nd} ‘ 𝑏 ) ) ) ) ‘ ( ( 𝑎 + ( √ ‘ ( ( 𝑎 ↑ 2 ) − 1 ) ) ) ↑ 𝑛 ) ) ) ) 
35 
0 34

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