Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stefan O'Rear
Pell equations 3: characterizing fundamental solution
pellfundne1
Next ⟩
Logarithm laws generalized to an arbitrary base
Metamath Proof Explorer
Ascii
Unicode
Theorem
pellfundne1
Description:
The fundamental Pell solution is never 1.
(Contributed by
Stefan O'Rear
, 19-Sep-2014)
Ref
Expression
Assertion
pellfundne1
⊢
D
∈
ℕ
∖
◻
ℕ
→
PellFund
⁡
D
≠
1
Proof
Step
Hyp
Ref
Expression
1
1red
⊢
D
∈
ℕ
∖
◻
ℕ
→
1
∈
ℝ
2
pellfundgt1
⊢
D
∈
ℕ
∖
◻
ℕ
→
1
<
PellFund
⁡
D
3
1
2
gtned
⊢
D
∈
ℕ
∖
◻
ℕ
→
PellFund
⁡
D
≠
1