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

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑎 = 𝐷 → ( Pell14QR ‘ 𝑎 ) = ( Pell14QR ‘ 𝐷 ) )
2		rabeq	⊢ ( ( Pell14QR ‘ 𝑎 ) = ( Pell14QR ‘ 𝐷 ) → { 𝑥 ∈ ( Pell14QR ‘ 𝑎 ) ∣ 1 < 𝑥 } = { 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑥 } )
3	1 2	syl	⊢ ( 𝑎 = 𝐷 → { 𝑥 ∈ ( Pell14QR ‘ 𝑎 ) ∣ 1 < 𝑥 } = { 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑥 } )
4	3	infeq1d	⊢ ( 𝑎 = 𝐷 → inf ( { 𝑥 ∈ ( Pell14QR ‘ 𝑎 ) ∣ 1 < 𝑥 } , ℝ , < ) = inf ( { 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑥 } , ℝ , < ) )
5		df-pellfund	⊢ PellFund = ( 𝑎 ∈ ( ℕ ∖ ◻NN ) ↦ inf ( { 𝑥 ∈ ( Pell14QR ‘ 𝑎 ) ∣ 1 < 𝑥 } , ℝ , < ) )
6		ltso	⊢ < Or ℝ
7	6	infex	⊢ inf ( { 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑥 } , ℝ , < ) ∈ V
8	4 5 7	fvmpt	⊢ ( 𝐷 ∈ ( ℕ ∖ ◻NN ) → ( PellFund ‘ 𝐷 ) = inf ( { 𝑥 ∈ ( Pell14QR ‘ 𝐷 ) ∣ 1 < 𝑥 } , ℝ , < ) )