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	$$⊢\mathrm{PellFund}=\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼sup\left(\left\{z\in \mathrm{Pell14QR}\left(x\right)|1<z\right\},ℝ,<\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpellfund	$$class\mathrm{PellFund}$$
1		vx	$$setvarx$$
2		cn	$$class\mathbb{N}$$
3		csquarenn	$$class{◻}_{\mathbb{N}}$$
4	2 3	cdif	$$class\left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)$$
5		vz	$$setvarz$$
6		cpell14qr	$$class\mathrm{Pell14QR}$$
7	1	cv	$$setvarx$$
8	7 6	cfv	$$class\mathrm{Pell14QR}\left(x\right)$$
9		c1	$$class1$$
10		clt	$$class<$$
11	5	cv	$$setvarz$$
12	9 11 10	wbr	$$wff1<z$$
13	12 5 8	crab	$$class\left\{z\in \mathrm{Pell14QR}\left(x\right)|1<z\right\}$$
14		cr	$$classℝ$$
15	13 14 10	cinf	$$classsup\left(\left\{z\in \mathrm{Pell14QR}\left(x\right)|1<z\right\},ℝ,<\right)$$
16	1 4 15	cmpt	$$class\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼sup\left(\left\{z\in \mathrm{Pell14QR}\left(x\right)|1<z\right\},ℝ,<\right)\right)$$
17	0 16	wceq	$$wff\mathrm{PellFund}=\left(x\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼sup\left(\left\{z\in \mathrm{Pell14QR}\left(x\right)|1<z\right\},ℝ,<\right)\right)$$