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