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 e. ( NN \ []NN ) |-> inf ( { z e. ( Pell14QR ` x ) | 1 < z } , RR , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpellfund	|- PellFund
1		vx	|- x
2		cn	|- NN
3		csquarenn	|- []NN
4	2 3	cdif	|- ( NN \ []NN )
5		vz	|- z
6		cpell14qr	|- Pell14QR
7	1	cv	|- x
8	7 6	cfv	|- ( Pell14QR ` x )
9		c1	|- 1
10		clt	|- <
11	5	cv	|- z
12	9 11 10	wbr	|- 1 < z
13	12 5 8	crab	|- { z e. ( Pell14QR ` x ) | 1 < z }
14		cr	|- RR
15	13 14 10	cinf	|- inf ( { z e. ( Pell14QR ` x ) | 1 < z } , RR , < )
16	1 4 15	cmpt	|- ( x e. ( NN \ []NN ) |-> inf ( { z e. ( Pell14QR ` x ) | 1 < z } , RR , < ) )
17	0 16	wceq	|- PellFund = ( x e. ( NN \ []NN ) |-> inf ( { z e. ( Pell14QR ` x ) | 1 < z } , RR , < ) )