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 41272
Description: Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 41284 and rmxyval 41286 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 41270 . 2 class Xrm
2 va . . 3 setvar ๐‘Ž
3 vn . . 3 setvar ๐‘›
4 c2 12216 . . . 4 class 2
5 cuz 12771 . . . 4 class โ„คโ‰ฅ
64, 5cfv 6500 . . 3 class (โ„คโ‰ฅโ€˜2)
7 cz 12507 . . 3 class โ„ค
82cv 1541 . . . . . . 7 class ๐‘Ž
9 cexp 13976 . . . . . . . . . 10 class โ†‘
108, 4, 9co 7361 . . . . . . . . 9 class (๐‘Žโ†‘2)
11 c1 11060 . . . . . . . . 9 class 1
12 cmin 11393 . . . . . . . . 9 class โˆ’
1310, 11, 12co 7361 . . . . . . . 8 class ((๐‘Žโ†‘2) โˆ’ 1)
14 csqrt 15127 . . . . . . . 8 class โˆš
1513, 14cfv 6500 . . . . . . 7 class (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1))
16 caddc 11062 . . . . . . 7 class +
178, 15, 16co 7361 . . . . . 6 class (๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))
183cv 1541 . . . . . 6 class ๐‘›
1917, 18, 9co 7361 . . . . 5 class ((๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))โ†‘๐‘›)
20 vb . . . . . . 7 setvar ๐‘
21 cn0 12421 . . . . . . . 8 class โ„•0
2221, 7cxp 5635 . . . . . . 7 class (โ„•0 ร— โ„ค)
2320cv 1541 . . . . . . . . 9 class ๐‘
24 c1st 7923 . . . . . . . . 9 class 1st
2523, 24cfv 6500 . . . . . . . 8 class (1st โ€˜๐‘)
26 c2nd 7924 . . . . . . . . . 10 class 2nd
2723, 26cfv 6500 . . . . . . . . 9 class (2nd โ€˜๐‘)
28 cmul 11064 . . . . . . . . 9 class ยท
2915, 27, 28co 7361 . . . . . . . 8 class ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))
3025, 29, 16co 7361 . . . . . . 7 class ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘)))
3120, 22, 30cmpt 5192 . . . . . 6 class (๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))
3231ccnv 5636 . . . . 5 class โ—ก(๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))
3319, 32cfv 6500 . . . 4 class (โ—ก(๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))โ€˜((๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))โ†‘๐‘›))
3433, 24cfv 6500 . . 3 class (1st โ€˜(โ—ก(๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))โ€˜((๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))โ†‘๐‘›)))
352, 3, 6, 7, 34cmpo 7363 . 2 class (๐‘Ž โˆˆ (โ„คโ‰ฅโ€˜2), ๐‘› โˆˆ โ„ค โ†ฆ (1st โ€˜(โ—ก(๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))โ€˜((๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))โ†‘๐‘›))))
361, 35wceq 1542 1 wff Xrm = (๐‘Ž โˆˆ (โ„คโ‰ฅโ€˜2), ๐‘› โˆˆ โ„ค โ†ฆ (1st โ€˜(โ—ก(๐‘ โˆˆ (โ„•0 ร— โ„ค) โ†ฆ ((1st โ€˜๐‘) + ((โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)) ยท (2nd โ€˜๐‘))))โ€˜((๐‘Ž + (โˆšโ€˜((๐‘Žโ†‘2) โˆ’ 1)))โ†‘๐‘›))))
Colors of variables: wff setvar class
This definition is referenced by:  rmxfval  41274  frmx  41284
  Copyright terms: Public domain W3C validator