pell1234qrdich

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

		Ref	Expression
	Assertion	pell1234qrdich	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))$

Proof

Step	Hyp	Ref	Expression
1		elpell1234qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1234QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
2		simp-4r	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land a \in ℕ_{0}) \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \in ℝ$
3		oveq1	$⊢ c = a \to c + \sqrt{D} b = a + \sqrt{D} b$
4	3	eqeq2d	$⊢ c = a \to (A = c + \sqrt{D} b \leftrightarrow A = a + \sqrt{D} b)$
5		oveq1	$⊢ c = a \to c^{2} = a^{2}$
6	5	oveq1d	$⊢ c = a \to c^{2} - D b^{2} = a^{2} - D b^{2}$
7	6	eqeq1d	$⊢ c = a \to (c^{2} - D b^{2} = 1 \leftrightarrow a^{2} - D b^{2} = 1)$
8	4 7	anbi12d	$⊢ c = a \to ((A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1) \leftrightarrow (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1))$
9	8	rexbidv	$⊢ c = a \to (\exists b \in ℤ (A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1) \leftrightarrow \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1))$
10	9	rspcev	$⊢ (a \in ℕ_{0} \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \exists c \in ℕ_{0} \exists b \in ℤ (A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1)$
11	10	adantll	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land a \in ℕ_{0}) \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \exists c \in ℕ_{0} \exists b \in ℤ (A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1)$
12		elpell14qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists c \in ℕ_{0} \exists b \in ℤ (A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1)))$
13	12	ad4antr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land a \in ℕ_{0}) \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists c \in ℕ_{0} \exists b \in ℤ (A = c + \sqrt{D} b \land c^{2} - D b^{2} = 1)))$
14	2 11 13	mpbir2and	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land a \in ℕ_{0}) \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \in Pell14QR (D)$
15	14	orcd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land a \in ℕ_{0}) \land \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))$
16	15	exp31	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \to (a \in ℕ_{0} \to (\exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))))$
17		simp-5r	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \in ℝ$
18	17	renegcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - A \in ℝ$
19		simpllr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - a \in ℕ_{0}$
20		znegcl	$⊢ b \in ℤ \to - b \in ℤ$
21	20	ad2antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - b \in ℤ$
22		simprl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A = a + \sqrt{D} b$
23	22	negeqd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - A = - (a + \sqrt{D} b)$
24		zcn	$⊢ a \in ℤ \to a \in ℂ$
25	24	ad4antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a \in ℂ$
26		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
27	26	nncnd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℂ$
28	27	ad5antr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to D \in ℂ$
29	28	sqrtcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} \in ℂ$
30		zcn	$⊢ b \in ℤ \to b \in ℂ$
31	30	ad2antlr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to b \in ℂ$
32	29 31	mulcld	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \sqrt{D} b \in ℂ$
33	25 32	negdid	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - (a + \sqrt{D} b) = - a + (- \sqrt{D} b)$
34		mulneg2	$⊢ (\sqrt{D} \in ℂ \land b \in ℂ) \to \sqrt{D} (- b) = - \sqrt{D} b$
35	34	eqcomd	$⊢ (\sqrt{D} \in ℂ \land b \in ℂ) \to - \sqrt{D} b = \sqrt{D} (- b)$
36	29 31 35	syl2anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - \sqrt{D} b = \sqrt{D} (- b)$
37	36	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - a + (- \sqrt{D} b) = - a + \sqrt{D} (- b)$
38	23 33 37	3eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - A = - a + \sqrt{D} (- b)$
39		sqneg	$⊢ a \in ℂ \to {(- a)}^{2} = a^{2}$
40	25 39	syl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {(- a)}^{2} = a^{2}$
41		sqneg	$⊢ b \in ℂ \to {(- b)}^{2} = b^{2}$
42	31 41	syl	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {(- b)}^{2} = b^{2}$
43	42	oveq2d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to D {(- b)}^{2} = D b^{2}$
44	40 43	oveq12d	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {(- a)}^{2} - D {(- b)}^{2} = a^{2} - D b^{2}$
45		simprr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a^{2} - D b^{2} = 1$
46	44 45	eqtrd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to {(- a)}^{2} - D {(- b)}^{2} = 1$
47		oveq1	$⊢ c = - a \to c + \sqrt{D} d = - a + \sqrt{D} d$
48	47	eqeq2d	$⊢ c = - a \to (- A = c + \sqrt{D} d \leftrightarrow - A = - a + \sqrt{D} d)$
49		oveq1	$⊢ c = - a \to c^{2} = {(- a)}^{2}$
50	49	oveq1d	$⊢ c = - a \to c^{2} - D d^{2} = {(- a)}^{2} - D d^{2}$
51	50	eqeq1d	$⊢ c = - a \to (c^{2} - D d^{2} = 1 \leftrightarrow {(- a)}^{2} - D d^{2} = 1)$
52	48 51	anbi12d	$⊢ c = - a \to ((- A = c + \sqrt{D} d \land c^{2} - D d^{2} = 1) \leftrightarrow (- A = - a + \sqrt{D} d \land {(- a)}^{2} - D d^{2} = 1))$
53		oveq2	$⊢ d = - b \to \sqrt{D} d = \sqrt{D} (- b)$
54	53	oveq2d	$⊢ d = - b \to - a + \sqrt{D} d = - a + \sqrt{D} (- b)$
55	54	eqeq2d	$⊢ d = - b \to (- A = - a + \sqrt{D} d \leftrightarrow - A = - a + \sqrt{D} (- b))$
56		oveq1	$⊢ d = - b \to d^{2} = {(- b)}^{2}$
57	56	oveq2d	$⊢ d = - b \to D d^{2} = D {(- b)}^{2}$
58	57	oveq2d	$⊢ d = - b \to {(- a)}^{2} - D d^{2} = {(- a)}^{2} - D {(- b)}^{2}$
59	58	eqeq1d	$⊢ d = - b \to ({(- a)}^{2} - D d^{2} = 1 \leftrightarrow {(- a)}^{2} - D {(- b)}^{2} = 1)$
60	55 59	anbi12d	$⊢ d = - b \to ((- A = - a + \sqrt{D} d \land {(- a)}^{2} - D d^{2} = 1) \leftrightarrow (- A = - a + \sqrt{D} (- b) \land {(- a)}^{2} - D {(- b)}^{2} = 1))$
61	52 60	rspc2ev	$⊢ (- a \in ℕ_{0} \land - b \in ℤ \land (- A = - a + \sqrt{D} (- b) \land {(- a)}^{2} - D {(- b)}^{2} = 1)) \to \exists c \in ℕ_{0} \exists d \in ℤ (- A = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)$
62	19 21 38 46 61	syl112anc	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to \exists c \in ℕ_{0} \exists d \in ℤ (- A = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)$
63		elpell14qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (- A \in Pell14QR (D) \leftrightarrow (- A \in ℝ \land \exists c \in ℕ_{0} \exists d \in ℤ (- A = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
64	63	ad5antr	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (- A \in Pell14QR (D) \leftrightarrow (- A \in ℝ \land \exists c \in ℕ_{0} \exists d \in ℤ (- A = c + \sqrt{D} d \land c^{2} - D d^{2} = 1)))$
65	18 62 64	mpbir2and	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to - A \in Pell14QR (D)$
66	65	olcd	$⊢ (((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))$
67	66	ex	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \land b \in ℤ) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
68	67	rexlimdva	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \land - a \in ℕ_{0}) \to (\exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
69	68	ex	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \to (- a \in ℕ_{0} \to (\exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))))$
70		elznn0	$⊢ a \in ℤ \leftrightarrow (a \in ℝ \land (a \in ℕ_{0} \lor - a \in ℕ_{0}))$
71	70	simprbi	$⊢ a \in ℤ \to (a \in ℕ_{0} \lor - a \in ℕ_{0})$
72	71	adantl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \to (a \in ℕ_{0} \lor - a \in ℕ_{0})$
73	16 69 72	mpjaod	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land a \in ℤ) \to (\exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
74	73	rexlimdva	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \to (\exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
75	74	expimpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in ℝ \land \exists a \in ℤ \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
76	1 75	sylbid	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1234QR (D) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D)))$
77	76	imp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to (A \in Pell14QR (D) \lor - A \in Pell14QR (D))$

Metamath Proof Explorer

Theorem pell1234qrdich

Proof