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 37908
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 37903 . 2 class Pell1QR
2 vx . . 3 setvar 𝑥
3 cn 11212 . . . 4 class
4 csquarenn 37902 . . . 4 class NN
53, 4cdif 3712 . . 3 class (ℕ ∖ ◻NN)
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1631 . . . . . . . 8 class 𝑦
8 vz . . . . . . . . . 10 setvar 𝑧
98cv 1631 . . . . . . . . 9 class 𝑧
102cv 1631 . . . . . . . . . . 11 class 𝑥
11 csqrt 14172 . . . . . . . . . . 11 class
1210, 11cfv 6049 . . . . . . . . . 10 class (√‘𝑥)
13 vw . . . . . . . . . . 11 setvar 𝑤
1413cv 1631 . . . . . . . . . 10 class 𝑤
15 cmul 10133 . . . . . . . . . 10 class ·
1612, 14, 15co 6813 . . . . . . . . 9 class ((√‘𝑥) · 𝑤)
17 caddc 10131 . . . . . . . . 9 class +
189, 16, 17co 6813 . . . . . . . 8 class (𝑧 + ((√‘𝑥) · 𝑤))
197, 18wceq 1632 . . . . . . 7 wff 𝑦 = (𝑧 + ((√‘𝑥) · 𝑤))
20 c2 11262 . . . . . . . . . 10 class 2
21 cexp 13054 . . . . . . . . . 10 class
229, 20, 21co 6813 . . . . . . . . 9 class (𝑧↑2)
2314, 20, 21co 6813 . . . . . . . . . 10 class (𝑤↑2)
2410, 23, 15co 6813 . . . . . . . . 9 class (𝑥 · (𝑤↑2))
25 cmin 10458 . . . . . . . . 9 class
2622, 24, 25co 6813 . . . . . . . 8 class ((𝑧↑2) − (𝑥 · (𝑤↑2)))
27 c1 10129 . . . . . . . 8 class 1
2826, 27wceq 1632 . . . . . . 7 wff ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1
2919, 28wa 383 . . . . . 6 wff (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
30 cn0 11484 . . . . . 6 class 0
3129, 13, 30wrex 3051 . . . . 5 wff 𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
3231, 8, 30wrex 3051 . . . 4 wff 𝑧 ∈ ℕ0𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
33 cr 10127 . . . 4 class
3432, 6, 33crab 3054 . . 3 class {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}
352, 5, 34cmpt 4881 . 2 class (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
361, 35wceq 1632 1 wff Pell1QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
Colors of variables: wff setvar class
This definition is referenced by:  pell1qrval  37912
  Copyright terms: Public domain W3C validator