# Metamath Proof Explorer

## Definition df-rmx

Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx and rmxyval for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion df-rmx ${⊢}{X}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{1}^{st}\left({\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)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 crmx ${class}{X}_{\mathrm{rm}}$
1 va ${setvar}{a}$
2 cuz ${class}{ℤ}_{\ge }$
3 c2 ${class}2$
4 3 2 cfv ${class}{ℤ}_{\ge 2}$
5 vn ${setvar}{n}$
6 cz ${class}ℤ$
7 c1st ${class}{1}^{st}$
8 vb ${setvar}{b}$
9 cn0 ${class}{ℕ}_{0}$
10 9 6 cxp ${class}\left({ℕ}_{0}×ℤ\right)$
11 8 cv ${setvar}{b}$
12 11 7 cfv ${class}{1}^{st}\left({b}\right)$
13 caddc ${class}+$
14 csqrt ${class}\surd$
15 1 cv ${setvar}{a}$
16 cexp ${class}^$
17 15 3 16 co ${class}{{a}}^{2}$
18 cmin ${class}-$
19 c1 ${class}1$
20 17 19 18 co ${class}\left({{a}}^{2}-1\right)$
21 20 14 cfv ${class}\sqrt{{{a}}^{2}-1}$
22 cmul ${class}×$
23 c2nd ${class}{2}^{nd}$
24 11 23 cfv ${class}{2}^{nd}\left({b}\right)$
25 21 24 22 co ${class}\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)$
26 12 25 13 co ${class}\left({1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)$
27 8 10 26 cmpt ${class}\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)$
28 27 ccnv ${class}{\left({b}\in \left({ℕ}_{0}×ℤ\right)⟼{1}^{st}\left({b}\right)+\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)\right)}^{-1}$
29 15 21 13 co ${class}\left({a}+\sqrt{{{a}}^{2}-1}\right)$
30 5 cv ${setvar}{n}$
31 29 30 16 co ${class}{\left({a}+\sqrt{{{a}}^{2}-1}\right)}^{{n}}$
32 31 28 cfv ${class}{\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)$
33 32 7 cfv ${class}{1}^{st}\left({\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)\right)$
34 1 5 4 6 33 cmpo ${class}\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{1}^{st}\left({\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)\right)\right)$
35 0 34 wceq ${wff}{X}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{1}^{st}\left({\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)\right)\right)$