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) (Proof shortened by SN, 23-Dec-2024)

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 rabssab 
 |-  { 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 ) ) /\ ( ( c ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( d ^ 2 ) ) ) = 1 ) }
6 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 ) ) )
7 6 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 ) ) )
8 7 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 ) ) )
9 8 ss2abi 
 |-  { a | 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 ) ) }
10 5 9 sstri 
 |-  { 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 ) ) }
11 4 10 eqsstrdi 
 |-  ( ( 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 ) ) } )
12 simpr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> N e. ZZ )
13 rmspecfund 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
14 13 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) )
15 14 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) = ( PellFund ` ( ( A ^ 2 ) - 1 ) ) )
16 15 oveq1d 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ N ) )
17 oveq2 
 |-  ( a = N -> ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ N ) )
18 17 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 ) )
19 12 16 18 syl2anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> E. a e. ZZ ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) = ( ( PellFund ` ( ( A ^ 2 ) - 1 ) ) ^ a ) )
20 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 ) ) )
21 2 20 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 ) ) )
22 19 21 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqrt ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. ( Pell14QR ` ( ( A ^ 2 ) - 1 ) ) )
23 11 22 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 ) ) } )