# Metamath Proof Explorer

## Theorem frmy

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

Ref Expression
Assertion frmy ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$

### 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 xp2nd ${⊢}{\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 {2}^{nd}\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 ℤ$
3 1 2 syl ${⊢}\left({a}\in {ℤ}_{\ge 2}\wedge {b}\in ℤ\right)\to {2}^{nd}\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 ℤ$
4 3 rgen2 ${⊢}\forall {a}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\forall {b}\in ℤ\phantom{\rule{.4em}{0ex}}{2}^{nd}\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 ℤ$
5 df-rmy ${⊢}{Y}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{b}\in ℤ⟼{2}^{nd}\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}}{2}^{nd}\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 ℤ↔{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$
7 4 6 mpbi ${⊢}{Y}_{\mathrm{rm}}:{ℤ}_{\ge 2}×ℤ⟶ℤ$