Metamath Proof Explorer

Theorem rmxy0

Description: Value of the X and Y sequences at 0. (Contributed by Stefan O'Rear, 22-Sep-2014)

Ref Expression
Assertion rmxy0 
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) )
3 1 2 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) )
4 rmbaserp 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )
5 4 rpcnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) e. CC )
6 5 exp0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 0 ) = 1 )
7 rmspecpos 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
8 7 rpcnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. CC )
9 8 sqrtcld 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. CC )
10 9 mul01d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) = 0 )
11 10 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) = ( 1 + 0 ) )
12 1p0e1 
 |-  ( 1 + 0 ) = 1
13 11 12 eqtr2di 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) )
14 3 6 13 3eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) )
15 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
16 nn0ssq 
 |-  NN0 C_ QQ
17 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
18 17 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( A rmX 0 ) e. NN0 )
19 1 18 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) e. NN0 )
20 16 19 sseldi 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 0 ) e. QQ )
21 zssq 
 |-  ZZ C_ QQ
22 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
23 22 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 0 e. ZZ ) -> ( A rmY 0 ) e. ZZ )
24 1 23 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) e. ZZ )
25 21 24 sseldi 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 0 ) e. QQ )
26 1z 
 |-  1 e. ZZ
27 21 26 sselii 
 |-  1 e. QQ
28 27 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. QQ )
29 21 1 sselii 
 |-  0 e. QQ
30 29 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 0 e. QQ )
31 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX 0 ) e. QQ /\ ( A rmY 0 ) e. QQ ) /\ ( 1 e. QQ /\ 0 e. QQ ) ) -> ( ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) <-> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) ) )
32 15 20 25 28 30 31 syl122anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A rmX 0 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 0 ) ) ) = ( 1 + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 0 ) ) <-> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) ) )
33 14 32 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 0 ) = 1 /\ ( A rmY 0 ) = 0 ) )