Step | Hyp | Ref
| Expression |
1 | | elpell1234qr 40285 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))) |
2 | | simp-4r 784 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ0) ∧
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ) |
3 | | oveq1 7189 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑎 → (𝑐 + ((√‘𝐷) · 𝑏)) = (𝑎 + ((√‘𝐷) · 𝑏))) |
4 | 3 | eqeq2d 2750 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ↔ 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))) |
5 | | oveq1 7189 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑎 → (𝑐↑2) = (𝑎↑2)) |
6 | 5 | oveq1d 7197 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑎 → ((𝑐↑2) − (𝐷 · (𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2)))) |
7 | 6 | eqeq1d 2741 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑎 → (((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) |
8 | 4, 7 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑎 → ((𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))) |
9 | 8 | rexbidv 3208 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑎 → (∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))) |
10 | 9 | rspcev 3529 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ ℕ0
∧ ∃𝑏 ∈
ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1)) |
11 | 10 | adantll 714 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ0) ∧
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1)) |
12 | | elpell14qr 40283 |
. . . . . . . . . 10
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1)))) |
13 | 12 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ0) ∧
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ0
∃𝑏 ∈ ℤ
(𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1)))) |
14 | 2, 11, 13 | mpbir2and 713 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ0) ∧
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ (Pell14QR‘𝐷)) |
15 | 14 | orcd 872 |
. . . . . . 7
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ0) ∧
∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))) |
16 | 15 | exp31 423 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ0 →
(∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))) |
17 | | simp-5r 786 |
. . . . . . . . . . . 12
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ) |
18 | 17 | renegcld 11157 |
. . . . . . . . . . 11
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ ℝ) |
19 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑎 ∈ ℕ0) |
20 | | znegcl 12110 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ ℤ → -𝑏 ∈
ℤ) |
21 | 20 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑏 ∈ ℤ) |
22 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏))) |
23 | 22 | negeqd 10970 |
. . . . . . . . . . . . 13
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = -(𝑎 + ((√‘𝐷) · 𝑏))) |
24 | | zcn 12079 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℤ → 𝑎 ∈
ℂ) |
25 | 24 | ad4antlr 733 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑎 ∈ ℂ) |
26 | | eldifi 4027 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℕ) |
27 | 26 | nncnd 11744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → 𝐷 ∈ ℂ) |
28 | 27 | ad5antr 734 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐷 ∈ ℂ) |
29 | 28 | sqrtcld 14899 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (√‘𝐷) ∈
ℂ) |
30 | | zcn 12079 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
31 | 30 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑏 ∈ ℂ) |
32 | 29, 31 | mulcld 10751 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((√‘𝐷) · 𝑏) ∈ ℂ) |
33 | 25, 32 | negdid 11100 |
. . . . . . . . . . . . 13
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -(𝑎 + ((√‘𝐷) · 𝑏)) = (-𝑎 + -((√‘𝐷) · 𝑏))) |
34 | | mulneg2 11167 |
. . . . . . . . . . . . . . . 16
⊢
(((√‘𝐷)
∈ ℂ ∧ 𝑏
∈ ℂ) → ((√‘𝐷) · -𝑏) = -((√‘𝐷) · 𝑏)) |
35 | 34 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢
(((√‘𝐷)
∈ ℂ ∧ 𝑏
∈ ℂ) → -((√‘𝐷) · 𝑏) = ((√‘𝐷) · -𝑏)) |
36 | 29, 31, 35 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) →
-((√‘𝐷)
· 𝑏) =
((√‘𝐷) ·
-𝑏)) |
37 | 36 | oveq2d 7198 |
. . . . . . . . . . . . 13
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎 + -((√‘𝐷) · 𝑏)) = (-𝑎 + ((√‘𝐷) · -𝑏))) |
38 | 23, 33, 37 | 3eqtrd 2778 |
. . . . . . . . . . . 12
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏))) |
39 | | sqneg 13586 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℂ → (-𝑎↑2) = (𝑎↑2)) |
40 | 25, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎↑2) = (𝑎↑2)) |
41 | | sqneg 13586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ ℂ → (-𝑏↑2) = (𝑏↑2)) |
42 | 31, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑏↑2) = (𝑏↑2)) |
43 | 42 | oveq2d 7198 |
. . . . . . . . . . . . . 14
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐷 · (-𝑏↑2)) = (𝐷 · (𝑏↑2))) |
44 | 40, 43 | oveq12d 7200 |
. . . . . . . . . . . . 13
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2)))) |
45 | | simprr 773 |
. . . . . . . . . . . . 13
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) |
46 | 44, 45 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1) |
47 | | oveq1 7189 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = -𝑎 → (𝑐 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · 𝑑))) |
48 | 47 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = -𝑎 → (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)))) |
49 | | oveq1 7189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = -𝑎 → (𝑐↑2) = (-𝑎↑2)) |
50 | 49 | oveq1d 7197 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = -𝑎 → ((𝑐↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (𝑑↑2)))) |
51 | 50 | eqeq1d 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = -𝑎 → (((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1)) |
52 | 48, 51 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑐 = -𝑎 → ((-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1))) |
53 | | oveq2 7190 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = -𝑏 → ((√‘𝐷) · 𝑑) = ((√‘𝐷) · -𝑏)) |
54 | 53 | oveq2d 7198 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = -𝑏 → (-𝑎 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · -𝑏))) |
55 | 54 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = -𝑏 → (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)))) |
56 | | oveq1 7189 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = -𝑏 → (𝑑↑2) = (-𝑏↑2)) |
57 | 56 | oveq2d 7198 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = -𝑏 → (𝐷 · (𝑑↑2)) = (𝐷 · (-𝑏↑2))) |
58 | 57 | oveq2d 7198 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 = -𝑏 → ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (-𝑏↑2)))) |
59 | 58 | eqeq1d 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = -𝑏 → (((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)) |
60 | 55, 59 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑑 = -𝑏 → ((-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1))) |
61 | 52, 60 | rspc2ev 3541 |
. . . . . . . . . . . 12
⊢ ((-𝑎 ∈ ℕ0
∧ -𝑏 ∈ ℤ
∧ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ0
∃𝑑 ∈ ℤ
(-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) |
62 | 19, 21, 38, 46, 61 | syl112anc 1375 |
. . . . . . . . . . 11
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ0
∃𝑑 ∈ ℤ
(-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)) |
63 | | elpell14qr 40283 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ0
∃𝑑 ∈ ℤ
(-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)))) |
64 | 63 | ad5antr 734 |
. . . . . . . . . . 11
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ0
∃𝑑 ∈ ℤ
(-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1)))) |
65 | 18, 62, 64 | mpbir2and 713 |
. . . . . . . . . 10
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ (Pell14QR‘𝐷)) |
66 | 65 | olcd 873 |
. . . . . . . . 9
⊢
((((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))) |
67 | 66 | ex 416 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
68 | 67 | rexlimdva 3195 |
. . . . . . 7
⊢ ((((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ0) →
(∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
69 | 68 | ex 416 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ0 →
(∃𝑏 ∈ ℤ
(𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))) |
70 | | elznn0 12089 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 ∈ ℕ0 ∨
-𝑎 ∈
ℕ0))) |
71 | 70 | simprbi 500 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → (𝑎 ∈ ℕ0 ∨
-𝑎 ∈
ℕ0)) |
72 | 71 | adantl 485 |
. . . . . 6
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ0 ∨ -𝑎 ∈
ℕ0)) |
73 | 16, 69, 72 | mpjaod 859 |
. . . . 5
⊢ (((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
74 | 73 | rexlimdva 3195 |
. . . 4
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
75 | 74 | expimpd 457 |
. . 3
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
76 | 1, 75 | sylbid 243 |
. 2
⊢ (𝐷 ∈ (ℕ ∖
◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))) |
77 | 76 | imp 410 |
1
⊢ ((𝐷 ∈ (ℕ ∖
◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))) |