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