Step 
Hyp 
Ref 
Expression 
0 

crmx 
 rmX 
1 

va 
 a 
2 

cuz 
 ZZ>= 
3 

c2 
 2 
4 
3 2

cfv 
 ( ZZ>= ` 2 ) 
5 

vn 
 n 
6 

cz 
 ZZ 
7 

c1st 
 1st 
8 

vb 
 b 
9 

cn0 
 NN0 
10 
9 6

cxp 
 ( NN0 X. ZZ ) 
11 
8

cv 
 b 
12 
11 7

cfv 
 ( 1st ` b ) 
13 

caddc 
 + 
14 

csqrt 
 sqrt 
15 
1

cv 
 a 
16 

cexp 
 ^ 
17 
15 3 16

co 
 ( a ^ 2 ) 
18 

cmin 
  
19 

c1 
 1 
20 
17 19 18

co 
 ( ( a ^ 2 )  1 ) 
21 
20 14

cfv 
 ( sqrt ` ( ( a ^ 2 )  1 ) ) 
22 

cmul 
 x. 
23 

c2nd 
 2nd 
24 
11 23

cfv 
 ( 2nd ` b ) 
25 
21 24 22

co 
 ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) 
26 
12 25 13

co 
 ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) 
27 
8 10 26

cmpt 
 ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) 
28 
27

ccnv 
 `' ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) 
29 
15 21 13

co 
 ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) 
30 
5

cv 
 n 
31 
29 30 16

co 
 ( ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) ^ n ) 
32 
31 28

cfv 
 ( `' ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) ^ n ) ) 
33 
32 7

cfv 
 ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) ^ n ) ) ) 
34 
1 5 4 6 33

cmpo 
 ( a e. ( ZZ>= ` 2 ) , n e. ZZ > ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) ^ n ) ) ) ) 
35 
0 34

wceq 
 rmX = ( a e. ( ZZ>= ` 2 ) , n e. ZZ > ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) > ( ( 1st ` b ) + ( ( sqrt ` ( ( a ^ 2 )  1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 )  1 ) ) ) ^ n ) ) ) ) 