Step | Hyp | Ref
| Expression |
1 | | 2re 11904 |
. . . 4
⊢ 2 ∈
ℝ |
2 | | pellfundre 40406 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℝ) |
3 | | remulcl 10814 |
. . . 4
⊢ ((2
∈ ℝ ∧ (PellFund‘𝐷) ∈ ℝ) → (2 ·
(PellFund‘𝐷)) ∈
ℝ) |
4 | 1, 2, 3 | sylancr 590 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (2 · (PellFund‘𝐷)) ∈
ℝ) |
5 | | 0red 10836 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 ∈ ℝ) |
6 | | 1red 10834 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 1 ∈ ℝ) |
7 | | 0lt1 11354 |
. . . . . . . 8
⊢ 0 <
1 |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 < 1) |
9 | | pellfundgt1 40408 |
. . . . . . 7
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 1 < (PellFund‘𝐷)) |
10 | 5, 6, 2, 8, 9 | lttrd 10993 |
. . . . . 6
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 0 < (PellFund‘𝐷)) |
11 | 2, 10 | elrpd 12625 |
. . . . 5
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈
ℝ+) |
12 | 2, 11 | ltaddrpd 12661 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) < ((PellFund‘𝐷) + (PellFund‘𝐷))) |
13 | 2 | recnd 10861 |
. . . . 5
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ ℂ) |
14 | 13 | 2timesd 12073 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (2 · (PellFund‘𝐷)) = ((PellFund‘𝐷) + (PellFund‘𝐷))) |
15 | 12, 14 | breqtrrd 5081 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) < (2 · (PellFund‘𝐷))) |
16 | | pellfundglb 40410 |
. . 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 484 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (PellFund‘𝐷) ∈ ℝ) |
19 | | pell1qrss14 40393 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
20 | 19 | sselda 3901 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ (Pell14QR‘𝐷)) |
21 | | pell14qrre 40382 |
. . . . . . 7
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷)) → 𝑎 ∈ ℝ) |
22 | 20, 21 | syldan 594 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → 𝑎 ∈ ℝ) |
23 | 18, 22 | leloed 10975 |
. . . . 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 3902 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 ∈ (Pell14QR‘𝐷)) |
32 | | pell14qrre 40382 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 𝑏 ∈ ℝ) |
33 | 24, 31, 32 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑏 ∈ ℝ) |
34 | | remulcl 10814 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝑏
∈ ℝ) → (2 · 𝑏) ∈ ℝ) |
35 | 1, 33, 34 | sylancr 590 |
. . . . . . . . . 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 11933 |
. . . . . . . . . . . . 13
⊢ 0 <
2 |
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 0 < 2) |
43 | | lemul2 11685 |
. . . . . . . . . . . 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 235 |
. . . . . . . . . 10
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → (2 · (PellFund‘𝐷)) ≤ (2 · 𝑏)) |
46 | 28, 29, 35, 37, 45 | ltletrd 10992 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) ≤ 𝑏 ∧ 𝑏 < 𝑎)) → 𝑎 < (2 · 𝑏)) |
47 | | simp1 1138 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝐷 ∈ (ℕ ∖
◻NN)) |
48 | 19 | 3ad2ant1 1135 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
49 | | simp2l 1201 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell1QR‘𝐷)) |
50 | 48, 49 | sseldd 3902 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ (Pell14QR‘𝐷)) |
51 | | simp2r 1202 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell1QR‘𝐷)) |
52 | 48, 51 | sseldd 3902 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ (Pell14QR‘𝐷)) |
53 | | pell14qrdivcl 40390 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell14QR‘𝐷) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) |
54 | 47, 50, 52, 53 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) |
55 | 47, 52, 32 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℝ) |
56 | 55 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 ∈ ℂ) |
57 | 56 | mulid2d 10851 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (1 · 𝑏) = 𝑏) |
58 | | simp3l 1203 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑏 < 𝑎) |
59 | 57, 58 | eqbrtrd 5075 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → (1 · 𝑏) < 𝑎) |
60 | | 1red 10834 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 1 ∈ ℝ) |
61 | 47, 50, 21 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 ∈ ℝ) |
62 | | pell14qrgt0 40384 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑏 ∈ (Pell14QR‘𝐷)) → 0 < 𝑏) |
63 | 47, 52, 62 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 0 < 𝑏) |
64 | | ltmuldiv 11705 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ ∧ 𝑎
∈ ℝ ∧ (𝑏
∈ ℝ ∧ 0 < 𝑏)) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏))) |
65 | 60, 61, 55, 63, 64 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → ((1 · 𝑏) < 𝑎 ↔ 1 < (𝑎 / 𝑏))) |
66 | 59, 65 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 1 < (𝑎 / 𝑏)) |
67 | | simp3r 1204 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 𝑎 < (2 · 𝑏)) |
68 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → 2 ∈ ℝ) |
69 | | ltdivmul2 11709 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℝ ∧ 2 ∈
ℝ ∧ (𝑏 ∈
ℝ ∧ 0 < 𝑏))
→ ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏))) |
70 | 61, 68, 55, 63, 69 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 ∈ (Pell1QR‘𝐷) ∧ 𝑏 ∈ (Pell1QR‘𝐷)) ∧ (𝑏 < 𝑎 ∧ 𝑎 < (2 · 𝑏))) → ((𝑎 / 𝑏) < 2 ↔ 𝑎 < (2 · 𝑏))) |
71 | 67, 70 | mpbird 260 |
. . . . . . . . . 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 40401 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷) ∧ 1 < (𝑎 / 𝑏)) → 2 < (𝑎 / 𝑏)) |
77 | 73, 74, 75, 76 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → 2 < (𝑎 / 𝑏)) |
78 | | pell14qrre 40382 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) → (𝑎 / 𝑏) ∈ ℝ) |
79 | 78 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (𝑎 / 𝑏) ∈ ℝ) |
80 | | ltnsym 10930 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (𝑎 /
𝑏) ∈ ℝ) →
(2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2)) |
81 | 1, 79, 80 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → (2 < (𝑎 / 𝑏) → ¬ (𝑎 / 𝑏) < 2)) |
82 | 77, 81 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝑎 / 𝑏) ∈ (Pell14QR‘𝐷)) ∧ (1 < (𝑎 / 𝑏) ∧ (𝑎 / 𝑏) < 2)) → ¬ (𝑎 / 𝑏) < 2) |
83 | 72, 82 | pm2.21dd 198 |
. . . . . . . . . 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 484 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) → 𝑎 ∈ ℝ) |
88 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) →
(PellFund‘𝐷) <
𝑎) |
89 | | pellfundglb 40410 |
. . . . . . . . 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 3208 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ ((PellFund‘𝐷) < 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷)))) →
(PellFund‘𝐷) ∈
(Pell1QR‘𝐷)) |
92 | 91 | exp32 424 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) < 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
93 | | simp2 1139 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) = 𝑎) |
94 | | simp1r 1200 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → 𝑎 ∈ (Pell1QR‘𝐷)) |
95 | 93, 94 | eqeltrd 2838 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) ∧ (PellFund‘𝐷) = 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |
96 | 95 | 3exp 1121 |
. . . . . 6
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) = 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
97 | 92, 96 | jaod 859 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) < 𝑎 ∨ (PellFund‘𝐷) = 𝑎) → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
98 | 23, 97 | sylbid 243 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → ((PellFund‘𝐷) ≤ 𝑎 → (𝑎 < (2 · (PellFund‘𝐷)) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)))) |
99 | 98 | impd 414 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝑎 ∈ (Pell1QR‘𝐷)) → (((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))) |
100 | 99 | rexlimdva 3203 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (∃𝑎 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑎 ∧ 𝑎 < (2 · (PellFund‘𝐷))) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))) |
101 | 17, 100 | mpd 15 |
1
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) |