pellexlem1

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of vandenDries p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014)

		Ref	Expression
	Assertion	pellexlem1	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \neg \sqrt{D} \in ℚ) \to A^{2} - D B^{2} \neq 0$

Proof

Step	Hyp	Ref	Expression
1		nncn	$⊢ A \in ℕ \to A \in ℂ$
2	1	3ad2ant2	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to A \in ℂ$
3	2	sqcld	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to A^{2} \in ℂ$
4		nncn	$⊢ D \in ℕ \to D \in ℂ$
5	4	3ad2ant1	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to D \in ℂ$
6		nncn	$⊢ B \in ℕ \to B \in ℂ$
7	6	3ad2ant3	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B \in ℂ$
8	7	sqcld	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B^{2} \in ℂ$
9	5 8	mulcld	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to D B^{2} \in ℂ$
10	3 9	subeq0ad	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (A^{2} - D B^{2} = 0 \leftrightarrow A^{2} = D B^{2})$
11		nnne0	$⊢ B \in ℕ \to B \neq 0$
12	11	3ad2ant3	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B \neq 0$
13		sqne0	$⊢ B \in ℂ \to (B^{2} \neq 0 \leftrightarrow B \neq 0)$
14	7 13	syl	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (B^{2} \neq 0 \leftrightarrow B \neq 0)$
15	12 14	mpbird	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B^{2} \neq 0$
16	3 5 8 15	divmul3d	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (\frac{A^{2}}{B^{2}} = D \leftrightarrow A^{2} = D B^{2})$
17		sqdiv	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to {(\frac{A}{B})}^{2} = \frac{A^{2}}{B^{2}}$
18	17	fveq2d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \sqrt{{(\frac{A}{B})}^{2}} = \sqrt{\frac{A^{2}}{B^{2}}}$
19	2 7 12 18	syl3anc	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \sqrt{{(\frac{A}{B})}^{2}} = \sqrt{\frac{A^{2}}{B^{2}}}$
20		nnre	$⊢ A \in ℕ \to A \in ℝ$
21	20	3ad2ant2	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to A \in ℝ$
22		nnre	$⊢ B \in ℕ \to B \in ℝ$
23	22	3ad2ant3	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B \in ℝ$
24	21 23 12	redivcld	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \frac{A}{B} \in ℝ$
25		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
26	25	nn0ge0d	$⊢ A \in ℕ \to 0 \leq A$
27	26	3ad2ant2	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to 0 \leq A$
28		nngt0	$⊢ B \in ℕ \to 0 < B$
29	28	3ad2ant3	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to 0 < B$
30		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 < B)) \to 0 \leq \frac{A}{B}$
31	21 27 23 29 30	syl22anc	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to 0 \leq \frac{A}{B}$
32	24 31	sqrtsqd	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \sqrt{{(\frac{A}{B})}^{2}} = \frac{A}{B}$
33	19 32	eqtr3d	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \sqrt{\frac{A^{2}}{B^{2}}} = \frac{A}{B}$
34		nnq	$⊢ A \in ℕ \to A \in ℚ$
35	34	3ad2ant2	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to A \in ℚ$
36		nnq	$⊢ B \in ℕ \to B \in ℚ$
37	36	3ad2ant3	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to B \in ℚ$
38		qdivcl	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to \frac{A}{B} \in ℚ$
39	35 37 12 38	syl3anc	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \frac{A}{B} \in ℚ$
40	33 39	eqeltrd	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to \sqrt{\frac{A^{2}}{B^{2}}} \in ℚ$
41		fveq2	$⊢ \frac{A^{2}}{B^{2}} = D \to \sqrt{\frac{A^{2}}{B^{2}}} = \sqrt{D}$
42	41	eleq1d	$⊢ \frac{A^{2}}{B^{2}} = D \to (\sqrt{\frac{A^{2}}{B^{2}}} \in ℚ \leftrightarrow \sqrt{D} \in ℚ)$
43	40 42	syl5ibcom	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (\frac{A^{2}}{B^{2}} = D \to \sqrt{D} \in ℚ)$
44	16 43	sylbird	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (A^{2} = D B^{2} \to \sqrt{D} \in ℚ)$
45	10 44	sylbid	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (A^{2} - D B^{2} = 0 \to \sqrt{D} \in ℚ)$
46	45	necon3bd	$⊢ (D \in ℕ \land A \in ℕ \land B \in ℕ) \to (\neg \sqrt{D} \in ℚ \to A^{2} - D B^{2} \neq 0)$
47	46	imp	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \neg \sqrt{D} \in ℚ) \to A^{2} - D B^{2} \neq 0$

Metamath Proof Explorer

Theorem pellexlem1

Proof