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 ( ( 𝐷 ∈ ( ℕ ∖ ◻NN ) ∧ 𝐴 ∈ ( Pell14QR ‘ 𝐷 ) ∧ ( 1 ≤ 𝐴 ∧ 𝐴 < ( PellFund ‘ 𝐷 ) ) ) → 𝐴 = 1 )

Proof

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