Theorem pellfundval

Description: Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014) (Revised by AV, 17-Sep-2020)

	Ref	Expression
Assertion	pellfundval	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)=sup\left(\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\},ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢a=D\to \mathrm{Pell14QR}\left(a\right)=\mathrm{Pell14QR}\left(D\right)$$
2		rabeq	$$⊢\mathrm{Pell14QR}\left(a\right)=\mathrm{Pell14QR}\left(D\right)\to \left\{x\in \mathrm{Pell14QR}\left(a\right)|1<x\right\}=\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\}$$
3	1 2	syl	$$⊢a=D\to \left\{x\in \mathrm{Pell14QR}\left(a\right)|1<x\right\}=\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\}$$
4	3	infeq1d	$$⊢a=D\to sup\left(\left\{x\in \mathrm{Pell14QR}\left(a\right)|1<x\right\},ℝ,<\right)=sup\left(\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\},ℝ,<\right)$$
5		df-pellfund	$$⊢\mathrm{PellFund}=\left(a\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)⟼sup\left(\left\{x\in \mathrm{Pell14QR}\left(a\right)|1<x\right\},ℝ,<\right)\right)$$
6		ltso	$$⊢<\mathrm{Or}ℝ$$
7	6	infex	$$⊢sup\left(\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\},ℝ,<\right)\in \mathrm{V}$$
8	4 5 7	fvmpt	$$⊢D\in \left(\mathbb{N}\setminus {◻}_{\mathbb{N}}\right)\to \mathrm{PellFund}\left(D\right)=sup\left(\left\{x\in \mathrm{Pell14QR}\left(D\right)|1<x\right\},ℝ,<\right)$$