| Step | Hyp | Ref
| Expression |
| 1 | | 2re 12340 |
. . . 4
⊢ 2 ∈
ℝ |
| 2 | | pellfundre 42892 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℝ) |
| 3 | | remulcl 11240 |
. . . 4
⊢ ((2
∈ ℝ ∧ (PellFund‘𝐷) ∈ ℝ) → (2 ·
(PellFund‘𝐷)) ∈
ℝ) |
| 4 | 1, 2, 3 | sylancr 587 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (2 · (PellFund‘𝐷)) ∈
ℝ) |
| 5 | | 0red 11264 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 ∈ ℝ) |
| 6 | | 1red 11262 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 1 ∈ ℝ) |
| 7 | | 0lt1 11785 |
. . . . . . . 8
⊢ 0 <
1 |
| 8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 < 1) |
| 9 | | pellfundgt1 42894 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 1 < (PellFund‘𝐷)) |
| 10 | 5, 6, 2, 8, 9 | lttrd 11422 |
. . . . . 6
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 < (PellFund‘𝐷)) |
| 11 | 2, 10 | elrpd 13074 |
. . . . 5
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈
ℝ+) |
| 12 | 2, 11 | ltaddrpd 13110 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) < ((PellFund‘𝐷) + (PellFund‘𝐷))) |
| 13 | 2 | recnd 11289 |
. . . . 5
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℂ) |
| 14 | 13 | 2timesd 12509 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (2 · (PellFund‘𝐷)) = ((PellFund‘𝐷) + (PellFund‘𝐷))) |
| 15 | 12, 14 | breqtrrd 5171 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) < (2 · (PellFund‘𝐷))) |
| 16 | | pellfundglb 42896 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (2 · (PellFund‘𝐷)) ∈ ℝ ∧
(PellFund‘𝐷) < (2
· (PellFund‘𝐷))) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) |
| 17 | 4, 15, 16 | mpd3an23 1465 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) |
| 18 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (PellFund‘𝐷) ∈ ℝ) |
| 19 | | pell1qrss14 42879 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 20 | 19 | sselda 3983 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ (Pell14QR‘𝐷)) |
| 21 | | pell14qrre 42868 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ) |
| 22 | 20, 21 | syldan 591 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ ℝ) |
| 23 | 18, 22 | leloed 11404 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 ↔ ((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎))) |
| 24 | | simp-4l 783 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 25 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑎 ∈ (Pell1QR‘𝐷)) |
| 26 | | simplr 769 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 ∈ (Pell1QR‘𝐷)) |
| 27 | | simprr 773 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 < 𝑎) |
| 28 | 22 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑎 ∈ ℝ) |
| 29 | 4 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ∈
ℝ) |
| 30 | 19 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 31 | 30, 26 | sseldd 3984 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 ∈ (Pell14QR‘𝐷)) |
| 32 | | pell14qrre 42868 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 𝑏 ∈ ℝ) |
| 33 | 24, 31, 32 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 ∈ ℝ) |
| 34 | | remulcl 11240 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑏
∈ ℝ) → (2 · 𝑏) ∈ ℝ) |
| 35 | 1, 33, 34 | sylancr 587 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (2 · 𝑏) ∈ ℝ) |
| 36 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 < (2 · (PellFund‘𝐷))) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑎 < (2 · (PellFund‘𝐷))) |
| 38 | | simprl 771 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (PellFund‘𝐷) ≤ 𝑏) |
| 39 | 2 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ ℝ) |
| 40 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 2 ∈ ℝ) |
| 41 | | 2pos 12369 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 0 < 2) |
| 43 | | lemul2 12120 |
. . . . . . . . . . . 12
⊢
(((PellFund‘𝐷)
∈ ℝ ∧ 𝑏
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((PellFund‘𝐷) ≤
𝑏 ↔ (2 ·
(PellFund‘𝐷)) ≤ (2
· 𝑏))) |
| 44 | 39, 33, 40, 42, 43 | syl112anc 1376 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → ((PellFund‘𝐷) ≤ 𝑏 ↔ (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏))) |
| 45 | 38, 44 | mpbid 232 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)) |
| 46 | 28, 29, 35, 37, 45 | ltletrd 11421 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑎 < (2 · 𝑏)) |
| 47 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 48 | 19 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 49 | | simp2l 1200 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell1QR‘𝐷)) |
| 50 | 48, 49 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell14QR‘𝐷)) |
| 51 | | simp2r 1201 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell1QR‘𝐷)) |
| 52 | 48, 51 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell14QR‘𝐷)) |
| 53 | | pell14qrdivcl 42876 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) |
| 54 | 47, 50, 52, 53 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) |
| 55 | 47, 52, 32 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℝ) |
| 56 | 55 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℂ) |
| 57 | 56 | mullidd 11279 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (1 · 𝑏) = 𝑏) |
| 58 | | simp3l 1202 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 < 𝑎) |
| 59 | 57, 58 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (1 · 𝑏) < 𝑎) |
| 60 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 1 ∈ ℝ) |
| 61 | 47, 50, 21 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ ℝ) |
| 62 | | pell14qrgt0 42870 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 0 < 𝑏) |
| 63 | 47, 52, 62 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 0 < 𝑏) |
| 64 | | ltmuldiv 12141 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑎
∈ ℝ ∧ (𝑏
∈ ℝ ∧ 0 < 𝑏)) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏))) |
| 65 | 60, 61, 55, 63, 64 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏))) |
| 66 | 59, 65 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 1 < (𝑎 / 𝑏)) |
| 67 | | simp3r 1203 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 < (2 · 𝑏)) |
| 68 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 2 ∈ ℝ) |
| 69 | | ltdivmul2 12145 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 2 ∈
ℝ ∧ (𝑏 ∈
ℝ ∧ 0 < 𝑏))
→ ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏))) |
| 70 | 61, 68, 55, 63, 69 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏))) |
| 71 | 67, 70 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) < 2) |
| 72 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) < 2) |
| 73 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 74 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) |
| 75 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 1 < (𝑎 / 𝑏)) |
| 76 | | pell14qrgapw 42887 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷) ∧ 1 < (𝑎 / 𝑏)) → 2 < (𝑎 / 𝑏)) |
| 77 | 73, 74, 75, 76 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 2 < (𝑎 / 𝑏)) |
| 78 | | pell14qrre 42868 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ ℝ) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ ℝ) |
| 80 | | ltnsym 11359 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (𝑎 /
𝑏) ∈ ℝ) →
(2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2)) |
| 81 | 1, 79, 80 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2)) |
| 82 | 77, 81 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → ¬ (𝑎 / 𝑏) < 2) |
| 83 | 72, 82 | pm2.21dd 195 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |
| 84 | 47, 54, 66, 71, 83 | syl22anc 839 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |
| 85 | 24, 25, 26, 27, 46, 84 | syl122anc 1381 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |
| 86 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 87 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 ∈ ℝ) |
| 88 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) →
(PellFund‘𝐷) <
𝑎) |
| 89 | | pellfundglb 42896 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ ℝ ∧ (PellFund‘𝐷) < 𝑎) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) |
| 90 | 86, 87, 88, 89 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) → ∃𝑏 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) |
| 91 | 85, 90 | r19.29a 3162 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) →
(PellFund‘𝐷) ∈
(Pell1QR‘𝐷)) |
| 92 | 91 | exp32 420 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) < 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
| 93 | | simp2 1138 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) = 𝑎) |
| 94 | | simp1r 1199 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → 𝑎 ∈ (Pell1QR‘𝐷)) |
| 95 | 93, 94 | eqeltrd 2841 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |
| 96 | 95 | 3exp 1120 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) = 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
| 97 | 92, 96 | jaod 860 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎) → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
| 98 | 23, 97 | sylbid 240 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
| 99 | 98 | impd 410 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))) |
| 100 | 99 | rexlimdva 3155 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))) |
| 101 | 17, 100 | mpd 15 |
1
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |