Metamath Proof Explorer

Theorem rmxynorm

Description: The X and Y sequences define a solution to the corresponding Pell equation. (Contributed by Stefan O'Rear, 22-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. ZZ )
2 eqidd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A rmX N ) = ( A rmX N ) )
3 eqidd 
 |-  ( N e. ZZ -> ( A rmY N ) = ( A rmY N ) )
4 2 3 anim12i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A rmX N ) = ( A rmX N ) /\ ( A rmY N ) = ( A rmY N ) ) )
5 oveq2 
 |-  ( a = N -> ( A rmX a ) = ( A rmX N ) )
6 5 eqeq2d 
 |-  ( a = N -> ( ( A rmX N ) = ( A rmX a ) <-> ( A rmX N ) = ( A rmX N ) ) )
7 oveq2 
 |-  ( a = N -> ( A rmY a ) = ( A rmY N ) )
8 7 eqeq2d 
 |-  ( a = N -> ( ( A rmY N ) = ( A rmY a ) <-> ( A rmY N ) = ( A rmY N ) ) )
9 6 8 anbi12d 
 |-  ( a = N -> ( ( ( A rmX N ) = ( A rmX a ) /\ ( A rmY N ) = ( A rmY a ) ) <-> ( ( A rmX N ) = ( A rmX N ) /\ ( A rmY N ) = ( A rmY N ) ) ) )
10 9 rspcev 
 |-  ( ( N e. ZZ /\ ( ( A rmX N ) = ( A rmX N ) /\ ( A rmY N ) = ( A rmY N ) ) ) -> E. a e. ZZ ( ( A rmX N ) = ( A rmX a ) /\ ( A rmY N ) = ( A rmY a ) ) )
11 1 4 10 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> E. a e. ZZ ( ( A rmX N ) = ( A rmX a ) /\ ( A rmY N ) = ( A rmY a ) ) )
12 simpl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A e. ( ZZ>= ` 2 ) )
13 frmx 
 |-  rmX : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
14 13 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmX N ) e. NN0 )
15 frmy 
 |-  rmY : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
16 15 fovcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A rmY N ) e. ZZ )
17 rmxycomplete 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ ( A rmX N ) e. NN0 /\ ( A rmY N ) e. ZZ ) -> ( ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 <-> E. a e. ZZ ( ( A rmX N ) = ( A rmX a ) /\ ( A rmY N ) = ( A rmY a ) ) ) )
18 12 14 16 17 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 <-> E. a e. ZZ ( ( A rmX N ) = ( A rmX a ) /\ ( A rmY N ) = ( A rmY a ) ) ) )
19 11 18 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A rmX N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A rmY N ) ^ 2 ) ) ) = 1 )