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