Metamath Proof Explorer

Definition df-rmy

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

Ref Expression
Assertion df-rmy ${⊢}{Y}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{2}^{nd}\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 crmy ${class}{Y}_{\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 c2nd ${class}{2}^{nd}$
8 vb ${setvar}{b}$
9 cn0 ${class}{ℕ}_{0}$
10 9 6 cxp ${class}\left({ℕ}_{0}×ℤ\right)$
11 c1st ${class}{1}^{st}$
12 8 cv ${setvar}{b}$
13 12 11 cfv ${class}{1}^{st}\left({b}\right)$
14 caddc ${class}+$
15 csqrt ${class}\surd$
16 1 cv ${setvar}{a}$
17 cexp ${class}^$
18 16 3 17 co ${class}{{a}}^{2}$
19 cmin ${class}-$
20 c1 ${class}1$
21 18 20 19 co ${class}\left({{a}}^{2}-1\right)$
22 21 15 cfv ${class}\sqrt{{{a}}^{2}-1}$
23 cmul ${class}×$
24 12 7 cfv ${class}{2}^{nd}\left({b}\right)$
25 22 24 23 co ${class}\sqrt{{{a}}^{2}-1}{2}^{nd}\left({b}\right)$
26 13 25 14 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 16 22 14 co ${class}\left({a}+\sqrt{{{a}}^{2}-1}\right)$
30 5 cv ${setvar}{n}$
31 29 30 17 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}{2}^{nd}\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 ℤ⟼{2}^{nd}\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}{Y}_{\mathrm{rm}}=\left({a}\in {ℤ}_{\ge 2},{n}\in ℤ⟼{2}^{nd}\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)$