pell1234qrdich - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pell1234qrdich		Structured version Visualization version GIF version

Theorem pell1234qrdich 42346

Description: A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.)

**Assertion**
Ref	Expression
pell1234qrdich	⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))

Proof of Theorem pell1234qrdich Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpell1234qr 42336	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))))
2		simp-4r 782	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ)
3		oveq1 7424	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑎 → (𝑐 + ((√‘𝐷) · 𝑏)) = (𝑎 + ((√‘𝐷) · 𝑏)))
4	3	eqeq2d 2736	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑎 → (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ↔ 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏))))
5		oveq1 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑎 → (𝑐↑2) = (𝑎↑2))
6	5	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑎 → ((𝑐↑2) − (𝐷 · (𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2))))
7	6	eqeq1d 2727	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑎 → (((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))
8	4, 7	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑎 → ((𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))
9	8	rexbidv 3169	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑎 → (∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))
10	9	rspcev 3607	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℕ₀ ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))
11	10	adantll 712	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))
12		elpell14qr 42334	. . . . . . . . . 10 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))))
13	12	ad4antr 730	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))))
14	2, 11, 13	mpbir2and 711	. . . . . . . 8 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ (Pell14QR‘𝐷))
15	14	orcd 871	. . . . . . 7 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
16	15	exp31 418	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ₀ → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))))
17		simp-5r 784	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ)
18	17	renegcld 11671	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ ℝ)
19		simpllr 774	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑎 ∈ ℕ₀)
20		znegcl 12627	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ℤ → -𝑏 ∈ ℤ)
21	20	ad2antlr 725	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑏 ∈ ℤ)
22		simprl 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))
23	22	negeqd 11484	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = -(𝑎 + ((√‘𝐷) · 𝑏)))
24		zcn 12593	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
25	24	ad4antlr 731	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑎 ∈ ℂ)
26		eldifi 4124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → 𝐷 ∈ ℕ)
27	26	nncnd 12258	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → 𝐷 ∈ ℂ)
28	27	ad5antr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐷 ∈ ℂ)
29	28	sqrtcld 15416	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (√‘𝐷) ∈ ℂ)
30		zcn 12593	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
31	30	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑏 ∈ ℂ)
32	29, 31	mulcld 11264	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((√‘𝐷) · 𝑏) ∈ ℂ)
33	25, 32	negdid 11614	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -(𝑎 + ((√‘𝐷) · 𝑏)) = (-𝑎 + -((√‘𝐷) · 𝑏)))
34		mulneg2 11681	. . . . . . . . . . . . . . . 16 ⊢ (((√‘𝐷) ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((√‘𝐷) · -𝑏) = -((√‘𝐷) · 𝑏))
35	34	eqcomd 2731	. . . . . . . . . . . . . . 15 ⊢ (((√‘𝐷) ∈ ℂ ∧ 𝑏 ∈ ℂ) → -((√‘𝐷) · 𝑏) = ((√‘𝐷) · -𝑏))
36	29, 31, 35	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -((√‘𝐷) · 𝑏) = ((√‘𝐷) · -𝑏))
37	36	oveq2d 7433	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎 + -((√‘𝐷) · 𝑏)) = (-𝑎 + ((√‘𝐷) · -𝑏)))
38	23, 33, 37	3eqtrd 2769	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)))
39		sqneg 14112	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℂ → (-𝑎↑2) = (𝑎↑2))
40	25, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎↑2) = (𝑎↑2))
41		sqneg 14112	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ℂ → (-𝑏↑2) = (𝑏↑2))
42	31, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑏↑2) = (𝑏↑2))
43	42	oveq2d 7433	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐷 · (-𝑏↑2)) = (𝐷 · (𝑏↑2)))
44	40, 43	oveq12d 7435	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2))))
45		simprr 771	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
46	44, 45	eqtrd 2765	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)
47		oveq1 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = -𝑎 → (𝑐 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · 𝑑)))
48	47	eqeq2d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑐 = -𝑎 → (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑))))
49		oveq1 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = -𝑎 → (𝑐↑2) = (-𝑎↑2))
50	49	oveq1d 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = -𝑎 → ((𝑐↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (𝑑↑2))))
51	50	eqeq1d 2727	. . . . . . . . . . . . . 14 ⊢ (𝑐 = -𝑎 → (((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1))
52	48, 51	anbi12d 630	. . . . . . . . . . . . 13 ⊢ (𝑐 = -𝑎 → ((-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1)))
53		oveq2 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = -𝑏 → ((√‘𝐷) · 𝑑) = ((√‘𝐷) · -𝑏))
54	53	oveq2d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = -𝑏 → (-𝑎 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · -𝑏)))
55	54	eqeq2d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑑 = -𝑏 → (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏))))
56		oveq1 7424	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = -𝑏 → (𝑑↑2) = (-𝑏↑2))
57	56	oveq2d 7433	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = -𝑏 → (𝐷 · (𝑑↑2)) = (𝐷 · (-𝑏↑2)))
58	57	oveq2d 7433	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = -𝑏 → ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (-𝑏↑2))))
59	58	eqeq1d 2727	. . . . . . . . . . . . . 14 ⊢ (𝑑 = -𝑏 → (((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1))
60	55, 59	anbi12d 630	. . . . . . . . . . . . 13 ⊢ (𝑑 = -𝑏 → ((-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)))
61	52, 60	rspc2ev 3620	. . . . . . . . . . . 12 ⊢ ((-𝑎 ∈ ℕ₀ ∧ -𝑏 ∈ ℤ ∧ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))
62	19, 21, 38, 46, 61	syl112anc 1371	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))
63		elpell14qr 42334	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
64	63	ad5antr 732	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
65	18, 62, 64	mpbir2and 711	. . . . . . . . . 10 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ (Pell14QR‘𝐷))
66	65	olcd 872	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
67	66	ex 411	. . . . . . . 8 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
68	67	rexlimdva 3145	. . . . . . 7 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
69	68	ex 411	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ₀ → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))))
70		elznn0 12603	. . . . . . . 8 ⊢ (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀)))
71	70	simprbi 495	. . . . . . 7 ⊢ (𝑎 ∈ ℤ → (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀))
72	71	adantl 480	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀))
73	16, 69, 72	mpjaod 858	. . . . 5 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
74	73	rexlimdva 3145	. . . 4 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
75	74	expimpd 452	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
76	1, 75	sylbid 239	. 2 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell1234QR‘𝐷) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
77	76	imp 405	1 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1533 ∈ wcel 2098 ∃wrex 3060 ∖ cdif 3942 ‘cfv 6547 (class class class)co 7417 ℂcc 11136 ℝcr 11137 1c1 11139 + caddc 11141 · cmul 11143 − cmin 11474 -cneg 11475 ℕcn 12242 2c2 12297 ℕ₀cn0 12502 ℤcz 12588 ↑cexp 14058 √csqrt 15212 ◻_NNcsquarenn 42321 Pell1234QRcpell1234qr 42323 Pell14QRcpell14qr 42324

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7870 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8723 df-en 8963 df-dom 8964 df-sdom 8965 df-sup 9465 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-n0 12503 df-z 12589 df-uz 12853 df-rp 13007 df-seq 13999 df-exp 14059 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-pell14qr 42328 df-pell1234qr 42329

This theorem is referenced by: elpell14qr2 42347

W3C validator