Metamath Proof Explorer


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 < 𝑥 } , ℝ , < ) )