Metamath Proof Explorer

Definition df-pell1qr

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)

Ref Expression
Assertion df-pell1qr ⊢ Pell1QR = x ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpell1qr class Pell1QR
1 vx setvar x
2 cn class ℕ
3 csquarenn class ◻ ℕ
4 2 3 cdif class ℕ ∖ ◻ ℕ
5 vy setvar y
6 cr class ℝ
7 vz setvar z
8 cn0 class ℕ 0
9 vw setvar w
10 5 cv setvar y
11 7 cv setvar z
12 caddc class +
13 csqrt class √
14 1 cv setvar x
15 14 13 cfv class x
16 cmul class ×
17 9 cv setvar w
18 15 17 16 co class x ⁢ w
19 11 18 12 co class z + x ⁢ w
20 10 19 wceq wff y = z + x ⁢ w
21 cexp class ^
22 c2 class 2
23 11 22 21 co class z 2
24 cmin class −
25 17 22 21 co class w 2
26 14 25 16 co class x ⁢ w 2
27 23 26 24 co class z 2 − x ⁢ w 2
28 c1 class 1
29 27 28 wceq wff z 2 − x ⁢ w 2 = 1
30 20 29 wa wff y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
31 30 9 8 wrex wff ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
32 31 7 8 wrex wff ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
33 32 5 6 crab class y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
34 1 4 33 cmpt class x ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
35 0 34 wceq wff Pell1QR = x ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℕ 0 y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1