Definition df-pellfund 39449

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

Distinct variable group:   𝑥,𝑧

Detailed syntax breakdown of Definition df-pellfund

Step	Hyp	Ref	Expression
1		cpellfund 39444	. 2 class PellFund
2		vx	. . 3 setvar 𝑥
3		cn 11640	. . . 4 class ℕ
4		csquarenn 39440	. . . 4 class ◻NN
5	3, 4	cdif 3935	. . 3 class (ℕ ∖ ◻NN)
6		c1 10540	. . . . . 6 class 1
7		vz	. . . . . . 7 setvar 𝑧
8	7	cv 1536	. . . . . 6 class 𝑧
9		clt 10677	. . . . . 6 class <
10	6, 8, 9	wbr 5068	. . . . 5 wff 1 < 𝑧
11	2	cv 1536	. . . . . 6 class 𝑥
12		cpell14qr 39443	. . . . . 6 class Pell14QR
13	11, 12	cfv 6357	. . . . 5 class (Pell14QR‘𝑥)
14	10, 7, 13	crab 3144	. . . 4 class {𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}
15		cr 10538	. . . 4 class ℝ
16	14, 15, 9	cinf 8907	. . 3 class inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < )
17	2, 5, 16	cmpt 5148	. 2 class (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
18	1, 17	wceq 1537	1 wff PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))

This definition is referenced by:  pellfundval  39484