pellexlem2

Description: Lemma for pellex . Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014)

		Ref	Expression
	Assertion	pellexlem2	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|A^{2} - D B^{2}\| < 1 + 2 \sqrt{D}$

Proof

Step	Hyp	Ref	Expression
1		simpl3	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B \in ℕ$
2	1	nnred	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B \in ℝ$
3	2	resqcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \in ℝ$
4	2	sqge0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 \leq B^{2}$
5	3 4	absidd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|B^{2}\| = B^{2}$
6	5	eqcomd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} = \|B^{2}\|$
7	6	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{\|A^{2} - D B^{2}\|}{B^{2}} = \frac{\|A^{2} - D B^{2}\|}{\|B^{2}\|}$
8		simpl2	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to A \in ℕ$
9	8	nncnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to A \in ℂ$
10	9	sqcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to A^{2} \in ℂ$
11		simpl1	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to D \in ℕ$
12	11	nncnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to D \in ℂ$
13	1	nncnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B \in ℂ$
14	13	sqcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \in ℂ$
15	12 14	mulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to D B^{2} \in ℂ$
16	10 15	subcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to A^{2} - D B^{2} \in ℂ$
17	1	nnne0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B \neq 0$
18		sqne0	$⊢ B \in ℂ \to (B^{2} \neq 0 \leftrightarrow B \neq 0)$
19	18	biimpar	$⊢ (B \in ℂ \land B \neq 0) \to B^{2} \neq 0$
20	13 17 19	syl2anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \neq 0$
21	16 14 20	absdivd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|\frac{A^{2} - D B^{2}}{B^{2}}\| = \frac{\|A^{2} - D B^{2}\|}{\|B^{2}\|}$
22	7 21	eqtr4d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{\|A^{2} - D B^{2}\|}{B^{2}} = \|\frac{A^{2} - D B^{2}}{B^{2}}\|$
23	22	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} (\frac{\|A^{2} - D B^{2}\|}{B^{2}}) = B^{2} \|\frac{A^{2} - D B^{2}}{B^{2}}\|$
24	16	abscld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|A^{2} - D B^{2}\| \in ℝ$
25	24	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|A^{2} - D B^{2}\| \in ℂ$
26	25 14 20	divcan2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} (\frac{\|A^{2} - D B^{2}\|}{B^{2}}) = \|A^{2} - D B^{2}\|$
27	10 15 14 20	divsubdird	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{A^{2} - D B^{2}}{B^{2}} = (\frac{A^{2}}{B^{2}}) - (\frac{D B^{2}}{B^{2}})$
28	9 13 17	sqdivd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to {(\frac{A}{B})}^{2} = \frac{A^{2}}{B^{2}}$
29	28	eqcomd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{A^{2}}{B^{2}} = {(\frac{A}{B})}^{2}$
30	11	nnred	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to D \in ℝ$
31	11	nnnn0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to D \in ℕ_{0}$
32	31	nn0ge0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 \leq D$
33		remsqsqrt	$⊢ (D \in ℝ \land 0 \leq D) \to \sqrt{D} \sqrt{D} = D$
34	30 32 33	syl2anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} \sqrt{D} = D$
35	30 32	resqrtcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} \in ℝ$
36	35	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} \in ℂ$
37	36	sqvald	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to {\sqrt{D}}^{2} = \sqrt{D} \sqrt{D}$
38	12 14 20	divcan4d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{D B^{2}}{B^{2}} = D$
39	34 37 38	3eqtr4rd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{D B^{2}}{B^{2}} = {\sqrt{D}}^{2}$
40	29 39	oveq12d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A^{2}}{B^{2}}) - (\frac{D B^{2}}{B^{2}}) = {(\frac{A}{B})}^{2} - {\sqrt{D}}^{2}$
41	9 13 17	divcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{A}{B} \in ℂ$
42		subsq	$⊢ (\frac{A}{B} \in ℂ \land \sqrt{D} \in ℂ) \to {(\frac{A}{B})}^{2} - {\sqrt{D}}^{2} = ((\frac{A}{B}) + \sqrt{D}) ((\frac{A}{B}) - \sqrt{D})$
43	41 36 42	syl2anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to {(\frac{A}{B})}^{2} - {\sqrt{D}}^{2} = ((\frac{A}{B}) + \sqrt{D}) ((\frac{A}{B}) - \sqrt{D})$
44	41 36	addcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) + \sqrt{D} \in ℂ$
45	8	nnred	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to A \in ℝ$
46	45 1	nndivred	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{A}{B} \in ℝ$
47	46 35	resubcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) - \sqrt{D} \in ℝ$
48	47	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) - \sqrt{D} \in ℂ$
49	44 48	mulcomd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to ((\frac{A}{B}) + \sqrt{D}) ((\frac{A}{B}) - \sqrt{D}) = ((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})$
50	43 49	eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to {(\frac{A}{B})}^{2} - {\sqrt{D}}^{2} = ((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})$
51	27 40 50	3eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{A^{2} - D B^{2}}{B^{2}} = ((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})$
52	51	fveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|\frac{A^{2} - D B^{2}}{B^{2}}\| = \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\|$
53	52	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|\frac{A^{2} - D B^{2}}{B^{2}}\| = B^{2} \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\|$
54	23 26 53	3eqtr3d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|A^{2} - D B^{2}\| = B^{2} \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\|$
55	48 44	absmuld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\| = \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\|$
56	55	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\| = B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\|$
57	48	abscld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| \in ℝ$
58	44	abscld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ$
59	57 58	remulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ$
60	3 59	remulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ$
61		2nn0	$⊢ 2 \in ℕ_{0}$
62	61	nn0negzi	$⊢ - 2 \in ℤ$
63	62	a1i	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to - 2 \in ℤ$
64	2 17 63	reexpclzd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{- 2} \in ℝ$
65	64 58	remulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ$
66	3 65	remulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ$
67		1red	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 1 \in ℝ$
68		2re	$⊢ 2 \in ℝ$
69	68	a1i	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 2 \in ℝ$
70	69 35	remulcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 2 \sqrt{D} \in ℝ$
71	67 70	readdcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 1 + 2 \sqrt{D} \in ℝ$
72		simpr	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}$
73	8	nngt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < A$
74	1	nngt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < B$
75	45 2 73 74	divgt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < \frac{A}{B}$
76	11	nngt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < D$
77		sqrtgt0	$⊢ (D \in ℝ \land 0 < D) \to 0 < \sqrt{D}$
78	30 76 77	syl2anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < \sqrt{D}$
79	46 35 75 78	addgt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < (\frac{A}{B}) + \sqrt{D}$
80	79	gt0ne0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) + \sqrt{D} \neq 0$
81		absgt0	$⊢ (\frac{A}{B}) + \sqrt{D} \in ℂ \to ((\frac{A}{B}) + \sqrt{D} \neq 0 \leftrightarrow 0 < \|(\frac{A}{B}) + \sqrt{D}\|)$
82	81	biimpa	$⊢ ((\frac{A}{B}) + \sqrt{D} \in ℂ \land (\frac{A}{B}) + \sqrt{D} \neq 0) \to 0 < \|(\frac{A}{B}) + \sqrt{D}\|$
83	44 80 82	syl2anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < \|(\frac{A}{B}) + \sqrt{D}\|$
84		ltmul1	$⊢ (\|(\frac{A}{B}) - \sqrt{D}\| \in ℝ \land B^{- 2} \in ℝ \land (\|(\frac{A}{B}) + \sqrt{D}\| \in ℝ \land 0 < \|(\frac{A}{B}) + \sqrt{D}\|)) \to (\|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2} \leftrightarrow \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|)$
85	57 64 58 83 84	syl112anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2} \leftrightarrow \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|)$
86	72 85	mpbid	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|$
87	2 17	sqgt0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < B^{2}$
88		ltmul2	$⊢ (\|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ \land B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \in ℝ \land (B^{2} \in ℝ \land 0 < B^{2})) \to (\|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \leftrightarrow B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|)$
89	59 65 3 87 88	syl112anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \leftrightarrow B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|)$
90	86 89	mpbid	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|$
91	13 17 63	expclzd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{- 2} \in ℂ$
92	58	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) + \sqrt{D}\| \in ℂ$
93		mulass	$⊢ (B^{2} \in ℂ \land B^{- 2} \in ℂ \land \|(\frac{A}{B}) + \sqrt{D}\| \in ℂ) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| = B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|$
94	93	eqcomd	$⊢ (B^{2} \in ℂ \land B^{- 2} \in ℂ \land \|(\frac{A}{B}) + \sqrt{D}\| \in ℂ) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| = B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|$
95	14 91 92 94	syl3anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| = B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\|$
96		expneg	$⊢ (B \in ℂ \land 2 \in ℕ_{0}) \to B^{- 2} = \frac{1}{B^{2}}$
97	13 61 96	sylancl	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{- 2} = \frac{1}{B^{2}}$
98	97	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} = B^{2} (\frac{1}{B^{2}})$
99	14 20	recidd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} (\frac{1}{B^{2}}) = 1$
100	98 99	eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} = 1$
101	100	oveq1d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| = 1 \|(\frac{A}{B}) + \sqrt{D}\|$
102	92	mulid2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 1 \|(\frac{A}{B}) + \sqrt{D}\| = \|(\frac{A}{B}) + \sqrt{D}\|$
103	95 101 102	3eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| = \|(\frac{A}{B}) + \sqrt{D}\|$
104	41 36	addcomd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) + \sqrt{D} = \sqrt{D} + (\frac{A}{B})$
105		ppncan	$⊢ (\sqrt{D} \in ℂ \land \sqrt{D} \in ℂ \land \frac{A}{B} \in ℂ) \to \sqrt{D} + \sqrt{D} + ((\frac{A}{B}) - \sqrt{D}) = \sqrt{D} + (\frac{A}{B})$
106	105	eqcomd	$⊢ (\sqrt{D} \in ℂ \land \sqrt{D} \in ℂ \land \frac{A}{B} \in ℂ) \to \sqrt{D} + (\frac{A}{B}) = \sqrt{D} + \sqrt{D} + ((\frac{A}{B}) - \sqrt{D})$
107	36 36 41 106	syl3anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} + (\frac{A}{B}) = \sqrt{D} + \sqrt{D} + ((\frac{A}{B}) - \sqrt{D})$
108	36 36	addcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} + \sqrt{D} \in ℂ$
109	108 48	addcomd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} + \sqrt{D} + ((\frac{A}{B}) - \sqrt{D}) = ((\frac{A}{B}) - \sqrt{D}) + \sqrt{D} + \sqrt{D}$
110		2times	$⊢ \sqrt{D} \in ℂ \to 2 \sqrt{D} = \sqrt{D} + \sqrt{D}$
111	110	eqcomd	$⊢ \sqrt{D} \in ℂ \to \sqrt{D} + \sqrt{D} = 2 \sqrt{D}$
112	36 111	syl	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} + \sqrt{D} = 2 \sqrt{D}$
113	112	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to ((\frac{A}{B}) - \sqrt{D}) + \sqrt{D} + \sqrt{D} = (\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}$
114	109 113	eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \sqrt{D} + \sqrt{D} + ((\frac{A}{B}) - \sqrt{D}) = (\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}$
115	104 107 114	3eqtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) + \sqrt{D} = (\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}$
116	115	fveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) + \sqrt{D}\| = \|(\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}\|$
117	47 70	readdcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D} \in ℝ$
118	117	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D} \in ℂ$
119	118	abscld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}\| \in ℝ$
120	70	recnd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 2 \sqrt{D} \in ℂ$
121	120	abscld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|2 \sqrt{D}\| \in ℝ$
122	57 121	readdcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| + \|2 \sqrt{D}\| \in ℝ$
123	48 120	abstrid	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}\| \leq \|(\frac{A}{B}) - \sqrt{D}\| + \|2 \sqrt{D}\|$
124		0le2	$⊢ 0 \leq 2$
125	124	a1i	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 \leq 2$
126	30 32	sqrtge0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 \leq \sqrt{D}$
127	69 35 125 126	mulge0d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 \leq 2 \sqrt{D}$
128	70 127	absidd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|2 \sqrt{D}\| = 2 \sqrt{D}$
129	128	oveq2d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| + \|2 \sqrt{D}\| = \|(\frac{A}{B}) - \sqrt{D}\| + 2 \sqrt{D}$
130	1	nnsqcld	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \in ℕ$
131	130	nnge1d	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 1 \leq B^{2}$
132		0lt1	$⊢ 0 < 1$
133	132	a1i	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to 0 < 1$
134		lerec	$⊢ ((1 \in ℝ \land 0 < 1) \land (B^{2} \in ℝ \land 0 < B^{2})) \to (1 \leq B^{2} \leftrightarrow \frac{1}{B^{2}} \leq \frac{1}{1})$
135	67 133 3 87 134	syl22anc	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to (1 \leq B^{2} \leftrightarrow \frac{1}{B^{2}} \leq \frac{1}{1})$
136	131 135	mpbid	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{1}{B^{2}} \leq \frac{1}{1}$
137		1div1e1	$⊢ \frac{1}{1} = 1$
138	136 137	breqtrdi	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \frac{1}{B^{2}} \leq 1$
139	97 138	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{- 2} \leq 1$
140	57 64 67 72 139	ltletrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| < 1$
141	57 67 140	ltled	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| \leq 1$
142	57 67 70 141	leadd1dd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| + 2 \sqrt{D} \leq 1 + 2 \sqrt{D}$
143	129 142	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D}\| + \|2 \sqrt{D}\| \leq 1 + 2 \sqrt{D}$
144	119 122 71 123 143	letrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) - \sqrt{D} + 2 \sqrt{D}\| \leq 1 + 2 \sqrt{D}$
145	116 144	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|(\frac{A}{B}) + \sqrt{D}\| \leq 1 + 2 \sqrt{D}$
146	103 145	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} B^{- 2} \|(\frac{A}{B}) + \sqrt{D}\| \leq 1 + 2 \sqrt{D}$
147	60 66 71 90 146	ltletrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|(\frac{A}{B}) - \sqrt{D}\| \|(\frac{A}{B}) + \sqrt{D}\| < 1 + 2 \sqrt{D}$
148	56 147	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to B^{2} \|((\frac{A}{B}) - \sqrt{D}) ((\frac{A}{B}) + \sqrt{D})\| < 1 + 2 \sqrt{D}$
149	54 148	eqbrtrd	$⊢ ((D \in ℕ \land A \in ℕ \land B \in ℕ) \land \|(\frac{A}{B}) - \sqrt{D}\| < B^{- 2}) \to \|A^{2} - D B^{2}\| < 1 + 2 \sqrt{D}$

Metamath Proof Explorer

Theorem pellexlem2

Proof