Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pellfund Structured version   Visualization version   GIF version

Definition df-pellfund 37928
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
StepHypRef Expression
1 cpellfund 37923 . 2 class PellFund
2 vx . . 3 setvar 𝑥
3 cn 11221 . . . 4 class
4 csquarenn 37919 . . . 4 class NN
53, 4cdif 3718 . . 3 class (ℕ ∖ ◻NN)
6 c1 10138 . . . . . 6 class 1
7 vz . . . . . . 7 setvar 𝑧
87cv 1629 . . . . . 6 class 𝑧
9 clt 10275 . . . . . 6 class <
106, 8, 9wbr 4784 . . . . 5 wff 1 < 𝑧
112cv 1629 . . . . . 6 class 𝑥
12 cpell14qr 37922 . . . . . 6 class Pell14QR
1311, 12cfv 6031 . . . . 5 class (Pell14QR‘𝑥)
1410, 7, 13crab 3064 . . . 4 class {𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}
15 cr 10136 . . . 4 class
1614, 15, 9cinf 8502 . . 3 class inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < )
172, 5, 16cmpt 4861 . 2 class (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
181, 17wceq 1630 1 wff PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
Colors of variables: wff setvar class
This definition is referenced by:  pellfundval  37963
  Copyright terms: Public domain W3C validator