Definition df-pellfund 37409

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.)

Assertion

Ref	Expression
df-pellfund	|- PellFund = ( x e. ( NN \ ◻NN ) |-> inf ( { z e. (Pell14QR ` x ) | 1 < z } , RR , < ) )

Distinct variable group:   x, z

Detailed syntax breakdown of Definition df-pellfund

Step	Hyp	Ref	Expression
1		cpellfund 37404	. 2 class PellFund
2		vx	. . 3 setvar x
3		cn 11020	. . . 4 class NN
4		csquarenn 37400	. . . 4 class ◻NN
5	3, 4	cdif 3571	. . 3 class ( NN \ ◻NN )
6		c1 9937	. . . . . 6 class 1
7		vz	. . . . . . 7 setvar z
8	7	cv 1482	. . . . . 6 class z
9		clt 10074	. . . . . 6 class <
10	6, 8, 9	wbr 4653	. . . . 5 wff 1 < z
11	2	cv 1482	. . . . . 6 class x
12		cpell14qr 37403	. . . . . 6 class Pell14QR
13	11, 12	cfv 5888	. . . . 5 class (Pell14QR ` x )
14	10, 7, 13	crab 2916	. . . 4 class { z e. (Pell14QR ` x ) | 1 < z }
15		cr 9935	. . . 4 class RR
16	14, 15, 9	cinf 8347	. . 3 class inf ( { z e. (Pell14QR ` x ) | 1 < z } , RR , < )
17	2, 5, 16	cmpt 4729	. 2 class ( x e. ( NN \ ◻NN ) |-> inf ( { z e. (Pell14QR ` x ) | 1 < z } , RR , < ) )
18	1, 17	wceq 1483	1 wff PellFund = ( x e. ( NN \ ◻NN ) |-> inf ( { z e. (Pell14QR ` x ) | 1 < z } , RR , < ) )

This definition is referenced by:  pellfundval  37444