# 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 ) )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( 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 ) ) } )`