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 ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )

Proof

Step Hyp Ref Expression
1 rmspecnonsq ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) )
3 pell14qrval ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } )
4 2 3 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } )
5 rabssab ⊢ { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) }
6 simpl ⊢ ( ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
7 6 reximi ⊢ ( ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
8 7 reximi ⊢ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
9 8 ss2abi ⊢ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) }
10 5 9 sstri ⊢ { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) }
11 4 10 eqsstrdi ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
12 simpr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
13 rmspecfund ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
14 13 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
15 14 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) = ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
16 15 oveq1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) )
17 oveq2 ⊢ ( 𝑎 = 𝑁 → ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) )
18 17 rspceeqv ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) )
19 12 16 18 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) )
20 pellfund14b ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) ) )
21 2 20 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) ) )
22 19 21 mpbird ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
23 11 22 sseldd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )