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

Definition df-pellfund 29646
Description: A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
Assertion
Ref Expression
df-pellfund
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-pellfund
StepHypRef Expression
1 cpellfund 29641 . 2
2 vx . . 3
3 cn 10460 . . . 4
4 csquarenn 29637 . . . 4
53, 4cdif 3439 . . 3
6 c1 9420 . . . . . 6
7 vz . . . . . . 7
87cv 1369 . . . . . 6
9 clt 9555 . . . . . 6
106, 8, 9wbr 4409 . . . . 5
112cv 1369 . . . . . 6
12 cpell14qr 29640 . . . . . 6
1311, 12cfv 5537 . . . . 5
1410, 7, 13crab 2804 . . . 4
15 cr 9418 . . . 4
169ccnv 4956 . . . 4
1714, 15, 16csup 7826 . . 3
182, 5, 17cmpt 4467 . 2
191, 18wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  pellfundval  29681
  Copyright terms: Public domain W3C validator