Metamath Proof Explorer

Theorem frmy

Description: The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion frmy 
|- rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ

Proof

Step Hyp Ref Expression
1 rmxyelxp 
 |-  ( ( a e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) e. ( NN0 X. ZZ ) )
2 xp2nd 
 |-  ( ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) e. ( NN0 X. ZZ ) -> ( 2nd ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. ZZ )
3 1 2 syl 
 |-  ( ( a e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( 2nd ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. ZZ )
4 3 rgen2 
 |-  A. a e. ( ZZ>= ` 2 ) A. b e. ZZ ( 2nd ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. ZZ
5 df-rmy 
 |-  rmY = ( a e. ( ZZ>= ` 2 ) , b e. ZZ |-> ( 2nd ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) )
6 5 fmpo 
 |-  ( A. a e. ( ZZ>= ` 2 ) A. b e. ZZ ( 2nd ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. ZZ <-> rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ )
7 4 6 mpbi 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ