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 36443

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 36433	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))))
2		simp-4r 803	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ)
3		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑎 → (𝑐 + ((√‘𝐷) · 𝑏)) = (𝑎 + ((√‘𝐷) · 𝑏)))
4	3	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑎 → (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ↔ 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏))))
5		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑎 → (𝑐↑2) = (𝑎↑2))
6	5	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑎 → ((𝑐↑2) − (𝐷 · (𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2))))
7	6	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑎 → (((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1))
8	4, 7	anbi12d 743	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑎 → ((𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))
9	8	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑎 → (∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1) ↔ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)))
10	9	rspcev 3282	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℕ₀ ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))
11	10	adantll 746	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))
12		elpell14qr 36431	. . . . . . . . . 10 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))))
13	12	ad4antr 764	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑏 ∈ ℤ (𝐴 = (𝑐 + ((√‘𝐷) · 𝑏)) ∧ ((𝑐↑2) − (𝐷 · (𝑏↑2))) = 1))))
14	2, 11, 13	mpbir2and 959	. . . . . . . 8 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ (Pell14QR‘𝐷))
15	14	orcd 406	. . . . . . 7 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ 𝑎 ∈ ℕ₀) ∧ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
16	15	exp31 628	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ₀ → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))))
17		simp-5r 805	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 ∈ ℝ)
18	17	renegcld 10336	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ ℝ)
19		simpllr 795	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑎 ∈ ℕ₀)
20		znegcl 11289	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ ℤ → -𝑏 ∈ ℤ)
21	20	ad2antlr 759	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝑏 ∈ ℤ)
22		simprl 790	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)))
23	22	negeqd 10154	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = -(𝑎 + ((√‘𝐷) · 𝑏)))
24		zcn 11259	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℤ → 𝑎 ∈ ℂ)
25	24	ad4antlr 765	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑎 ∈ ℂ)
26		eldifi 3694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → 𝐷 ∈ ℕ)
27	26	nncnd 10913	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → 𝐷 ∈ ℂ)
28	27	ad5antr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝐷 ∈ ℂ)
29	28	sqrtcld 14024	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (√‘𝐷) ∈ ℂ)
30		zcn 11259	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ℤ → 𝑏 ∈ ℂ)
31	30	ad2antlr 759	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → 𝑏 ∈ ℂ)
32	29, 31	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((√‘𝐷) · 𝑏) ∈ ℂ)
33	25, 32	negdid 10284	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -(𝑎 + ((√‘𝐷) · 𝑏)) = (-𝑎 + -((√‘𝐷) · 𝑏)))
34		mulneg2 10346	. . . . . . . . . . . . . . . 16 ⊢ (((√‘𝐷) ∈ ℂ ∧ 𝑏 ∈ ℂ) → ((√‘𝐷) · -𝑏) = -((√‘𝐷) · 𝑏))
35	34	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ (((√‘𝐷) ∈ ℂ ∧ 𝑏 ∈ ℂ) → -((√‘𝐷) · 𝑏) = ((√‘𝐷) · -𝑏))
36	29, 31, 35	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -((√‘𝐷) · 𝑏) = ((√‘𝐷) · -𝑏))
37	36	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎 + -((√‘𝐷) · 𝑏)) = (-𝑎 + ((√‘𝐷) · -𝑏)))
38	23, 33, 37	3eqtrd 2648	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)))
39		sqneg 12785	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ ℂ → (-𝑎↑2) = (𝑎↑2))
40	25, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑎↑2) = (𝑎↑2))
41		sqneg 12785	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ ℂ → (-𝑏↑2) = (𝑏↑2))
42	31, 41	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝑏↑2) = (𝑏↑2))
43	42	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐷 · (-𝑏↑2)) = (𝐷 · (𝑏↑2)))
44	40, 43	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = ((𝑎↑2) − (𝐷 · (𝑏↑2))))
45		simprr 792	. . . . . . . . . . . . 13 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
46	44, 45	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)
47		oveq1 6556	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = -𝑎 → (𝑐 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · 𝑑)))
48	47	eqeq2d 2620	. . . . . . . . . . . . . 14 ⊢ (𝑐 = -𝑎 → (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑))))
49		oveq1 6556	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = -𝑎 → (𝑐↑2) = (-𝑎↑2))
50	49	oveq1d 6564	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = -𝑎 → ((𝑐↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (𝑑↑2))))
51	50	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑐 = -𝑎 → (((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1))
52	48, 51	anbi12d 743	. . . . . . . . . . . . 13 ⊢ (𝑐 = -𝑎 → ((-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1)))
53		oveq2 6557	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = -𝑏 → ((√‘𝐷) · 𝑑) = ((√‘𝐷) · -𝑏))
54	53	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = -𝑏 → (-𝑎 + ((√‘𝐷) · 𝑑)) = (-𝑎 + ((√‘𝐷) · -𝑏)))
55	54	eqeq2d 2620	. . . . . . . . . . . . . 14 ⊢ (𝑑 = -𝑏 → (-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ↔ -𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏))))
56		oveq1 6556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = -𝑏 → (𝑑↑2) = (-𝑏↑2))
57	56	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = -𝑏 → (𝐷 · (𝑑↑2)) = (𝐷 · (-𝑏↑2)))
58	57	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = -𝑏 → ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = ((-𝑎↑2) − (𝐷 · (-𝑏↑2))))
59	58	eqeq1d 2612	. . . . . . . . . . . . . 14 ⊢ (𝑑 = -𝑏 → (((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1 ↔ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1))
60	55, 59	anbi12d 743	. . . . . . . . . . . . 13 ⊢ (𝑑 = -𝑏 → ((-𝐴 = (-𝑎 + ((√‘𝐷) · 𝑑)) ∧ ((-𝑎↑2) − (𝐷 · (𝑑↑2))) = 1) ↔ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)))
61	52, 60	rspc2ev 3295	. . . . . . . . . . . 12 ⊢ ((-𝑎 ∈ ℕ₀ ∧ -𝑏 ∈ ℤ ∧ (-𝐴 = (-𝑎 + ((√‘𝐷) · -𝑏)) ∧ ((-𝑎↑2) − (𝐷 · (-𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))
62	19, 21, 38, 46, 61	syl112anc 1322	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))
63		elpell14qr 36431	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
64	63	ad5antr 766	. . . . . . . . . . 11 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (-𝐴 ∈ (Pell14QR‘𝐷) ↔ (-𝐴 ∈ ℝ ∧ ∃𝑐 ∈ ℕ₀ ∃𝑑 ∈ ℤ (-𝐴 = (𝑐 + ((√‘𝐷) · 𝑑)) ∧ ((𝑐↑2) − (𝐷 · (𝑑↑2))) = 1))))
65	18, 62, 64	mpbir2and 959	. . . . . . . . . 10 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → -𝐴 ∈ (Pell14QR‘𝐷))
66	65	olcd 407	. . . . . . . . 9 ⊢ ((((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) ∧ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
67	66	ex 449	. . . . . . . 8 ⊢ (((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) ∧ 𝑏 ∈ ℤ) → ((𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
68	67	rexlimdva 3013	. . . . . . 7 ⊢ ((((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) ∧ -𝑎 ∈ ℕ₀) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
69	68	ex 449	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (-𝑎 ∈ ℕ₀ → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))))
70		elznn0 11269	. . . . . . . 8 ⊢ (𝑎 ∈ ℤ ↔ (𝑎 ∈ ℝ ∧ (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀)))
71	70	simprbi 479	. . . . . . 7 ⊢ (𝑎 ∈ ℤ → (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀))
72	71	adantl 481	. . . . . 6 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (𝑎 ∈ ℕ₀ ∨ -𝑎 ∈ ℕ₀))
73	16, 69, 72	mpjaod 395	. . . . 5 ⊢ (((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) ∧ 𝑎 ∈ ℤ) → (∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
74	73	rexlimdva 3013	. . . 4 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ ℝ) → (∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
75	74	expimpd 627	. . 3 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → ((𝐴 ∈ ℝ ∧ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑎 + ((√‘𝐷) · 𝑏)) ∧ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
76	1, 75	sylbid 229	. 2 ⊢ (𝐷 ∈ (ℕ ∖ ◻_NN) → (𝐴 ∈ (Pell1234QR‘𝐷) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))))
77	76	imp 444	1 ⊢ ((𝐷 ∈ (ℕ ∖ ◻_NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∃wrex 2897 ∖ cdif 3537 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 ℝcr 9814 1c1 9816 + caddc 9818 · cmul 9820 − cmin 10145 -cneg 10146 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 ℤcz 11254 ↑cexp 12722 √csqrt 13821 ◻_NNcsquarenn 36418 Pell1234QRcpell1234qr 36420 Pell14QRcpell14qr 36421

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-sup 8231 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-rp 11709 df-seq 12664 df-exp 12723 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-pell14qr 36425 df-pell1234qr 36426

This theorem is referenced by: elpell14qr2 36444

W3C validator