Theorem frmx

Description: The X sequence is a nonnegative integer. See rmxnn for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014)

	Ref	Expression
Assertion	frmx	|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0

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		xp1st	|- ( ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) e. ( NN0 X. ZZ ) -> ( 1st ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. NN0 )
3	1 2	syl	|- ( ( a e. ( ZZ>= ` 2 ) /\ b e. ZZ ) -> ( 1st ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. NN0 )
4	3	rgen2	|- A. a e. ( ZZ>= ` 2 ) A. b e. ZZ ( 1st ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. NN0
5		df-rmx	|- rmX = ( a e. ( ZZ>= ` 2 ) , b e. ZZ |-> ( 1st ` ( `' ( 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 ( 1st ` ( `' ( c e. ( NN0 X. ZZ ) |-> ( ( 1st ` c ) + ( ( sqrt ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` c ) ) ) ) ` ( ( a + ( sqrt ` ( ( a ^ 2 ) - 1 ) ) ) ^ b ) ) ) e. NN0 <-> rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0 )
7	4 6	mpbi	|- rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0