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 = ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ inf ( { 𝑧 ∈ ( Pell14QR ‘ 𝑥 ) ∣ 1 < 𝑧 } , ℝ , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpellfund	⊢ PellFund
1		vx	⊢ 𝑥
2		cn	⊢ ℕ
3		csquarenn	⊢ ◻NN
4	2 3	cdif	⊢ ( ℕ ∖ ◻NN )
5		vz	⊢ 𝑧
6		cpell14qr	⊢ Pell14QR
7	1	cv	⊢ 𝑥
8	7 6	cfv	⊢ ( Pell14QR ‘ 𝑥 )
9		c1	⊢ 1
10		clt	⊢ <
11	5	cv	⊢ 𝑧
12	9 11 10	wbr	⊢ 1 < 𝑧
13	12 5 8	crab	⊢ { 𝑧 ∈ ( Pell14QR ‘ 𝑥 ) ∣ 1 < 𝑧 }
14		cr	⊢ ℝ
15	13 14 10	cinf	⊢ inf ( { 𝑧 ∈ ( Pell14QR ‘ 𝑥 ) ∣ 1 < 𝑧 } , ℝ , < )
16	1 4 15	cmpt	⊢ ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ inf ( { 𝑧 ∈ ( Pell14QR ‘ 𝑥 ) ∣ 1 < 𝑧 } , ℝ , < ) )
17	0 16	wceq	⊢ PellFund = ( 𝑥 ∈ ( ℕ ∖ ◻NN ) ↦ inf ( { 𝑧 ∈ ( Pell14QR ‘ 𝑥 ) ∣ 1 < 𝑧 } , ℝ , < ) )