Metamath Proof Explorer

Theorem pellfundglb

Description: If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014)

Ref Expression
Assertion pellfundglb ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∃ x ∈ Pell1QR ⁡ D PellFund ⁡ D ≤ x ∧ x < A

Proof

Step Hyp Ref Expression
1 pellfundval ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D = sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
2 1 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → PellFund ⁡ D = sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
3 simp3 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → PellFund ⁡ D < A
4 2 3 eqbrtrrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → sup a ∈ Pell14QR ⁡ D | 1 < a ℝ < < A
5 pellfundre ⊢ D ∈ ℕ ∖ ◻ ℕ → PellFund ⁡ D ∈ ℝ
6 5 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → PellFund ⁡ D ∈ ℝ
7 2 6 eqeltrrd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → sup a ∈ Pell14QR ⁡ D | 1 < a ℝ < ∈ ℝ
8 simp2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → A ∈ ℝ
9 7 8 ltnled ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → sup a ∈ Pell14QR ⁡ D | 1 < a ℝ < < A ↔ ¬ A ≤ sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
10 4 9 mpbid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ¬ A ≤ sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
11 ssrab2 ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ Pell14QR ⁡ D
12 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ a ∈ Pell14QR ⁡ D → a ∈ ℝ
13 12 ex ⊢ D ∈ ℕ ∖ ◻ ℕ → a ∈ Pell14QR ⁡ D → a ∈ ℝ
14 13 ssrdv ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell14QR ⁡ D ⊆ ℝ
15 14 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → Pell14QR ⁡ D ⊆ ℝ
16 11 15 sstrid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ
17 pell1qrss14 ⊢ D ∈ ℕ ∖ ◻ ℕ → Pell1QR ⁡ D ⊆ Pell14QR ⁡ D
18 17 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → Pell1QR ⁡ D ⊆ Pell14QR ⁡ D
19 pellqrex ⊢ D ∈ ℕ ∖ ◻ ℕ → ∃ a ∈ Pell1QR ⁡ D 1 < a
20 19 3ad2ant1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∃ a ∈ Pell1QR ⁡ D 1 < a
21 ssrexv ⊢ Pell1QR ⁡ D ⊆ Pell14QR ⁡ D → ∃ a ∈ Pell1QR ⁡ D 1 < a → ∃ a ∈ Pell14QR ⁡ D 1 < a
22 18 20 21 sylc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∃ a ∈ Pell14QR ⁡ D 1 < a
23 rabn0 ⊢ a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅ ↔ ∃ a ∈ Pell14QR ⁡ D 1 < a
24 22 23 sylibr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅
25 infmrgelbi ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ ∧ a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅ ∧ A ∈ ℝ ∧ ∀ x ∈ a ∈ Pell14QR ⁡ D | 1 < a A ≤ x → A ≤ sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
26 25 ex ⊢ a ∈ Pell14QR ⁡ D | 1 < a ⊆ ℝ ∧ a ∈ Pell14QR ⁡ D | 1 < a ≠ ∅ ∧ A ∈ ℝ → ∀ x ∈ a ∈ Pell14QR ⁡ D | 1 < a A ≤ x → A ≤ sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
27 16 24 8 26 syl3anc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∀ x ∈ a ∈ Pell14QR ⁡ D | 1 < a A ≤ x → A ≤ sup a ∈ Pell14QR ⁡ D | 1 < a ℝ <
28 10 27 mtod ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ¬ ∀ x ∈ a ∈ Pell14QR ⁡ D | 1 < a A ≤ x
29 rexnal ⊢ ∃ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ¬ A ≤ x ↔ ¬ ∀ x ∈ a ∈ Pell14QR ⁡ D | 1 < a A ≤ x
30 28 29 sylibr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∃ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ¬ A ≤ x
31 breq2 ⊢ a = x → 1 < a ↔ 1 < x
32 31 elrab ⊢ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ↔ x ∈ Pell14QR ⁡ D ∧ 1 < x
33 simprl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → x ∈ Pell14QR ⁡ D
34 1red ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → 1 ∈ ℝ
35 simpl1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → D ∈ ℕ ∖ ◻ ℕ
36 pell14qrre ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ x ∈ Pell14QR ⁡ D → x ∈ ℝ
37 35 33 36 syl2anc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → x ∈ ℝ
38 simprr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → 1 < x
39 34 37 38 ltled ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → 1 ≤ x
40 33 39 jca ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → x ∈ Pell14QR ⁡ D ∧ 1 ≤ x
41 elpell1qr2 ⊢ D ∈ ℕ ∖ ◻ ℕ → x ∈ Pell1QR ⁡ D ↔ x ∈ Pell14QR ⁡ D ∧ 1 ≤ x
42 35 41 syl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → x ∈ Pell1QR ⁡ D ↔ x ∈ Pell14QR ⁡ D ∧ 1 ≤ x
43 40 42 mpbird ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → x ∈ Pell1QR ⁡ D
44 32 43 sylan2b ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a → x ∈ Pell1QR ⁡ D
45 44 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x ∈ Pell1QR ⁡ D
46 simpl1 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → D ∈ ℕ ∖ ◻ ℕ
47 simprl ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x ∈ a ∈ Pell14QR ⁡ D | 1 < a
48 11 47 sselid ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x ∈ Pell14QR ⁡ D
49 simpr ⊢ x ∈ Pell14QR ⁡ D ∧ 1 < x → 1 < x
50 49 a1i ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → x ∈ Pell14QR ⁡ D ∧ 1 < x → 1 < x
51 32 50 syl5bi ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → x ∈ a ∈ Pell14QR ⁡ D | 1 < a → 1 < x
52 51 imp ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a → 1 < x
53 52 adantrr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → 1 < x
54 pellfundlb ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ x ∈ Pell14QR ⁡ D ∧ 1 < x → PellFund ⁡ D ≤ x
55 46 48 53 54 syl3anc ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → PellFund ⁡ D ≤ x
56 simprr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → ¬ A ≤ x
57 15 adantr ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → Pell14QR ⁡ D ⊆ ℝ
58 57 48 sseldd ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x ∈ ℝ
59 simpl2 ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → A ∈ ℝ
60 58 59 ltnled ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x < A ↔ ¬ A ≤ x
61 56 60 mpbird ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → x < A
62 55 61 jca ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A ∧ x ∈ a ∈ Pell14QR ⁡ D | 1 < a ∧ ¬ A ≤ x → PellFund ⁡ D ≤ x ∧ x < A
63 30 45 62 reximssdv ⊢ D ∈ ℕ ∖ ◻ ℕ ∧ A ∈ ℝ ∧ PellFund ⁡ D < A → ∃ x ∈ Pell1QR ⁡ D PellFund ⁡ D ≤ x ∧ x < A