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 43216

Description: Lemma for pellex 43221. 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 1195	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℕ)
2	1	nnred 12174	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℝ)
3	2	resqcld 14062	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℝ)
4	2	sqge0d 14074	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (𝐵↑2))
5	3, 4	absidd 15360	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(𝐵↑2)) = (𝐵↑2))
6	5	eqcomd 2743	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) = (abs‘(𝐵↑2)))
7	6	oveq2d 7386	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
8		simpl2 1194	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℕ)
9	8	nncnd 12175	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℂ)
10	9	sqcld 14081	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴↑2) ∈ ℂ)
11		simpl1 1193	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ)
12	11	nncnd 12175	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℂ)
13	1	nncnd 12175	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℂ)
14	13	sqcld 14081	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℂ)
15	12, 14	mulcld 11166	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐷 · (𝐵↑2)) ∈ ℂ)
16	10, 15	subcld 11506	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ∈ ℂ)
17	1	nnne0d 12209	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ≠ 0)
18		sqne0 14060	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0))
19	18	biimpar 477	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵↑2) ≠ 0)
20	13, 17, 19	syl2anc 585	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ≠ 0)
21	16, 14, 20	absdivd 15395	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
22	7, 21	eqtr4d 2775	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))))
23	22	oveq2d 7386	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))))
24	16	abscld 15376	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℝ)
25	24	recnd 11174	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℂ)
26	25, 14, 20	divcan2d 11933	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))))
27	10, 15, 14, 20	divsubdird 11970	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))))
28	9, 13, 17	sqdivd 14096	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
29	28	eqcomd 2743	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) / (𝐵↑2)) = ((𝐴 / 𝐵)↑2))
30	11	nnred 12174	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℝ)
31	11	nnnn0d 12476	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ₀)
32	31	nn0ge0d 12479	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 𝐷)
33		remsqsqrt 15193	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
34	30, 32, 33	syl2anc 585	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
35	30, 32	resqrtcld 15355	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℝ)
36	35	recnd 11174	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℂ)
37	36	sqvald 14080	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷)↑2) = ((√‘𝐷) · (√‘𝐷)))
38	12, 14, 20	divcan4d 11937	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = 𝐷)
39	34, 37, 38	3eqtr4rd 2783	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = ((√‘𝐷)↑2))
40	29, 39	oveq12d 7388	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))) = (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)))
41	9, 13, 17	divcld 11931	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℂ)
42		subsq 14147	. . . . . . . 8 ⊢ (((𝐴 / 𝐵) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
43	41, 36, 42	syl2anc 585	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
44	41, 36	addcld 11165	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ)
45	8	nnred 12174	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℝ)
46	45, 1	nndivred 12213	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℝ)
47	46, 35	resubcld 11579	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℝ)
48	47	recnd 11174	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℂ)
49	44, 48	mulcomd 11167	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
50	43, 49	eqtrd 2772	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
51	27, 40, 50	3eqtrd 2776	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
52	51	fveq2d 6848	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))))
53	52	oveq2d 7386	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
54	23, 26, 53	3eqtr3d 2780	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
55	48, 44	absmuld 15394	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
56	55	oveq2d 7386	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) = ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
57	48	abscld 15376	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ)
58	44	abscld 15376	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ)
59	57, 58	remulcld 11176	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
60	3, 59	remulcld 11176	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
61		2nn0 12432	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
62	61	nn0negzi 12544	. . . . . . . 8 ⊢ -2 ∈ ℤ
63	62	a1i 11	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → -2 ∈ ℤ)
64	2, 17, 63	reexpclzd 14186	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℝ)
65	64, 58	remulcld 11176	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
66	3, 65	remulcld 11176	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
67		1red 11147	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ∈ ℝ)
68		2re 12233	. . . . . . 7 ⊢ 2 ∈ ℝ
69	68	a1i 11	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 2 ∈ ℝ)
70	69, 35	remulcld 11176	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℝ)
71	67, 70	readdcld 11175	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
72		simpr 484	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2))
73	8	nngt0d 12208	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐴)
74	1	nngt0d 12208	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐵)
75	45, 2, 73, 74	divgt0d 12091	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐴 / 𝐵))
76	11	nngt0d 12208	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐷)
77		sqrtgt0 15195	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℝ ∧ 0 < 𝐷) → 0 < (√‘𝐷))
78	30, 76, 77	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (√‘𝐷))
79	46, 35, 75, 78	addgt0d 11726	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < ((𝐴 / 𝐵) + (√‘𝐷)))
80	79	gt0ne0d 11715	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0)
81		absgt0 15262	. . . . . . . . 9 ⊢ (((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ → (((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0 ↔ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
82	81	biimpa 476	. . . . . . . 8 ⊢ ((((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ ∧ ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
83	44, 80, 82	syl2anc 585	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
84		ltmul1 12005	. . . . . . 7 ⊢ (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ ∧ (𝐵↑-2) ∈ ℝ ∧ ((abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ ∧ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
85	57, 64, 58, 83, 84	syl112anc 1377	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
86	72, 85	mpbid 232	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
87	2, 17	sqgt0d 14187	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐵↑2))
88		ltmul2 12006	. . . . . 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 1377	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ↔ ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))))
90	86, 89	mpbid 232	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
91	13, 17, 63	expclzd 14088	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℂ)
92	58	recnd 11174	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ)
93		mulass 11128	. . . . . . . 8 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
94	93	eqcomd 2743	. . . . . . 7 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
95	14, 91, 92, 94	syl3anc 1374	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
96		expneg 14006	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑-2) = (1 / (𝐵↑2)))
97	13, 61, 96	sylancl 587	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) = (1 / (𝐵↑2)))
98	97	oveq2d 7386	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = ((𝐵↑2) · (1 / (𝐵↑2))))
99	14, 20	recidd 11926	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (1 / (𝐵↑2))) = 1)
100	98, 99	eqtrd 2772	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = 1)
101	100	oveq1d 7385	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
102	92	mullidd 11164	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
103	95, 101, 102	3eqtrd 2776	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
104	41, 36	addcomd 11349	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = ((√‘𝐷) + (𝐴 / 𝐵)))
105		ppncan 11437	. . . . . . . . . 10 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = ((√‘𝐷) + (𝐴 / 𝐵)))
106	105	eqcomd 2743	. . . . . . . . 9 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
107	36, 36, 41, 106	syl3anc 1374	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
108	36, 36	addcld 11165	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) ∈ ℂ)
109	108, 48	addcomd 11349	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))))
110		2times 12290	. . . . . . . . . . . 12 ⊢ ((√‘𝐷) ∈ ℂ → (2 · (√‘𝐷)) = ((√‘𝐷) + (√‘𝐷)))
111	110	eqcomd 2743	. . . . . . . . . . 11 ⊢ ((√‘𝐷) ∈ ℂ → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
112	36, 111	syl 17	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
113	112	oveq2d 7386	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
114	109, 113	eqtrd 2772	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
115	104, 107, 114	3eqtrd 2776	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
116	115	fveq2d 6848	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))))
117	47, 70	readdcld 11175	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℝ)
118	117	recnd 11174	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℂ)
119	118	abscld 15376	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ∈ ℝ)
120	70	recnd 11174	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℂ)
121	120	abscld 15376	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) ∈ ℝ)
122	57, 121	readdcld 11175	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ∈ ℝ)
123	48, 120	abstrid 15396	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))))
124		0le2 12261	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
125	124	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 2)
126	30, 32	sqrtge0d 15358	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (√‘𝐷))
127	69, 35, 125, 126	mulge0d 11728	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (2 · (√‘𝐷)))
128	70, 127	absidd 15360	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) = (2 · (√‘𝐷)))
129	128	oveq2d 7386	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))))
130	1	nnsqcld 14181	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℕ)
131	130	nnge1d 12207	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ≤ (𝐵↑2))
132		0lt1 11673	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 1)
134		lerec 12039	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((𝐵↑2) ∈ ℝ ∧ 0 < (𝐵↑2))) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
135	67, 133, 3, 87, 134	syl22anc 839	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
136	131, 135	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ (1 / 1))
137		1div1e1 11846	. . . . . . . . . . . . 13 ⊢ (1 / 1) = 1
138	136, 137	breqtrdi 5141	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ 1)
139	97, 138	eqbrtrd 5122	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ≤ 1)
140	57, 64, 67, 72, 139	ltletrd 11307	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < 1)
141	57, 67, 140	ltled 11295	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ≤ 1)
142	57, 67, 70, 141	leadd1dd 11765	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
143	129, 142	eqbrtrd 5122	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
144	119, 122, 71, 123, 143	letrd 11304	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
145	116, 144	eqbrtrd 5122	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
146	103, 145	eqbrtrd 5122	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ≤ (1 + (2 · (√‘𝐷))))
147	60, 66, 71, 90, 146	ltletrd 11307	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
148	56, 147	eqbrtrd 5122	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
149	54, 148	eqbrtrd 5122	1 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5100 ‘cfv 6502 (class class class)co 7370 ℂcc 11038 ℝcr 11039 0cc0 11040 1c1 11041 + caddc 11043 · cmul 11045 < clt 11180 ≤ cle 11181 − cmin 11378 -cneg 11379 / cdiv 11808 ℕcn 12159 2c2 12214 ℕ₀cn0 12415 ℤcz 12502 ↑cexp 13998 √csqrt 15170 abscabs 15171

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-sup 9359 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-n0 12416 df-z 12503 df-uz 12766 df-rp 12920 df-seq 13939 df-exp 13999 df-cj 15036 df-re 15037 df-im 15038 df-sqrt 15172 df-abs 15173

This theorem is referenced by: pellexlem3 43217

W3C validator