frmy

Description: The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014)

		Ref	Expression
	Assertion	frmy	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$

Step	Hyp	Ref	Expression
1		rmxyelxp	$⊢ (a \in ℤ_{\geq 2} \land b \in ℤ) \to {(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b}) \in (ℕ_{0} \times ℤ)$
2		xp2nd	$⊢ {(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b}) \in (ℕ_{0} \times ℤ) \to 2^{nd} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℤ$
3	1 2	syl	$⊢ (a \in ℤ_{\geq 2} \land b \in ℤ) \to 2^{nd} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℤ$
4	3	rgen2	$⊢ \forall a \in ℤ_{\geq 2} \forall b \in ℤ 2^{nd} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℤ$
5		df-rmy	$⊢ Y_{rm} = (a \in ℤ_{\geq 2}, b \in ℤ ⟼ 2^{nd} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})))$
6	5	fmpo	$⊢ \forall a \in ℤ_{\geq 2} \forall b \in ℤ 2^{nd} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℤ \leftrightarrow Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$
7	4 6	mpbi	$⊢ Y_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℤ$

Metamath Proof Explorer