Proof of Theorem elpell1qr2
| Step | Hyp | Ref
| Expression |
| 1 | | pell1qrss14 42879 |
. . . 4
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) |
| 2 | 1 | sselda 3983 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 𝐴 ∈ (Pell14QR‘𝐷)) |
| 3 | | pell1qrge1 42881 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) |
| 4 | 2, 3 | jca 511 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴)) |
| 5 | | 1red 11262 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 1 ∈ ℝ) |
| 6 | | pell14qrre 42868 |
. . . . 5
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) |
| 7 | 5, 6 | leloed 11404 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 ≤ 𝐴 ↔ (1 < 𝐴 ∨ 1 = 𝐴))) |
| 8 | 5, 6 | ltnled 11408 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 < 𝐴 ↔ ¬ 𝐴 ≤ 1)) |
| 9 | 8 | biimpa 476 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → ¬ 𝐴 ≤ 1) |
| 10 | | 1div1e1 11958 |
. . . . . . . . . . . . 13
⊢ (1 / 1) =
1 |
| 11 | 10 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ 1 = (1 /
1) |
| 12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 1 = (1 / 1)) |
| 13 | 12 | breq2d 5155 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → (𝐴 ≤ 1 ↔ 𝐴 ≤ (1 / 1))) |
| 14 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) |
| 15 | | pell14qrgt0 42870 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 0 < 𝐴) |
| 17 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 1 ∈ ℝ) |
| 18 | | 0lt1 11785 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
| 19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 0 < 1) |
| 20 | | lerec2 12156 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 <
𝐴) ∧ (1 ∈ ℝ
∧ 0 < 1)) → (𝐴
≤ (1 / 1) ↔ 1 ≤ (1 / 𝐴))) |
| 21 | 14, 16, 17, 19, 20 | syl22anc 839 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → (𝐴 ≤ (1 / 1) ↔ 1 ≤ (1 / 𝐴))) |
| 22 | 13, 21 | bitrd 279 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → (𝐴 ≤ 1 ↔ 1 ≤ (1 / 𝐴))) |
| 23 | 9, 22 | mtbid 324 |
. . . . . . . 8
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → ¬ 1 ≤ (1 / 𝐴)) |
| 24 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) ∧ (1 / 𝐴) ∈ (Pell1QR‘𝐷)) → 𝐷 ∈ (ℕ ∖
◻NN)) |
| 25 | | pell1qrge1 42881 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (1 / 𝐴) ∈ (Pell1QR‘𝐷)) → 1 ≤ (1 / 𝐴)) |
| 26 | 24, 25 | sylancom 588 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) ∧ (1 / 𝐴) ∈ (Pell1QR‘𝐷)) → 1 ≤ (1 / 𝐴)) |
| 27 | 23, 26 | mtand 816 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → ¬ (1 / 𝐴) ∈ (Pell1QR‘𝐷)) |
| 28 | | pell14qrdich 42880 |
. . . . . . . 8
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷))) |
| 29 | 28 | adantr 480 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷))) |
| 30 | | orel2 891 |
. . . . . . 7
⊢ (¬ (1
/ 𝐴) ∈
(Pell1QR‘𝐷) →
((𝐴 ∈
(Pell1QR‘𝐷) ∨ (1 /
𝐴) ∈
(Pell1QR‘𝐷)) →
𝐴 ∈
(Pell1QR‘𝐷))) |
| 31 | 27, 29, 30 | sylc 65 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 < 𝐴) → 𝐴 ∈ (Pell1QR‘𝐷)) |
| 32 | | simpr 484 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 = 𝐴) → 1 = 𝐴) |
| 33 | | pell1qr1 42882 |
. . . . . . . 8
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 1 ∈ (Pell1QR‘𝐷)) |
| 34 | 33 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 = 𝐴) → 1 ∈ (Pell1QR‘𝐷)) |
| 35 | 32, 34 | eqeltrrd 2842 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ 1 = 𝐴) → 𝐴 ∈ (Pell1QR‘𝐷)) |
| 36 | 31, 35 | jaodan 960 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) ∧ (1 < 𝐴 ∨ 1 = 𝐴)) → 𝐴 ∈ (Pell1QR‘𝐷)) |
| 37 | 36 | ex 412 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ((1 < 𝐴 ∨ 1 = 𝐴) → 𝐴 ∈ (Pell1QR‘𝐷))) |
| 38 | 7, 37 | sylbid 240 |
. . 3
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 ≤ 𝐴 → 𝐴 ∈ (Pell1QR‘𝐷))) |
| 39 | 38 | impr 454 |
. 2
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴)) → 𝐴 ∈ (Pell1QR‘𝐷)) |
| 40 | 4, 39 | impbida 801 |
1
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴))) |