Metamath Proof Explorer

Theorem rmxyelqirrOLD

Description: Obsolete version of rmxyelqirr as of 23-Dec-2024. (Contributed by Stefan O'Rear, 21-Sep-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion rmxyelqirrOLD ( ( 𝐴 ∈ ( ℤ≥ ‘ 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 simpl ⊢ ( ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
6 5 reximi ⊢ ( ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
7 6 reximi ⊢ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
8 7 rgenw ⊢ ∀ 𝑎 ∈ ℝ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) )
9 8 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ∀ 𝑎 ∈ ℝ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ) )
10 ss2rab ⊢ ( { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ↔ ∀ 𝑎 ∈ ℝ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) → ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ) )
11 9 10 sylibr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
12 ssv ⊢ ℝ ⊆ V
13 rabss2 ⊢ ( ℝ ⊆ V → { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ⊆ { 𝑎 ∈ V ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
14 12 13 ax-mp ⊢ { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } ⊆ { 𝑎 ∈ V ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) }
15 11 14 sstrdi ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∈ V ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
16 rabab ⊢ { 𝑎 ∈ V ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } = { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) }
17 15 16 sseqtrdi ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → { 𝑎 ∈ ℝ ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ ( 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) ∧ ( ( 𝑐 ↑ 2 ) − ( ( ( 𝐴 ↑ 2 ) − 1 ) · ( 𝑑 ↑ 2 ) ) ) = 1 ) } ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
18 4 17 eqsstrd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ⊆ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )
19 simpr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
20 rmspecfund ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) = ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) )
22 21 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) = ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
23 22 oveq1d ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) )
24 oveq2 ⊢ ( 𝑎 = 𝑁 → ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) )
25 24 rspceeqv ⊢ ( ( 𝑁 ∈ ℤ ∧ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑁 ) ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) )
26 19 23 25 syl2anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) )
27 pellfund14b ⊢ ( ( ( 𝐴 ↑ 2 ) − 1 ) ∈ ( ℕ ∖ ◻NN ) → ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) ) )
28 2 27 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↔ ∃ 𝑎 ∈ ℤ ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) = ( ( PellFund ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ↑ 𝑎 ) ) )
29 26 28 mpbird ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ ( Pell14QR ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) )
30 18 29 sseldd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐴 + ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) ) ↑ 𝑁 ) ∈ { 𝑎 ∣ ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℤ 𝑎 = ( 𝑐 + ( ( √ ‘ ( ( 𝐴 ↑ 2 ) − 1 ) ) · 𝑑 ) ) } )