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

Definition df-pell1qr 41256
Description: Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014.)
Assertion
Ref Expression
df-pell1qr Pell1QR = (๐‘ฅ โˆˆ (โ„• โˆ– โ—ปNN) โ†ฆ {๐‘ฆ โˆˆ โ„ โˆฃ โˆƒ๐‘ง โˆˆ โ„•0 โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)})
Distinct variable group:   ๐‘ฅ,๐‘ฆ,๐‘ง,๐‘ค

Detailed syntax breakdown of Definition df-pell1qr
StepHypRef Expression
1 cpell1qr 41251 . 2 class Pell1QR
2 vx . . 3 setvar ๐‘ฅ
3 cn 12177 . . . 4 class โ„•
4 csquarenn 41250 . . . 4 class โ—ปNN
53, 4cdif 3925 . . 3 class (โ„• โˆ– โ—ปNN)
6 vy . . . . . . . . 9 setvar ๐‘ฆ
76cv 1540 . . . . . . . 8 class ๐‘ฆ
8 vz . . . . . . . . . 10 setvar ๐‘ง
98cv 1540 . . . . . . . . 9 class ๐‘ง
102cv 1540 . . . . . . . . . . 11 class ๐‘ฅ
11 csqrt 15145 . . . . . . . . . . 11 class โˆš
1210, 11cfv 6516 . . . . . . . . . 10 class (โˆšโ€˜๐‘ฅ)
13 vw . . . . . . . . . . 11 setvar ๐‘ค
1413cv 1540 . . . . . . . . . 10 class ๐‘ค
15 cmul 11080 . . . . . . . . . 10 class ยท
1612, 14, 15co 7377 . . . . . . . . 9 class ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)
17 caddc 11078 . . . . . . . . 9 class +
189, 16, 17co 7377 . . . . . . . 8 class (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค))
197, 18wceq 1541 . . . . . . 7 wff ๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค))
20 c2 12232 . . . . . . . . . 10 class 2
21 cexp 13992 . . . . . . . . . 10 class โ†‘
229, 20, 21co 7377 . . . . . . . . 9 class (๐‘งโ†‘2)
2314, 20, 21co 7377 . . . . . . . . . 10 class (๐‘คโ†‘2)
2410, 23, 15co 7377 . . . . . . . . 9 class (๐‘ฅ ยท (๐‘คโ†‘2))
25 cmin 11409 . . . . . . . . 9 class โˆ’
2622, 24, 25co 7377 . . . . . . . 8 class ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2)))
27 c1 11076 . . . . . . . 8 class 1
2826, 27wceq 1541 . . . . . . 7 wff ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1
2919, 28wa 396 . . . . . 6 wff (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)
30 cn0 12437 . . . . . 6 class โ„•0
3129, 13, 30wrex 3069 . . . . 5 wff โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)
3231, 8, 30wrex 3069 . . . 4 wff โˆƒ๐‘ง โˆˆ โ„•0 โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)
33 cr 11074 . . . 4 class โ„
3432, 6, 33crab 3418 . . 3 class {๐‘ฆ โˆˆ โ„ โˆฃ โˆƒ๐‘ง โˆˆ โ„•0 โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)}
352, 5, 34cmpt 5208 . 2 class (๐‘ฅ โˆˆ (โ„• โˆ– โ—ปNN) โ†ฆ {๐‘ฆ โˆˆ โ„ โˆฃ โˆƒ๐‘ง โˆˆ โ„•0 โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)})
361, 35wceq 1541 1 wff Pell1QR = (๐‘ฅ โˆˆ (โ„• โˆ– โ—ปNN) โ†ฆ {๐‘ฆ โˆˆ โ„ โˆฃ โˆƒ๐‘ง โˆˆ โ„•0 โˆƒ๐‘ค โˆˆ โ„•0 (๐‘ฆ = (๐‘ง + ((โˆšโ€˜๐‘ฅ) ยท ๐‘ค)) โˆง ((๐‘งโ†‘2) โˆ’ (๐‘ฅ ยท (๐‘คโ†‘2))) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  pell1qrval  41260
  Copyright terms: Public domain W3C validator