Definition df-pell1qr 41580

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

Step	Hyp	Ref	Expression
1		cpell1qr 41575	. 2 class Pell1QR
2		vx	. . 3 setvar 𝑥
3		cn 12212	. . . 4 class ℕ
4		csquarenn 41574	. . . 4 class ◻NN
5	3, 4	cdif 3946	. . 3 class (ℕ ∖ ◻NN)
6		vy	. . . . . . . . 9 setvar 𝑦
7	6	cv 1541	. . . . . . . 8 class 𝑦
8		vz	. . . . . . . . . 10 setvar 𝑧
9	8	cv 1541	. . . . . . . . 9 class 𝑧
10	2	cv 1541	. . . . . . . . . . 11 class 𝑥
11		csqrt 15180	. . . . . . . . . . 11 class √
12	10, 11	cfv 6544	. . . . . . . . . 10 class (√‘𝑥)
13		vw	. . . . . . . . . . 11 setvar 𝑤
14	13	cv 1541	. . . . . . . . . 10 class 𝑤
15		cmul 11115	. . . . . . . . . 10 class ·
16	12, 14, 15	co 7409	. . . . . . . . 9 class ((√‘𝑥) · 𝑤)
17		caddc 11113	. . . . . . . . 9 class +
18	9, 16, 17	co 7409	. . . . . . . 8 class (𝑧 + ((√‘𝑥) · 𝑤))
19	7, 18	wceq 1542	. . . . . . 7 wff 𝑦 = (𝑧 + ((√‘𝑥) · 𝑤))
20		c2 12267	. . . . . . . . . 10 class 2
21		cexp 14027	. . . . . . . . . 10 class ↑
22	9, 20, 21	co 7409	. . . . . . . . 9 class (𝑧↑2)
23	14, 20, 21	co 7409	. . . . . . . . . 10 class (𝑤↑2)
24	10, 23, 15	co 7409	. . . . . . . . 9 class (𝑥 · (𝑤↑2))
25		cmin 11444	. . . . . . . . 9 class −
26	22, 24, 25	co 7409	. . . . . . . 8 class ((𝑧↑2) − (𝑥 · (𝑤↑2)))
27		c1 11111	. . . . . . . 8 class 1
28	26, 27	wceq 1542	. . . . . . 7 wff ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1
29	19, 28	wa 397	. . . . . 6 wff (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
30		cn0 12472	. . . . . 6 class ℕ0
31	29, 13, 30	wrex 3071	. . . . 5 wff ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
32	31, 8, 30	wrex 3071	. . . 4 wff ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)
33		cr 11109	. . . 4 class ℝ
34	32, 6, 33	crab 3433	. . 3 class {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}
35	2, 5, 34	cmpt 5232	. 2 class (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})
36	1, 35	wceq 1542	1 wff Pell1QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)})

This definition is referenced by:  pell1qrval  41584