Metamath Proof Explorer

Theorem pellfundlb

Description: A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014) (Proof shortened by AV, 15-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 pellfundval ⊢D∈ℕ∖◻ℕ→PellFund⁡D=supa∈Pell14QR⁡D|1<aℝ<
2 1 3ad2ant1 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→PellFund⁡D=supa∈Pell14QR⁡D|1<aℝ<
3 ssrab2 ⊢a∈Pell14QR⁡D|1<a⊆Pell14QR⁡D
4 pell14qrre ⊢D∈ℕ∖◻ℕ∧d∈Pell14QR⁡D→d∈ℝ
5 4 ex ⊢D∈ℕ∖◻ℕ→d∈Pell14QR⁡D→d∈ℝ
6 5 ssrdv ⊢D∈ℕ∖◻ℕ→Pell14QR⁡D⊆ℝ
7 3 6 sstrid ⊢D∈ℕ∖◻ℕ→a∈Pell14QR⁡D|1<a⊆ℝ
8 7 3ad2ant1 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→a∈Pell14QR⁡D|1<a⊆ℝ
9 1re ⊢1∈ℝ
10 breq2 ⊢a=c→1<a↔1<c
11 10 elrab ⊢c∈a∈Pell14QR⁡D|1<a↔c∈Pell14QR⁡D∧1<c
12 pell14qrre ⊢D∈ℕ∖◻ℕ∧c∈Pell14QR⁡D→c∈ℝ
13 ltle ⊢1∈ℝ∧c∈ℝ→1<c→1≤c
14 9 12 13 sylancr ⊢D∈ℕ∖◻ℕ∧c∈Pell14QR⁡D→1<c→1≤c
15 14 expimpd ⊢D∈ℕ∖◻ℕ→c∈Pell14QR⁡D∧1<c→1≤c
16 11 15 biimtrid ⊢D∈ℕ∖◻ℕ→c∈a∈Pell14QR⁡D|1<a→1≤c
17 16 ralrimiv ⊢D∈ℕ∖◻ℕ→∀c∈a∈Pell14QR⁡D|1<a1≤c
18 17 3ad2ant1 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→∀c∈a∈Pell14QR⁡D|1<a1≤c
19 breq1 ⊢b=1→b≤c↔1≤c
20 19 ralbidv ⊢b=1→∀c∈a∈Pell14QR⁡D|1<ab≤c↔∀c∈a∈Pell14QR⁡D|1<a1≤c
21 20 rspcev ⊢1∈ℝ∧∀c∈a∈Pell14QR⁡D|1<a1≤c→∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c
22 9 18 21 sylancr ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c
23 simp2 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→A∈Pell14QR⁡D
24 simp3 ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→1<A
25 breq2 ⊢a=A→1<a↔1<A
26 25 elrab ⊢A∈a∈Pell14QR⁡D|1<a↔A∈Pell14QR⁡D∧1<A
27 23 24 26 sylanbrc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→A∈a∈Pell14QR⁡D|1<a
28 infrelb ⊢a∈Pell14QR⁡D|1<a⊆ℝ∧∃b∈ℝ∀c∈a∈Pell14QR⁡D|1<ab≤c∧A∈a∈Pell14QR⁡D|1<a→supa∈Pell14QR⁡D|1<aℝ<≤A
29 8 22 27 28 syl3anc ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→supa∈Pell14QR⁡D|1<aℝ<≤A
30 2 29 eqbrtrd ⊢D∈ℕ∖◻ℕ∧A∈Pell14QR⁡D∧1<A→PellFund⁡D≤A