Metamath Proof Explorer

Theorem rmxy1

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

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

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 rmxyval 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) )
3 1 2 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) )
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 exp1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ 1 ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 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 mulid1d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) = ( sqrt ` ( ( A ^ 2 ) - 1 ) ) )
11 10 eqcomd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) = ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) )
12 11 oveq2d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) )
13 3 6 12 3eqtrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) )
14 rmspecsqrtnq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
15 nn0ssq 
 |-  NN0 C_ QQ
16 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
17 16 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmX 1 ) e. NN0 )
18 1 17 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) e. NN0 )
19 15 18 sseldi 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX 1 ) e. QQ )
20 zssq 
 |-  ZZ C_ QQ
21 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
22 21 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ 1 e. ZZ ) -> ( A rmY 1 ) e. ZZ )
23 1 22 mpan2 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) e. ZZ )
24 20 23 sseldi 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmY 1 ) e. QQ )
25 eluzelz 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. ZZ )
26 zq 
 |-  ( A e. ZZ -> A e. QQ )
27 25 26 syl 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. QQ )
28 20 1 sselii 
 |-  1 e. QQ
29 28 a1i 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 e. QQ )
30 qirropth 
 |-  ( ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) /\ ( ( A rmX 1 ) e. QQ /\ ( A rmY 1 ) e. QQ ) /\ ( A e. QQ /\ 1 e. QQ ) ) -> ( ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) <-> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) ) )
31 14 19 24 27 29 30 syl122anc 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( ( A rmX 1 ) + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. ( A rmY 1 ) ) ) = ( A + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. 1 ) ) <-> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) ) )
32 13 31 mpbid 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A rmX 1 ) = A /\ ( A rmY 1 ) = 1 ) )