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 ) ) } )