Metamath Proof Explorer

Theorem rmxyelqirr

Description: The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion rmxyelqirr 
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )

Proof

Step Hyp Ref Expression
1 rmspecnonsq 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
2 1 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) )
3 pell14qrval 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) = { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } )
4 2 3 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) = { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } )
5 simpl 
 |-  ( ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )
6 5 reximi 
 |-  ( E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )
7 6 reximi 
 |-  ( E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )
8 7 rgenw 
 |-  A. a e. RR ( E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) )
9 8 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> A. a e. RR ( E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) ) )
10 ss2rab 
 |-  ( { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } C_ { a e. RR | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } <-> A. a e. RR ( E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) -> E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) ) )
11 9 10 sylibr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } C_ { a e. RR | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
12 ssv 
 |-  RR C_ _V
13 rabss2 
 |-  ( RR C_ _V -> { a e. RR | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } C_ { a e. _V | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
14 12 13 ax-mp 
 |-  { a e. RR | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } C_ { a e. _V | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) }
15 11 14 sstrdi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } C_ { a e. _V | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
16 rabab 
 |-  { a e. _V | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } = { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) }
17 15 16 sseqtrdi 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> { a e. RR | E. c e. NN0 E. d e. ZZ ( a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) } C_ { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
18 4 17 eqsstrd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) C_ { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
19 simpr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. ZZ )
20 rmspecfund 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
21 20 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
22 21 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( PellFund ` ( ( A ^ 2 ) - 1 ) ) )
23 22 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ N ) )
24 oveq2 
 |-  ( a = N -> ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ N ) )
25 24 rspceeqv 
 |-  ( ( N e. ZZ /\ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ N ) ) -> E. a e. ZZ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) )
26 19 23 25 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> E. a e. ZZ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) )
27 pellfund14b 
 |-  ( ( ( A ^ 2 ) - 1 ) e. ( NN \ []NN ) -> ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> E. a e. ZZ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) ) )
28 2 27 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) <-> E. a e. ZZ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) ) )
29 26 28 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
30 18 29 sseldd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqrt ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )