| Step | Hyp | Ref
| Expression |
| 1 | | pellfundval 42891 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) = inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
| 2 | 1 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) = inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
| 3 | | simp3 1139 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) < 𝐴) |
| 4 | 2, 3 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) < 𝐴) |
| 5 | | pellfundre 42892 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℝ) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) ∈ ℝ) |
| 7 | 2, 6 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) ∈
ℝ) |
| 8 | | simp2 1138 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → 𝐴 ∈ ℝ) |
| 9 | 7, 8 | ltnled 11408 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) < 𝐴 ↔ ¬ 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
| 10 | 4, 9 | mpbid 232 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ¬ 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
| 11 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ (Pell14QR‘𝐷) |
| 12 | | pell14qrre 42868 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ) |
| 13 | 12 | ex 412 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝑎 ∈ (Pell14QR‘𝐷) → 𝑎 ∈ ℝ)) |
| 14 | 13 | ssrdv 3989 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell14QR‘𝐷) ⊆ ℝ) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (Pell14QR‘𝐷) ⊆ ℝ) |
| 16 | 11, 15 | sstrid 3995 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ) |
| 17 | | pell1qrss14 42879 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 18 | 17 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 19 | | pellqrex 42890 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ∃𝑎 ∈ (Pell1QR‘𝐷)1 < 𝑎) |
| 20 | 19 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑎 ∈ (Pell1QR‘𝐷)1 < 𝑎) |
| 21 | | ssrexv 4053 |
. . . . . . 7
⊢
((Pell1QR‘𝐷)
⊆ (Pell14QR‘𝐷)
→ (∃𝑎 ∈
(Pell1QR‘𝐷)1 <
𝑎 → ∃𝑎 ∈ (Pell14QR‘𝐷)1 < 𝑎)) |
| 22 | 18, 20, 21 | sylc 65 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑎 ∈ (Pell14QR‘𝐷)1 < 𝑎) |
| 23 | | rabn0 4389 |
. . . . . 6
⊢ ({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ↔
∃𝑎 ∈
(Pell14QR‘𝐷)1 <
𝑎) |
| 24 | 22, 23 | sylibr 234 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅) |
| 25 | | infmrgelbi 42889 |
. . . . . 6
⊢ ((({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ ∧ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ∧ 𝐴 ∈ ℝ) ∧
∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
| 26 | 25 | ex 412 |
. . . . 5
⊢ (({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ ∧ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ∧ 𝐴 ∈ ℝ) →
(∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥 → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
| 27 | 16, 24, 8, 26 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥 → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
| 28 | 10, 27 | mtod 198 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ¬ ∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) |
| 29 | | rexnal 3100 |
. . 3
⊢
(∃𝑥 ∈
{𝑎 ∈
(Pell14QR‘𝐷) ∣
1 < 𝑎} ¬ 𝐴 ≤ 𝑥 ↔ ¬ ∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) |
| 30 | 28, 29 | sylibr 234 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ¬ 𝐴 ≤ 𝑥) |
| 31 | | breq2 5147 |
. . . . 5
⊢ (𝑎 = 𝑥 → (1 < 𝑎 ↔ 1 < 𝑥)) |
| 32 | 31 | elrab 3692 |
. . . 4
⊢ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) |
| 33 | | simprl 771 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ (Pell14QR‘𝐷)) |
| 34 | | 1red 11262 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 ∈ ℝ) |
| 35 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 36 | | pell14qrre 42868 |
. . . . . . . 8
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑥 ∈ (Pell14QR‘𝐷)) → 𝑥 ∈ ℝ) |
| 37 | 35, 33, 36 | syl2anc 584 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ ℝ) |
| 38 | | simprr 773 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 < 𝑥) |
| 39 | 34, 37, 38 | ltled 11409 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 ≤ 𝑥) |
| 40 | 33, 39 | jca 511 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥)) |
| 41 | | elpell1qr2 42883 |
. . . . . 6
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝑥 ∈ (Pell1QR‘𝐷) ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥))) |
| 42 | 35, 41 | syl 17 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → (𝑥 ∈ (Pell1QR‘𝐷) ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥))) |
| 43 | 40, 42 | mpbird 257 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ (Pell1QR‘𝐷)) |
| 44 | 32, 43 | sylan2b 594 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) → 𝑥 ∈ (Pell1QR‘𝐷)) |
| 45 | 44 | adantrr 717 |
. 2
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ (Pell1QR‘𝐷)) |
| 46 | | simpl1 1192 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 47 | | simprl 771 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) |
| 48 | 11, 47 | sselid 3981 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ (Pell14QR‘𝐷)) |
| 49 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → 1 < 𝑥) |
| 50 | 49 | a1i 11 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ((𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → 1 < 𝑥)) |
| 51 | 32, 50 | biimtrid 242 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} → 1 < 𝑥)) |
| 52 | 51 | imp 406 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) → 1 < 𝑥) |
| 53 | 52 | adantrr 717 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 1 < 𝑥) |
| 54 | | pellfundlb 42895 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → (PellFund‘𝐷) ≤ 𝑥) |
| 55 | 46, 48, 53, 54 | syl3anc 1373 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (PellFund‘𝐷) ≤ 𝑥) |
| 56 | | simprr 773 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → ¬ 𝐴 ≤ 𝑥) |
| 57 | 15 | adantr 480 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (Pell14QR‘𝐷) ⊆ ℝ) |
| 58 | 57, 48 | sseldd 3984 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
| 59 | | simpl2 1193 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝐴 ∈ ℝ) |
| 60 | 58, 59 | ltnled 11408 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (𝑥 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑥)) |
| 61 | 56, 60 | mpbird 257 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 < 𝐴) |
| 62 | 55, 61 | jca 511 |
. 2
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → ((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) |
| 63 | 30, 45, 62 | reximssdv 3173 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) |