Metamath Proof Explorer

Definition df-pell14qr

Description: Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpell14qr class Pell14QR
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 cz class ℤ
11 5 cv setvar y
12 7 cv setvar z
13 caddc class +
14 csqrt class √
15 1 cv setvar x
16 15 14 cfv class x
17 cmul class ×
18 9 cv setvar w
19 16 18 17 co class x ⁢ w
20 12 19 13 co class z + x ⁢ w
21 11 20 wceq wff y = z + x ⁢ w
22 cexp class ^
23 c2 class 2
24 12 23 22 co class z 2
25 cmin class −
26 18 23 22 co class w 2
27 15 26 17 co class x ⁢ w 2
28 24 27 25 co class z 2 − x ⁢ w 2
29 c1 class 1
30 28 29 wceq wff z 2 − x ⁢ w 2 = 1
31 21 30 wa wff y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
32 31 9 10 wrex wff ∃ w ∈ ℤ y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
33 32 7 8 wrex wff ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
34 33 5 6 crab class y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
35 1 4 34 cmpt class x ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1
36 0 35 wceq wff Pell14QR = x ∈ ℕ ∖ ◻ ℕ ⟼ y ∈ ℝ | ∃ z ∈ ℕ 0 ∃ w ∈ ℤ y = z + x ⁢ w ∧ z 2 − x ⁢ w 2 = 1