Metamath Proof Explorer

Theorem pellfund14gap

Description: There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfund14gap ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→A=1

Proof

Step Hyp Ref Expression
1 simp3r ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→A<PellFund⁡D
2 pell14qrre ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D→A∈ℝ
3 2 3adant3 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→A∈ℝ
4 pellfundre ⊢D∈ℕ∖◻ℕ→PellFund⁡D∈ℝ
5 4 3ad2ant1 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→PellFund⁡D∈ℝ
6 3 5 ltnled ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→A<PellFund⁡D↔¬PellFund⁡D≤A
7 1 6 mpbid ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→¬PellFund⁡D≤A
8 simpl1 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D∧1<A→D∈ℕ∖◻ℕ
9 simpl2 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D∧1<A→A∈Pell14QR⁡D
10 simpr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D∧1<A→1<A
11 pellfundlb ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→PellFund⁡D≤A
12 8 9 10 11 syl3anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D∧1<A→PellFund⁡D≤A
13 7 12 mtand ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→¬1<A
14 simp3l ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→1≤A
15 1re ⊢1∈ℝ
16 leloe ⊢1∈ℝ∧A∈ℝ→1≤A↔1<A∨1=A
17 15 3 16 sylancr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→1≤A↔1<A∨1=A
18 14 17 mpbid ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→1<A∨1=A
19 orel1 ⊢¬1<A→1<A∨1=A→1=A
20 13 18 19 sylc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→1=A
21 20 eqcomd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1≤A∧A<PellFund⁡D→A=1