pellexlem2 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pellexlem2		Structured version Visualization version GIF version

Theorem pellexlem2 40568

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

**Assertion**
Ref	Expression
pellexlem2	⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))

**Proof of Theorem pellexlem2**
Step	Hyp	Ref	Expression
1		simpl3 1191	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℕ)
2	1	nnred 11918	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℝ)
3	2	resqcld 13893	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℝ)
4	2	sqge0d 13894	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (𝐵↑2))
5	3, 4	absidd 15062	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(𝐵↑2)) = (𝐵↑2))
6	5	eqcomd 2744	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) = (abs‘(𝐵↑2)))
7	6	oveq2d 7271	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
8		simpl2 1190	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℕ)
9	8	nncnd 11919	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℂ)
10	9	sqcld 13790	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴↑2) ∈ ℂ)
11		simpl1 1189	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ)
12	11	nncnd 11919	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℂ)
13	1	nncnd 11919	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℂ)
14	13	sqcld 13790	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℂ)
15	12, 14	mulcld 10926	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐷 · (𝐵↑2)) ∈ ℂ)
16	10, 15	subcld 11262	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ∈ ℂ)
17	1	nnne0d 11953	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ≠ 0)
18		sqne0 13771	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0))
19	18	biimpar 477	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵↑2) ≠ 0)
20	13, 17, 19	syl2anc 583	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ≠ 0)
21	16, 14, 20	absdivd 15095	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
22	7, 21	eqtr4d 2781	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))))
23	22	oveq2d 7271	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))))
24	16	abscld 15076	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℝ)
25	24	recnd 10934	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℂ)
26	25, 14, 20	divcan2d 11683	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))))
27	10, 15, 14, 20	divsubdird 11720	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))))
28	9, 13, 17	sqdivd 13805	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
29	28	eqcomd 2744	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) / (𝐵↑2)) = ((𝐴 / 𝐵)↑2))
30	11	nnred 11918	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℝ)
31	11	nnnn0d 12223	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ₀)
32	31	nn0ge0d 12226	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 𝐷)
33		remsqsqrt 14896	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
34	30, 32, 33	syl2anc 583	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
35	30, 32	resqrtcld 15057	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℝ)
36	35	recnd 10934	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℂ)
37	36	sqvald 13789	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷)↑2) = ((√‘𝐷) · (√‘𝐷)))
38	12, 14, 20	divcan4d 11687	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = 𝐷)
39	34, 37, 38	3eqtr4rd 2789	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = ((√‘𝐷)↑2))
40	29, 39	oveq12d 7273	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))) = (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)))
41	9, 13, 17	divcld 11681	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℂ)
42		subsq 13854	. . . . . . . 8 ⊢ (((𝐴 / 𝐵) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
43	41, 36, 42	syl2anc 583	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
44	41, 36	addcld 10925	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ)
45	8	nnred 11918	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℝ)
46	45, 1	nndivred 11957	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℝ)
47	46, 35	resubcld 11333	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℝ)
48	47	recnd 10934	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℂ)
49	44, 48	mulcomd 10927	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
50	43, 49	eqtrd 2778	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
51	27, 40, 50	3eqtrd 2782	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
52	51	fveq2d 6760	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))))
53	52	oveq2d 7271	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
54	23, 26, 53	3eqtr3d 2786	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
55	48, 44	absmuld 15094	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
56	55	oveq2d 7271	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) = ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
57	48	abscld 15076	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ)
58	44	abscld 15076	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ)
59	57, 58	remulcld 10936	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
60	3, 59	remulcld 10936	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
61		2nn0 12180	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
62	61	nn0negzi 12289	. . . . . . . 8 ⊢ -2 ∈ ℤ
63	62	a1i 11	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → -2 ∈ ℤ)
64	2, 17, 63	reexpclzd 13892	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℝ)
65	64, 58	remulcld 10936	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
66	3, 65	remulcld 10936	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
67		1red 10907	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ∈ ℝ)
68		2re 11977	. . . . . . 7 ⊢ 2 ∈ ℝ
69	68	a1i 11	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 2 ∈ ℝ)
70	69, 35	remulcld 10936	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℝ)
71	67, 70	readdcld 10935	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
72		simpr 484	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2))
73	8	nngt0d 11952	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐴)
74	1	nngt0d 11952	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐵)
75	45, 2, 73, 74	divgt0d 11840	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐴 / 𝐵))
76	11	nngt0d 11952	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐷)
77		sqrtgt0 14898	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℝ ∧ 0 < 𝐷) → 0 < (√‘𝐷))
78	30, 76, 77	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (√‘𝐷))
79	46, 35, 75, 78	addgt0d 11480	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < ((𝐴 / 𝐵) + (√‘𝐷)))
80	79	gt0ne0d 11469	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0)
81		absgt0 14964	. . . . . . . . 9 ⊢ (((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ → (((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0 ↔ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
82	81	biimpa 476	. . . . . . . 8 ⊢ ((((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ ∧ ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
83	44, 80, 82	syl2anc 583	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
84		ltmul1 11755	. . . . . . 7 ⊢ (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ ∧ (𝐵↑-2) ∈ ℝ ∧ ((abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ ∧ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
85	57, 64, 58, 83, 84	syl112anc 1372	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
86	72, 85	mpbid 231	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
87	2, 17	sqgt0d 13895	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐵↑2))
88		ltmul2 11756	. . . . . 6 ⊢ ((((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ ∧ ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ ∧ ((𝐵↑2) ∈ ℝ ∧ 0 < (𝐵↑2))) → (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ↔ ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))))
89	59, 65, 3, 87, 88	syl112anc 1372	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ↔ ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))))
90	86, 89	mpbid 231	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
91	13, 17, 63	expclzd 13797	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℂ)
92	58	recnd 10934	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ)
93		mulass 10890	. . . . . . . 8 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
94	93	eqcomd 2744	. . . . . . 7 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
95	14, 91, 92, 94	syl3anc 1369	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
96		expneg 13718	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑-2) = (1 / (𝐵↑2)))
97	13, 61, 96	sylancl 585	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) = (1 / (𝐵↑2)))
98	97	oveq2d 7271	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = ((𝐵↑2) · (1 / (𝐵↑2))))
99	14, 20	recidd 11676	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (1 / (𝐵↑2))) = 1)
100	98, 99	eqtrd 2778	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = 1)
101	100	oveq1d 7270	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
102	92	mulid2d 10924	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
103	95, 101, 102	3eqtrd 2782	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
104	41, 36	addcomd 11107	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = ((√‘𝐷) + (𝐴 / 𝐵)))
105		ppncan 11193	. . . . . . . . . 10 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = ((√‘𝐷) + (𝐴 / 𝐵)))
106	105	eqcomd 2744	. . . . . . . . 9 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
107	36, 36, 41, 106	syl3anc 1369	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
108	36, 36	addcld 10925	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) ∈ ℂ)
109	108, 48	addcomd 11107	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))))
110		2times 12039	. . . . . . . . . . . 12 ⊢ ((√‘𝐷) ∈ ℂ → (2 · (√‘𝐷)) = ((√‘𝐷) + (√‘𝐷)))
111	110	eqcomd 2744	. . . . . . . . . . 11 ⊢ ((√‘𝐷) ∈ ℂ → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
112	36, 111	syl 17	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
113	112	oveq2d 7271	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
114	109, 113	eqtrd 2778	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
115	104, 107, 114	3eqtrd 2782	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
116	115	fveq2d 6760	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))))
117	47, 70	readdcld 10935	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℝ)
118	117	recnd 10934	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℂ)
119	118	abscld 15076	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ∈ ℝ)
120	70	recnd 10934	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℂ)
121	120	abscld 15076	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) ∈ ℝ)
122	57, 121	readdcld 10935	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ∈ ℝ)
123	48, 120	abstrid 15096	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))))
124		0le2 12005	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
125	124	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 2)
126	30, 32	sqrtge0d 15060	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (√‘𝐷))
127	69, 35, 125, 126	mulge0d 11482	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (2 · (√‘𝐷)))
128	70, 127	absidd 15062	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) = (2 · (√‘𝐷)))
129	128	oveq2d 7271	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))))
130	1	nnsqcld 13887	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℕ)
131	130	nnge1d 11951	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ≤ (𝐵↑2))
132		0lt1 11427	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 1)
134		lerec 11788	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((𝐵↑2) ∈ ℝ ∧ 0 < (𝐵↑2))) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
135	67, 133, 3, 87, 134	syl22anc 835	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
136	131, 135	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ (1 / 1))
137		1div1e1 11595	. . . . . . . . . . . . 13 ⊢ (1 / 1) = 1
138	136, 137	breqtrdi 5111	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ 1)
139	97, 138	eqbrtrd 5092	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ≤ 1)
140	57, 64, 67, 72, 139	ltletrd 11065	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < 1)
141	57, 67, 140	ltled 11053	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ≤ 1)
142	57, 67, 70, 141	leadd1dd 11519	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
143	129, 142	eqbrtrd 5092	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
144	119, 122, 71, 123, 143	letrd 11062	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
145	116, 144	eqbrtrd 5092	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
146	103, 145	eqbrtrd 5092	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ≤ (1 + (2 · (√‘𝐷))))
147	60, 66, 71, 90, 146	ltletrd 11065	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
148	56, 147	eqbrtrd 5092	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
149	54, 148	eqbrtrd 5092	1 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ↑cexp 13710 √csqrt 14872 abscabs 14873

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875

This theorem is referenced by: pellexlem3 40569

W3C validator