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 36427
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 36422 . 2 class PellFund
2 vx . . 3 setvar 𝑥
3 cn 10897 . . . 4 class
4 csquarenn 36418 . . . 4 class NN
53, 4cdif 3537 . . 3 class (ℕ ∖ ◻NN)
6 c1 9816 . . . . . 6 class 1
7 vz . . . . . . 7 setvar 𝑧
87cv 1474 . . . . . 6 class 𝑧
9 clt 9953 . . . . . 6 class <
106, 8, 9wbr 4583 . . . . 5 wff 1 < 𝑧
112cv 1474 . . . . . 6 class 𝑥
12 cpell14qr 36421 . . . . . 6 class Pell14QR
1311, 12cfv 5804 . . . . 5 class (Pell14QR‘𝑥)
1410, 7, 13crab 2900 . . . 4 class {𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}
15 cr 9814 . . . 4 class
1614, 15, 9cinf 8230 . . 3 class inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < )
172, 5, 16cmpt 4643 . 2 class (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
181, 17wceq 1475 1 wff PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < ))
Colors of variables: wff setvar class
This definition is referenced by:  pellfundval  36462
  Copyright terms: Public domain W3C validator