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 \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$

Proof

Step	Hyp	Ref	Expression
1		rmspecnonsq	$⊢ A \in ℤ_{\geq 2} \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
2	1	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A^{2} - 1 \in (ℕ ∖ ◻_{ℕ})$
3		pell14qrval	$⊢ A^{2} - 1 \in (ℕ ∖ ◻_{ℕ}) \to Pell14QR (A^{2} - 1) = \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\}$
4	2 3	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to Pell14QR (A^{2} - 1) = \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\}$
5		rabssab	$⊢ \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\} \subseteq \{a \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\}$
6		simpl	$⊢ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1) \to a = c + \sqrt{A^{2} - 1} d$
7	6	reximi	$⊢ \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1) \to \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d$
8	7	reximi	$⊢ \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1) \to \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d$
9	8	ss2abi	$⊢ \{a \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\} \subseteq \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
10	5 9	sstri	$⊢ \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ (a = c + \sqrt{A^{2} - 1} d \land c^{2} - (A^{2} - 1) d^{2} = 1)\} \subseteq \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
11	4 10	eqsstrdi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to Pell14QR (A^{2} - 1) \subseteq \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
12		simpr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℤ$
13		rmspecfund	$⊢ A \in ℤ_{\geq 2} \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
14	13	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
15	14	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A + \sqrt{A^{2} - 1} = PellFund (A^{2} - 1)$
16	15	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{N}$
17		oveq2	$⊢ a = N \to {PellFund (A^{2} - 1)}^{a} = {PellFund (A^{2} - 1)}^{N}$
18	17	rspceeqv	$⊢ (N \in ℤ \land {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{N}) \to \exists a \in ℤ {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{a}$
19	12 16 18	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \exists a \in ℤ {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{a}$
20		pellfund14b	$⊢ A^{2} - 1 \in (ℕ ∖ ◻_{ℕ}) \to ({(A + \sqrt{A^{2} - 1})}^{N} \in Pell14QR (A^{2} - 1) \leftrightarrow \exists a \in ℤ {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{a})$
21	2 20	syl	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to ({(A + \sqrt{A^{2} - 1})}^{N} \in Pell14QR (A^{2} - 1) \leftrightarrow \exists a \in ℤ {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{a})$
22	19 21	mpbird	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in Pell14QR (A^{2} - 1)$
23	11 22	sseldd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$

Metamath Proof Explorer

Theorem rmxyelqirr

Proof