Metamath Proof Explorer


Definition df-pell1234qr

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

Ref Expression
Assertion df-pell1234qr Pell1234QR = x y | z w y = z + x w z 2 x w 2 = 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpell1234qr class Pell1234QR
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 cz class
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 y = z + x w z 2 x w 2 = 1
32 31 7 8 wrex wff z w y = z + x w z 2 x w 2 = 1
33 32 5 6 crab class y | z w y = z + x w z 2 x w 2 = 1
34 1 4 33 cmpt class x y | z w y = z + x w z 2 x w 2 = 1
35 0 34 wceq wff Pell1234QR = x y | z w y = z + x w z 2 x w 2 = 1