rmxyelxp

Description: Lemma for frmx and frmy . (Contributed by Stefan O'Rear, 22-Sep-2014)

		Ref	Expression
	Assertion	rmxyelxp	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \in (ℕ_{0} \times ℤ)$

Step	Hyp	Ref	Expression
1		rmxypairf1o	$⊢ A \in ℤ_{\geq 2} \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
2	1	adantr	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to (b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}$
3		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\}$
4		f1ocnvdm	$⊢ ((b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b)) : ℕ_{0} \times ℤ \underset{1-1 onto}{⟶} \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\} \land {(A + \sqrt{A^{2} - 1})}^{N} \in \{a \| \exists c \in ℕ_{0} \exists d \in ℤ a = c + \sqrt{A^{2} - 1} d\}) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \in (ℕ_{0} \times ℤ)$
5	2 3 4	syl2anc	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ) \to {(b \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (b) + \sqrt{A^{2} - 1} 2^{nd} (b))}^{-1} ({(A + \sqrt{A^{2} - 1})}^{N}) \in (ℕ_{0} \times ℤ)$

Metamath Proof Explorer