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 43483

Description: Lemma for pellex 43488. 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 1210	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℕ)
2	1	nnred 12248	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℝ)
3	2	resqcld 14161	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℝ)
4	2	sqge0d 14173	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (𝐵↑2))
5	3, 4	absidd 15474	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(𝐵↑2)) = (𝐵↑2))
6	5	eqcomd 2775	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) = (abs‘(𝐵↑2)))
7	6	oveq2d 7427	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
8		simpl2 1209	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℕ)
9	8	nncnd 12249	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℂ)
10	9	sqcld 14180	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴↑2) ∈ ℂ)
11		simpl1 1208	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ)
12	11	nncnd 12249	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℂ)
13	1	nncnd 12249	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℂ)
14	13	sqcld 14180	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℂ)
15	12, 14	mulcld 11229	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐷 · (𝐵↑2)) ∈ ℂ)
16	10, 15	subcld 11569	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ∈ ℂ)
17	1	nnne0d 12286	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ≠ 0)
18		sqne0 14159	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0))
19	18	biimpar 482	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵↑2) ≠ 0)
20	13, 17, 19	syl2anc 595	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ≠ 0)
21	16, 14, 20	absdivd 15509	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
22	7, 21	eqtr4d 2807	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))))
23	22	oveq2d 7427	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))))
24	16	abscld 15490	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℝ)
25	24	recnd 11237	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℂ)
26	25, 14, 20	divcan2d 11993	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))))
27	10, 15, 14, 20	divsubdird 12030	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))))
28	9, 13, 17	sqdivd 14195	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
29	28	eqcomd 2775	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) / (𝐵↑2)) = ((𝐴 / 𝐵)↑2))
30	11	nnred 12248	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℝ)
31	11	nnnn0d 12565	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ₀)
32	31	nn0ge0d 12568	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 𝐷)
33		remsqsqrt 15307	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
34	30, 32, 33	syl2anc 595	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
35	30, 32	resqrtcld 15469	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℝ)
36	35	recnd 11237	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℂ)
37	36	sqvald 14179	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷)↑2) = ((√‘𝐷) · (√‘𝐷)))
38	12, 14, 20	divcan4d 11997	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = 𝐷)
39	34, 37, 38	3eqtr4rd 2815	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = ((√‘𝐷)↑2))
40	29, 39	oveq12d 7429	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))) = (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)))
41	9, 13, 17	divcld 11991	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℂ)
42		subsq 14246	. . . . . . . 8 ⊢ (((𝐴 / 𝐵) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
43	41, 36, 42	syl2anc 595	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
44	41, 36	addcld 11228	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ)
45	8	nnred 12248	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℝ)
46	45, 1	nndivred 12290	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℝ)
47	46, 35	resubcld 11642	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℝ)
48	47	recnd 11237	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℂ)
49	44, 48	mulcomd 11230	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
50	43, 49	eqtrd 2804	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
51	27, 40, 50	3eqtrd 2808	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
52	51	fveq2d 6886	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))))
53	52	oveq2d 7427	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
54	23, 26, 53	3eqtr3d 2812	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
55	48, 44	absmuld 15508	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
56	55	oveq2d 7427	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) = ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
57	48	abscld 15490	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ)
58	44	abscld 15490	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ)
59	57, 58	remulcld 11239	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
60	3, 59	remulcld 11239	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
61		2nn0 12521	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
62	61	nn0negzi 12633	. . . . . . . 8 ⊢ -2 ∈ ℤ
63	62	a1i 11	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → -2 ∈ ℤ)
64	2, 17, 63	reexpclzd 14285	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℝ)
65	64, 58	remulcld 11239	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
66	3, 65	remulcld 11239	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
67		1red 11209	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ∈ ℝ)
68		2re 12315	. . . . . . 7 ⊢ 2 ∈ ℝ
69	68	a1i 11	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 2 ∈ ℝ)
70	69, 35	remulcld 11239	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℝ)
71	67, 70	readdcld 11238	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
72		simpr 489	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2))
73	8	nngt0d 12285	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐴)
74	1	nngt0d 12285	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐵)
75	45, 2, 73, 74	divgt0d 12150	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐴 / 𝐵))
76	11	nngt0d 12285	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐷)
77		sqrtgt0 15309	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℝ ∧ 0 < 𝐷) → 0 < (√‘𝐷))
78	30, 76, 77	syl2anc 595	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (√‘𝐷))
79	46, 35, 75, 78	addgt0d 11789	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < ((𝐴 / 𝐵) + (√‘𝐷)))
80	79	gt0ne0d 11778	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0)
81		absgt0 15376	. . . . . . . . 9 ⊢ (((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ → (((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0 ↔ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
82	81	biimpa 481	. . . . . . . 8 ⊢ ((((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ ∧ ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
83	44, 80, 82	syl2anc 595	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
84		ltmul1 12065	. . . . . . 7 ⊢ (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ ∧ (𝐵↑-2) ∈ ℝ ∧ ((abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ ∧ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
85	57, 64, 58, 83, 84	syl112anc 1399	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
86	72, 85	mpbid 235	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
87	2, 17	sqgt0d 14286	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐵↑2))
88		ltmul2 12066	. . . . . 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 1399	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ↔ ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))))
90	86, 89	mpbid 235	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
91	13, 17, 63	expclzd 14187	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℂ)
92	58	recnd 11237	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ)
93		mulass 11188	. . . . . . . 8 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
94	93	eqcomd 2775	. . . . . . 7 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
95	14, 91, 92, 94	syl3anc 1396	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
96		expneg 14105	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑-2) = (1 / (𝐵↑2)))
97	13, 61, 96	sylancl 597	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) = (1 / (𝐵↑2)))
98	97	oveq2d 7427	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = ((𝐵↑2) · (1 / (𝐵↑2))))
99	14, 20	recidd 11986	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (1 / (𝐵↑2))) = 1)
100	98, 99	eqtrd 2804	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = 1)
101	100	oveq1d 7426	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
102	92	mullidd 11227	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
103	95, 101, 102	3eqtrd 2808	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
104	41, 36	addcomd 11412	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = ((√‘𝐷) + (𝐴 / 𝐵)))
105		ppncan 11500	. . . . . . . . . 10 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = ((√‘𝐷) + (𝐴 / 𝐵)))
106	105	eqcomd 2775	. . . . . . . . 9 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
107	36, 36, 41, 106	syl3anc 1396	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
108	36, 36	addcld 11228	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) ∈ ℂ)
109	108, 48	addcomd 11412	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))))
110		2times 12376	. . . . . . . . . . . 12 ⊢ ((√‘𝐷) ∈ ℂ → (2 · (√‘𝐷)) = ((√‘𝐷) + (√‘𝐷)))
111	110	eqcomd 2775	. . . . . . . . . . 11 ⊢ ((√‘𝐷) ∈ ℂ → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
112	36, 111	syl 18	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
113	112	oveq2d 7427	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
114	109, 113	eqtrd 2804	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
115	104, 107, 114	3eqtrd 2808	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
116	115	fveq2d 6886	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))))
117	47, 70	readdcld 11238	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℝ)
118	117	recnd 11237	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℂ)
119	118	abscld 15490	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ∈ ℝ)
120	70	recnd 11237	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℂ)
121	120	abscld 15490	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) ∈ ℝ)
122	57, 121	readdcld 11238	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ∈ ℝ)
123	48, 120	abstrid 15510	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))))
124		0le2 12343	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
125	124	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 2)
126	30, 32	sqrtge0d 15472	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (√‘𝐷))
127	69, 35, 125, 126	mulge0d 11791	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (2 · (√‘𝐷)))
128	70, 127	absidd 15474	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) = (2 · (√‘𝐷)))
129	128	oveq2d 7427	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))))
130	1	nnsqcld 14280	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℕ)
131	130	nnge1d 12284	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ≤ (𝐵↑2))
132		0lt1 11736	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 1)
134		lerec 12098	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((𝐵↑2) ∈ ℝ ∧ 0 < (𝐵↑2))) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
135	67, 133, 3, 87, 134	syl22anc 851	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
136	131, 135	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ (1 / 1))
137		1div1e1 11905	. . . . . . . . . . . . 13 ⊢ (1 / 1) = 1
138	136, 137	breqtrdi 5156	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ 1)
139	97, 138	eqbrtrd 5137	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ≤ 1)
140	57, 64, 67, 72, 139	ltletrd 11370	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < 1)
141	57, 67, 140	ltled 11358	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ≤ 1)
142	57, 67, 70, 141	leadd1dd 11828	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
143	129, 142	eqbrtrd 5137	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
144	119, 122, 71, 123, 143	letrd 11367	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
145	116, 144	eqbrtrd 5137	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
146	103, 145	eqbrtrd 5137	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ≤ (1 + (2 · (√‘𝐷))))
147	60, 66, 71, 90, 146	ltletrd 11370	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
148	56, 147	eqbrtrd 5137	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
149	54, 148	eqbrtrd 5137	1 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 class class class wbr 5113 ‘cfv 6537 (class class class)co 7411 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 ≤ cle 11244 − cmin 11441 -cneg 11442 / cdiv 11871 ℕcn 12233 2c2 12295 ℕ₀cn0 12504 ℤcz 12591 ↑cexp 14097 √csqrt 15284 abscabs 15285

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-sup 9402 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-n0 12505 df-z 12592 df-uz 12863 df-rp 13017 df-seq 14038 df-exp 14098 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287

This theorem is referenced by: pellexlem3 43484

W3C validator