pell1234qrne0

Description: No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014)

		Ref	Expression
	Assertion	pell1234qrne0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \neq 0$

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		simprl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A = a + \sqrt{D} b$
3		ax-1ne0	$⊢ 1 \neq 0$
4		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
5	4	adantr	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \to D \in ℕ$
6	5	nncnd	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \to D \in ℂ$
7	6	ad3antrrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to D \in ℂ$
8	7	sqrtcld	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to \sqrt{D} \in ℂ$
9		zcn	$⊢ b \in ℤ \to b \in ℂ$
10	9	ad2antll	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
11	10	ad2antrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to b \in ℂ$
12	8 11	sqmuld	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to {\sqrt{D} b}^{2} = {\sqrt{D}}^{2} b^{2}$
13	7	sqsqrtd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to {\sqrt{D}}^{2} = D$
14	13	oveq1d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to {\sqrt{D}}^{2} b^{2} = D b^{2}$
15	12 14	eqtr2d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to D b^{2} = {\sqrt{D} b}^{2}$
16	15	oveq2d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a^{2} - D b^{2} = a^{2} - {\sqrt{D} b}^{2}$
17		zcn	$⊢ a \in ℤ \to a \in ℂ$
18	17	ad2antrl	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
19	18	ad2antrr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a \in ℂ$
20	8 11	mulcld	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to \sqrt{D} b \in ℂ$
21		subsq	$⊢ (a \in ℂ \land \sqrt{D} b \in ℂ) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
22	19 20 21	syl2anc	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a^{2} - {\sqrt{D} b}^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
23	16 22	eqtrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a^{2} - D b^{2} = (a + \sqrt{D} b) (a - \sqrt{D} b)$
24		simplr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a^{2} - D b^{2} = 1$
25		simpr	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a + \sqrt{D} b = 0$
26	25	oveq1d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to (a + \sqrt{D} b) (a - \sqrt{D} b) = 0 \cdot (a - \sqrt{D} b)$
27	19 20	subcld	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to a - \sqrt{D} b \in ℂ$
28	27	mul02d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to 0 \cdot (a - \sqrt{D} b) = 0$
29	26 28	eqtrd	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to (a + \sqrt{D} b) (a - \sqrt{D} b) = 0$
30	23 24 29	3eqtr3d	$⊢ ((((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \land a + \sqrt{D} b = 0) \to 1 = 0$
31	30	ex	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (a + \sqrt{D} b = 0 \to 1 = 0)$
32	31	necon3d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (1 \neq 0 \to a + \sqrt{D} b \neq 0)$
33	3 32	mpi	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a + \sqrt{D} b \neq 0$
34	33	adantrl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to a + \sqrt{D} b \neq 0$
35	2 34	eqnetrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \land (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to A \neq 0$
36	35	ex	$⊢ ((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℤ \land b \in ℤ)) \to ((A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to A \neq 0)$
37	36	rexlimdvva	$⊢ (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 \neq 0)$
38	37	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 \neq 0)$
39	1 38	sylbid	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell1234QR (D) \to A \neq 0)$
40	39	imp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell1234QR (D)) \to A \neq 0$

Metamath Proof Explorer

Theorem pell1234qrne0

Proof