Step | Hyp | Ref
| Expression |
1 | | pellfundval 39470 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) = inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
2 | 1 | 3ad2ant1 1129 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) = inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
3 | | simp3 1134 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) < 𝐴) |
4 | 2, 3 | eqbrtrrd 5083 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) < 𝐴) |
5 | | pellfundre 39471 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℝ) |
6 | 5 | 3ad2ant1 1129 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (PellFund‘𝐷) ∈ ℝ) |
7 | 2, 6 | eqeltrrd 2914 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) ∈
ℝ) |
8 | | simp2 1133 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → 𝐴 ∈ ℝ) |
9 | 7, 8 | ltnled 10781 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ) < 𝐴 ↔ ¬ 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
10 | 4, 9 | mpbid 234 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ¬ 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
11 | | ssrab2 4056 |
. . . . . 6
⊢ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ (Pell14QR‘𝐷) |
12 | | pell14qrre 39447 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ) |
13 | 12 | ex 415 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝑎 ∈ (Pell14QR‘𝐷) → 𝑎 ∈ ℝ)) |
14 | 13 | ssrdv 3973 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell14QR‘𝐷) ⊆ ℝ) |
15 | 14 | 3ad2ant1 1129 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (Pell14QR‘𝐷) ⊆ ℝ) |
16 | 11, 15 | sstrid 3978 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ) |
17 | | pell1qrss14 39458 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
18 | 17 | 3ad2ant1 1129 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
19 | | pellqrex 39469 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ∃𝑎 ∈ (Pell1QR‘𝐷)1 < 𝑎) |
20 | 19 | 3ad2ant1 1129 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑎 ∈ (Pell1QR‘𝐷)1 < 𝑎) |
21 | | ssrexv 4034 |
. . . . . . 7
⊢
((Pell1QR‘𝐷)
⊆ (Pell14QR‘𝐷)
→ (∃𝑎 ∈
(Pell1QR‘𝐷)1 <
𝑎 → ∃𝑎 ∈ (Pell14QR‘𝐷)1 < 𝑎)) |
22 | 18, 20, 21 | sylc 65 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑎 ∈ (Pell14QR‘𝐷)1 < 𝑎) |
23 | | rabn0 4339 |
. . . . . 6
⊢ ({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ↔
∃𝑎 ∈
(Pell14QR‘𝐷)1 <
𝑎) |
24 | 22, 23 | sylibr 236 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅) |
25 | | infmrgelbi 39468 |
. . . . . 6
⊢ ((({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ ∧ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ∧ 𝐴 ∈ ℝ) ∧
∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < )) |
26 | 25 | ex 415 |
. . . . 5
⊢ (({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ⊆ ℝ ∧ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ≠ ∅ ∧ 𝐴 ∈ ℝ) →
(∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥 → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
27 | 16, 24, 8, 26 | syl3anc 1367 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥 → 𝐴 ≤ inf({𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}, ℝ, < ))) |
28 | 10, 27 | mtod 200 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ¬ ∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) |
29 | | rexnal 3238 |
. . 3
⊢
(∃𝑥 ∈
{𝑎 ∈
(Pell14QR‘𝐷) ∣
1 < 𝑎} ¬ 𝐴 ≤ 𝑥 ↔ ¬ ∀𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}𝐴 ≤ 𝑥) |
30 | 28, 29 | sylibr 236 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ¬ 𝐴 ≤ 𝑥) |
31 | | breq2 5063 |
. . . . 5
⊢ (𝑎 = 𝑥 → (1 < 𝑎 ↔ 1 < 𝑥)) |
32 | 31 | elrab 3680 |
. . . 4
⊢ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) |
33 | | simprl 769 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ (Pell14QR‘𝐷)) |
34 | | 1red 10636 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 ∈ ℝ) |
35 | | simpl1 1187 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
36 | | pell14qrre 39447 |
. . . . . . . 8
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑥 ∈ (Pell14QR‘𝐷)) → 𝑥 ∈ ℝ) |
37 | 35, 33, 36 | syl2anc 586 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ ℝ) |
38 | | simprr 771 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 < 𝑥) |
39 | 34, 37, 38 | ltled 10782 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 1 ≤ 𝑥) |
40 | 33, 39 | jca 514 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥)) |
41 | | elpell1qr2 39462 |
. . . . . 6
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝑥 ∈ (Pell1QR‘𝐷) ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥))) |
42 | 35, 41 | syl 17 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → (𝑥 ∈ (Pell1QR‘𝐷) ↔ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝑥))) |
43 | 40, 42 | mpbird 259 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥)) → 𝑥 ∈ (Pell1QR‘𝐷)) |
44 | 32, 43 | sylan2b 595 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) → 𝑥 ∈ (Pell1QR‘𝐷)) |
45 | 44 | adantrr 715 |
. 2
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ (Pell1QR‘𝐷)) |
46 | | simpl1 1187 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
47 | | simprl 769 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) |
48 | 11, 47 | sseldi 3965 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ (Pell14QR‘𝐷)) |
49 | | simpr 487 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → 1 < 𝑥) |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ((𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → 1 < 𝑥)) |
51 | 32, 50 | syl5bi 244 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} → 1 < 𝑥)) |
52 | 51 | imp 409 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ 𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎}) → 1 < 𝑥) |
53 | 52 | adantrr 715 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 1 < 𝑥) |
54 | | pellfundlb 39474 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑥 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝑥) → (PellFund‘𝐷) ≤ 𝑥) |
55 | 46, 48, 53, 54 | syl3anc 1367 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (PellFund‘𝐷) ≤ 𝑥) |
56 | | simprr 771 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → ¬ 𝐴 ≤ 𝑥) |
57 | 15 | adantr 483 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (Pell14QR‘𝐷) ⊆ ℝ) |
58 | 57, 48 | sseldd 3968 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 ∈ ℝ) |
59 | | simpl2 1188 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝐴 ∈ ℝ) |
60 | 58, 59 | ltnled 10781 |
. . . 4
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → (𝑥 < 𝐴 ↔ ¬ 𝐴 ≤ 𝑥)) |
61 | 56, 60 | mpbird 259 |
. . 3
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → 𝑥 < 𝐴) |
62 | 55, 61 | jca 514 |
. 2
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) ∧ (𝑥 ∈ {𝑎 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑎} ∧ ¬ 𝐴 ≤ 𝑥)) → ((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) |
63 | 30, 45, 62 | reximssdv 3276 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) |