pell14qrgt0

Description: A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014)

		Ref	Expression
	Assertion	pell14qrgt0	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 < A$

Proof

Step	Hyp	Ref	Expression
1		elpell14qr	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \leftrightarrow (A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)))$
2		0cnd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 \in ℂ$
3		eldifi	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to D \in ℕ$
4	3	ad3antrrr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D \in ℕ$
5	4	nnred	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D \in ℝ$
6	4	nnnn0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D \in ℕ_{0}$
7	6	nn0ge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 \leq D$
8	5 7	resqrtcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \sqrt{D} \in ℝ$
9		zre	$⊢ b \in ℤ \to b \in ℝ$
10	9	adantl	$⊢ (a \in ℕ_{0} \land b \in ℤ) \to b \in ℝ$
11	10	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to b \in ℝ$
12	8 11	remulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \sqrt{D} b \in ℝ$
13	12	recnd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \sqrt{D} b \in ℂ$
14	2 13	abssubd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|0 - \sqrt{D} b\| = \|\sqrt{D} b - 0\|$
15	13	subid1d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \sqrt{D} b - 0 = \sqrt{D} b$
16	15	fveq2d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|\sqrt{D} b - 0\| = \|\sqrt{D} b\|$
17	14 16	eqtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|0 - \sqrt{D} b\| = \|\sqrt{D} b\|$
18		absresq	$⊢ \sqrt{D} b \in ℝ \to {\|\sqrt{D} b\|}^{2} = {\sqrt{D} b}^{2}$
19	12 18	syl	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\|\sqrt{D} b\|}^{2} = {\sqrt{D} b}^{2}$
20	5	recnd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D \in ℂ$
21	20	sqrtcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \sqrt{D} \in ℂ$
22	10	recnd	$⊢ (a \in ℕ_{0} \land b \in ℤ) \to b \in ℂ$
23	22	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to b \in ℂ$
24	21 23	sqmuld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\sqrt{D} b}^{2} = {\sqrt{D}}^{2} b^{2}$
25	20	sqsqrtd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\sqrt{D}}^{2} = D$
26	25	oveq1d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\sqrt{D}}^{2} b^{2} = D b^{2}$
27	19 24 26	3eqtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\|\sqrt{D} b\|}^{2} = D b^{2}$
28		0lt1	$⊢ 0 < 1$
29		simpr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a^{2} - D b^{2} = 1$
30	28 29	breqtrrid	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 < a^{2} - D b^{2}$
31	11	resqcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to b^{2} \in ℝ$
32	5 31	remulcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D b^{2} \in ℝ$
33		nn0re	$⊢ a \in ℕ_{0} \to a \in ℝ$
34	33	adantr	$⊢ (a \in ℕ_{0} \land b \in ℤ) \to a \in ℝ$
35	34	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a \in ℝ$
36	35	resqcld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a^{2} \in ℝ$
37	32 36	posdifd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (D b^{2} < a^{2} \leftrightarrow 0 < a^{2} - D b^{2})$
38	30 37	mpbird	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to D b^{2} < a^{2}$
39	27 38	eqbrtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to {\|\sqrt{D} b\|}^{2} < a^{2}$
40	13	abscld	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|\sqrt{D} b\| \in ℝ$
41	13	absge0d	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 \leq \|\sqrt{D} b\|$
42		nn0ge0	$⊢ a \in ℕ_{0} \to 0 \leq a$
43	42	adantr	$⊢ (a \in ℕ_{0} \land b \in ℤ) \to 0 \leq a$
44	43	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 \leq a$
45	40 35 41 44	lt2sqd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (\|\sqrt{D} b\| < a \leftrightarrow {\|\sqrt{D} b\|}^{2} < a^{2})$
46	39 45	mpbird	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|\sqrt{D} b\| < a$
47	17 46	eqbrtrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to \|0 - \sqrt{D} b\| < a$
48		0red	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 \in ℝ$
49	48 12 35	absdifltd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (\|0 - \sqrt{D} b\| < a \leftrightarrow (\sqrt{D} b - a < 0 \land 0 < \sqrt{D} b + a))$
50	47 49	mpbid	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to (\sqrt{D} b - a < 0 \land 0 < \sqrt{D} b + a)$
51	50	simprd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 < \sqrt{D} b + a$
52		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
53	52	adantr	$⊢ (a \in ℕ_{0} \land b \in ℤ) \to a \in ℂ$
54	53	ad2antlr	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a \in ℂ$
55	54 13	addcomd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to a + \sqrt{D} b = \sqrt{D} b + a$
56	51 55	breqtrrd	$⊢ (((D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \land (a \in ℕ_{0} \land b \in ℤ)) \land a^{2} - D b^{2} = 1) \to 0 < a + \sqrt{D} b$
57	56	adantrl	$⊢ (((D \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 0 < a + \sqrt{D} b$
58		simprl	$⊢ (((D \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$
59	57 58	breqtrrd	$⊢ (((D \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 0 < A$
60	59	ex	$⊢ ((D \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 0 < A)$
61	60	rexlimdvva	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in ℝ) \to (\exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1) \to 0 < A)$
62	61	expimpd	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to ((A \in ℝ \land \exists a \in ℕ_{0} \exists b \in ℤ (A = a + \sqrt{D} b \land a^{2} - D b^{2} = 1)) \to 0 < A)$
63	1 62	sylbid	$⊢ D \in (ℕ ∖ ◻_{ℕ}) \to (A \in Pell14QR (D) \to 0 < A)$
64	63	imp	$⊢ (D \in (ℕ ∖ ◻_{ℕ}) \land A \in Pell14QR (D)) \to 0 < A$

Metamath Proof Explorer

Theorem pell14qrgt0

Proof