Metamath Proof Explorer


Definition df-pellfund

Description: A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014) (Revised by AV, 17-Sep-2020)

Ref Expression
Assertion df-pellfund PellFund = x sup z Pell14QR x | 1 < z <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpellfund class PellFund
1 vx setvar x
2 cn class
3 csquarenn class
4 2 3 cdif class
5 vz setvar z
6 cpell14qr class Pell14QR
7 1 cv setvar x
8 7 6 cfv class Pell14QR x
9 c1 class 1
10 clt class <
11 5 cv setvar z
12 9 11 10 wbr wff 1 < z
13 12 5 8 crab class z Pell14QR x | 1 < z
14 cr class
15 13 14 10 cinf class sup z Pell14QR x | 1 < z <
16 1 4 15 cmpt class x sup z Pell14QR x | 1 < z <
17 0 16 wceq wff PellFund = x sup z Pell14QR x | 1 < z <