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	$⊢ (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		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$
6	5	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$
7	6	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$
8	7	rgenw	$⊢ \forall 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) \to \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d)$
9	8	a1i	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \forall 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) \to \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d)$
10		ss2rab	$⊢ \{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 \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \leftrightarrow \forall 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) \to \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d)$
11	9 10	sylibr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \{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 \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
12		ssv	$⊢ ℝ \subseteq V$
13		rabss2	$⊢ ℝ \subseteq V \to \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \subseteq \{a \in V \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
14	12 13	ax-mp	$⊢ \{a \in ℝ \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \subseteq \{a \in V \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
15	11 14	sstrdi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \{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 \in V \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
16		rabab	$⊢ \{a \in V \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} = \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
17	15 16	sseqtrdi	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \{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\}$
18	4 17	eqsstrd	$⊢ (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\}$
19		simpr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to N \in ℤ$
20		rmspecfund	$⊢ A \in ℤ_{\geq 2} \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
21	20	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to PellFund (A^{2} - 1) = A + \sqrt{A^{2} - 1}$
22	21	eqcomd	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to A + \sqrt{A^{2} - 1} = PellFund (A^{2} - 1)$
23	22	oveq1d	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{N}$
24		oveq2	$⊢ a = N \to {PellFund (A^{2} - 1)}^{a} = {PellFund (A^{2} - 1)}^{N}$
25	24	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}$
26	19 23 25	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to \exists a \in ℤ {(A + \sqrt{A^{2} - 1})}^{N} = {PellFund (A^{2} - 1)}^{a}$
27		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})$
28	2 27	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})$
29	26 28	mpbird	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(A + \sqrt{A^{2} - 1})}^{N} \in Pell14QR (A^{2} - 1)$
30	18 29	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 rmxyelqirrOLD

Proof