# Metamath Proof Explorer

## Theorem 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}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$

### Proof

Step Hyp Ref Expression
1 rmxyelxp ${⊢}\left({a}\in {ℤ}_{\ge 2}\wedge {b}\in ℤ\right)\to {\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\in \left({ℕ}_{0}×ℤ\right)$
2 xp1st ${⊢}{\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\in \left({ℕ}_{0}×ℤ\right)\to {1}^{st}\left({\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\right)\in {ℕ}_{0}$
3 1 2 syl ${⊢}\left({a}\in {ℤ}_{\ge 2}\wedge {b}\in ℤ\right)\to {1}^{st}\left({\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\right)\in {ℕ}_{0}$
4 3 rgen2 ${⊢}\forall {a}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\forall {b}\in ℤ\phantom{\rule{.4em}{0ex}}{1}^{st}\left({\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\right)\in {ℕ}_{0}$
5 df-rmx ${⊢}{X}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{b}\in ℤ⟼{1}^{st}\left({\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\right)\right)$
6 5 fmpo ${⊢}\forall {a}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\forall {b}\in ℤ\phantom{\rule{.4em}{0ex}}{1}^{st}\left({\left({c}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({c}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({c}\right)\right)}^{-1}\left({\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{b}}\right)\right)\in {ℕ}_{0}↔{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$
7 4 6 mpbi ${⊢}{X}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶{ℕ}_{0}$