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

Definition df-rmx 29152
 Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 29163 and rmxyval 29165 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
Assertion
Ref Expression
df-rmx Xrm
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-rmx
StepHypRef Expression
1 crmx 29150 . 2 Xrm
2 va . . 3
3 vn . . 3
4 c2 10367 . . . 4
5 cuz 10857 . . . 4
64, 5cfv 5415 . . 3
7 cz 10642 . . 3
82cv 1363 . . . . . . 7
9 cexp 11861 . . . . . . . . . 10
108, 4, 9co 6090 . . . . . . . . 9
11 c1 9279 . . . . . . . . 9
12 cmin 9591 . . . . . . . . 9
1310, 11, 12co 6090 . . . . . . . 8
14 csqr 12718 . . . . . . . 8
1513, 14cfv 5415 . . . . . . 7
16 caddc 9281 . . . . . . 7
178, 15, 16co 6090 . . . . . 6
183cv 1363 . . . . . 6
1917, 18, 9co 6090 . . . . 5
20 vb . . . . . . 7
21 cn0 10575 . . . . . . . 8
2221, 7cxp 4834 . . . . . . 7
2320cv 1363 . . . . . . . . 9
24 c1st 6574 . . . . . . . . 9
2523, 24cfv 5415 . . . . . . . 8
26 c2nd 6575 . . . . . . . . . 10
2723, 26cfv 5415 . . . . . . . . 9
28 cmul 9283 . . . . . . . . 9
2915, 27, 28co 6090 . . . . . . . 8
3025, 29, 16co 6090 . . . . . . 7
3120, 22, 30cmpt 4347 . . . . . 6
3231ccnv 4835 . . . . 5
3319, 32cfv 5415 . . . 4
3433, 24cfv 5415 . . 3
352, 3, 6, 7, 34cmpt2 6092 . 2
361, 35wceq 1364 1 Xrm
 Colors of variables: wff setvar class This definition is referenced by:  rmxfval  29154  frmx  29163
 Copyright terms: Public domain W3C validator