Metamath Proof Explorer

Theorem rmxyelxp

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

Ref Expression
Assertion rmxyelxp ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\in \left({ℕ}_{0}×ℤ\right)$

Proof

Step Hyp Ref Expression
1 rmxypairf1o ${⊢}{A}\in {ℤ}_{\ge 2}\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
2 1 adantr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to \left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
3 rmxyelqirr ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}$
4 f1ocnvdm ${⊢}\left(\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right):{ℕ}_{0}×ℤ\underset{1-1 onto}{⟶}\left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\wedge {\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\in \left\{{a}|\exists {c}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℤ\phantom{\rule{.4em}{0ex}}{a}={c}+\sqrt{{{A}}^{2}-1}{d}\right\}\right)\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\in \left({ℕ}_{0}×ℤ\right)$
5 2 3 4 syl2anc ${⊢}\left({A}\in {ℤ}_{\ge 2}\wedge {N}\in ℤ\right)\to {\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{A}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}\left({\left({A}+\sqrt{{{A}}^{2}-1}\right)}^{{N}}\right)\in \left({ℕ}_{0}×ℤ\right)$