Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rmx Structured version   Visualization version   GIF version

Definition df-rmx 37968
Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 37980 and rmxyval 37982 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
Assertion
Ref Expression
df-rmx Xrm = (𝑎 ∈ (ℤ‘2), 𝑛 ∈ ℤ ↦ (1st ‘((𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))
Distinct variable group:   𝑛,𝑎,𝑏

Detailed syntax breakdown of Definition df-rmx
StepHypRef Expression
1 crmx 37966 . 2 class Xrm
2 va . . 3 setvar 𝑎
3 vn . . 3 setvar 𝑛
4 c2 11262 . . . 4 class 2
5 cuz 11879 . . . 4 class
64, 5cfv 6049 . . 3 class (ℤ‘2)
7 cz 11569 . . 3 class
82cv 1631 . . . . . . 7 class 𝑎
9 cexp 13054 . . . . . . . . . 10 class
108, 4, 9co 6813 . . . . . . . . 9 class (𝑎↑2)
11 c1 10129 . . . . . . . . 9 class 1
12 cmin 10458 . . . . . . . . 9 class
1310, 11, 12co 6813 . . . . . . . 8 class ((𝑎↑2) − 1)
14 csqrt 14172 . . . . . . . 8 class
1513, 14cfv 6049 . . . . . . 7 class (√‘((𝑎↑2) − 1))
16 caddc 10131 . . . . . . 7 class +
178, 15, 16co 6813 . . . . . 6 class (𝑎 + (√‘((𝑎↑2) − 1)))
183cv 1631 . . . . . 6 class 𝑛
1917, 18, 9co 6813 . . . . 5 class ((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)
20 vb . . . . . . 7 setvar 𝑏
21 cn0 11484 . . . . . . . 8 class 0
2221, 7cxp 5264 . . . . . . 7 class (ℕ0 × ℤ)
2320cv 1631 . . . . . . . . 9 class 𝑏
24 c1st 7331 . . . . . . . . 9 class 1st
2523, 24cfv 6049 . . . . . . . 8 class (1st𝑏)
26 c2nd 7332 . . . . . . . . . 10 class 2nd
2723, 26cfv 6049 . . . . . . . . 9 class (2nd𝑏)
28 cmul 10133 . . . . . . . . 9 class ·
2915, 27, 28co 6813 . . . . . . . 8 class ((√‘((𝑎↑2) − 1)) · (2nd𝑏))
3025, 29, 16co 6813 . . . . . . 7 class ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏)))
3120, 22, 30cmpt 4881 . . . . . 6 class (𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))
3231ccnv 5265 . . . . 5 class (𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))
3319, 32cfv 6049 . . . 4 class ((𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))
3433, 24cfv 6049 . . 3 class (1st ‘((𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))
352, 3, 6, 7, 34cmpt2 6815 . 2 class (𝑎 ∈ (ℤ‘2), 𝑛 ∈ ℤ ↦ (1st ‘((𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))
361, 35wceq 1632 1 wff Xrm = (𝑎 ∈ (ℤ‘2), 𝑛 ∈ ℤ ↦ (1st ‘((𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛))))
Colors of variables: wff setvar class
This definition is referenced by:  rmxfval  37970  frmx  37980
  Copyright terms: Public domain W3C validator