frmx

Description: The X sequence is a nonnegative integer. See rmxnn for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014)

		Ref	Expression
	Assertion	frmx	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$

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		xp1st	$⊢ {(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 1^{st} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℕ_{0}$
3	1 2	syl	$⊢ (a \in ℤ_{\geq 2} \land b \in ℤ) \to 1^{st} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℕ_{0}$
4	3	rgen2	$⊢ \forall a \in ℤ_{\geq 2} \forall b \in ℤ 1^{st} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℕ_{0}$
5		df-rmx	$⊢ X_{rm} = (a \in ℤ_{\geq 2}, b \in ℤ ⟼ 1^{st} ({(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 ℤ 1^{st} ({(c \in (ℕ_{0} \times ℤ) ⟼ 1^{st} (c) + \sqrt{a^{2} - 1} 2^{nd} (c))}^{-1} ({(a + \sqrt{a^{2} - 1})}^{b})) \in ℕ_{0} \leftrightarrow X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$
7	4 6	mpbi	$⊢ X_{rm} : ℤ_{\geq 2} \times ℤ ⟶ ℕ_{0}$

Metamath Proof Explorer