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 43290

Description: Lemma for pellex 43295. 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 1201	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℕ)
2	1	nnred 12184	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℝ)
3	2	resqcld 14082	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℝ)
4	2	sqge0d 14094	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (𝐵↑2))
5	3, 4	absidd 15380	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(𝐵↑2)) = (𝐵↑2))
6	5	eqcomd 2747	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) = (abs‘(𝐵↑2)))
7	6	oveq2d 7376	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
8		simpl2 1200	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℕ)
9	8	nncnd 12185	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℂ)
10	9	sqcld 14101	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴↑2) ∈ ℂ)
11		simpl1 1199	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ)
12	11	nncnd 12185	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℂ)
13	1	nncnd 12185	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ∈ ℂ)
14	13	sqcld 14101	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℂ)
15	12, 14	mulcld 11160	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐷 · (𝐵↑2)) ∈ ℂ)
16	10, 15	subcld 11500	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ∈ ℂ)
17	1	nnne0d 12222	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐵 ≠ 0)
18		sqne0 14080	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → ((𝐵↑2) ≠ 0 ↔ 𝐵 ≠ 0))
19	18	biimpar 479	. . . . . . 7 ⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵↑2) ≠ 0)
20	13, 17, 19	syl2anc 591	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ≠ 0)
21	16, 14, 20	absdivd 15415	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (abs‘(𝐵↑2))))
22	7, 21	eqtr4d 2779	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2)) = (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))))
23	22	oveq2d 7376	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))))
24	16	abscld 15396	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℝ)
25	24	recnd 11168	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) ∈ ℂ)
26	25, 14, 20	divcan2d 11928	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) / (𝐵↑2))) = (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))))
27	10, 15, 14, 20	divsubdird 11965	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))))
28	9, 13, 17	sqdivd 14116	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
29	28	eqcomd 2747	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴↑2) / (𝐵↑2)) = ((𝐴 / 𝐵)↑2))
30	11	nnred 12184	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℝ)
31	11	nnnn0d 12493	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐷 ∈ ℕ₀)
32	31	nn0ge0d 12496	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 𝐷)
33		remsqsqrt 15213	. . . . . . . . 9 ⊢ ((𝐷 ∈ ℝ ∧ 0 ≤ 𝐷) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
34	30, 32, 33	syl2anc 591	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) · (√‘𝐷)) = 𝐷)
35	30, 32	resqrtcld 15375	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℝ)
36	35	recnd 11168	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (√‘𝐷) ∈ ℂ)
37	36	sqvald 14100	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷)↑2) = ((√‘𝐷) · (√‘𝐷)))
38	12, 14, 20	divcan4d 11932	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = 𝐷)
39	34, 37, 38	3eqtr4rd 2787	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐷 · (𝐵↑2)) / (𝐵↑2)) = ((√‘𝐷)↑2))
40	29, 39	oveq12d 7378	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) / (𝐵↑2)) − ((𝐷 · (𝐵↑2)) / (𝐵↑2))) = (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)))
41	9, 13, 17	divcld 11926	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℂ)
42		subsq 14167	. . . . . . . 8 ⊢ (((𝐴 / 𝐵) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
43	41, 36, 42	syl2anc 591	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))))
44	41, 36	addcld 11159	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ)
45	8	nnred 12184	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 𝐴 ∈ ℝ)
46	45, 1	nndivred 12226	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐴 / 𝐵) ∈ ℝ)
47	46, 35	resubcld 11573	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℝ)
48	47	recnd 11168	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) − (√‘𝐷)) ∈ ℂ)
49	44, 48	mulcomd 11161	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) + (√‘𝐷)) · ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
50	43, 49	eqtrd 2776	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵)↑2) − ((√‘𝐷)↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
51	27, 40, 50	3eqtrd 2780	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)) = (((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))
52	51	fveq2d 6835	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))))
53	52	oveq2d 7376	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴↑2) − (𝐷 · (𝐵↑2))) / (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
54	23, 26, 53	3eqtr3d 2784	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) = ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))))
55	48, 44	absmuld 15414	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
56	55	oveq2d 7376	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) = ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
57	48	abscld 15396	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ)
58	44	abscld 15396	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ)
59	57, 58	remulcld 11170	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
60	3, 59	remulcld 11170	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
61		2nn0 12449	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
62	61	nn0negzi 12561	. . . . . . . 8 ⊢ -2 ∈ ℤ
63	62	a1i 11	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → -2 ∈ ℤ)
64	2, 17, 63	reexpclzd 14206	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℝ)
65	64, 58	remulcld 11170	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ∈ ℝ)
66	3, 65	remulcld 11170	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ∈ ℝ)
67		1red 11140	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ∈ ℝ)
68		2re 12250	. . . . . . 7 ⊢ 2 ∈ ℝ
69	68	a1i 11	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 2 ∈ ℝ)
70	69, 35	remulcld 11170	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℝ)
71	67, 70	readdcld 11169	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 + (2 · (√‘𝐷))) ∈ ℝ)
72		simpr 486	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2))
73	8	nngt0d 12221	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐴)
74	1	nngt0d 12221	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐵)
75	45, 2, 73, 74	divgt0d 12086	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐴 / 𝐵))
76	11	nngt0d 12221	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 𝐷)
77		sqrtgt0 15215	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ ℝ ∧ 0 < 𝐷) → 0 < (√‘𝐷))
78	30, 76, 77	syl2anc 591	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (√‘𝐷))
79	46, 35, 75, 78	addgt0d 11720	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < ((𝐴 / 𝐵) + (√‘𝐷)))
80	79	gt0ne0d 11709	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0)
81		absgt0 15282	. . . . . . . . 9 ⊢ (((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ → (((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0 ↔ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
82	81	biimpa 478	. . . . . . . 8 ⊢ ((((𝐴 / 𝐵) + (√‘𝐷)) ∈ ℂ ∧ ((𝐴 / 𝐵) + (√‘𝐷)) ≠ 0) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
83	44, 80, 82	syl2anc 591	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
84		ltmul1 12000	. . . . . . 7 ⊢ (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) ∈ ℝ ∧ (𝐵↑-2) ∈ ℝ ∧ ((abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℝ ∧ 0 < (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
85	57, 64, 58, 83, 84	syl112anc 1383	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2) ↔ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
86	72, 85	mpbid 234	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
87	2, 17	sqgt0d 14207	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < (𝐵↑2))
88		ltmul2 12001	. . . . . 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 1383	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) < ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) ↔ ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))))
90	86, 89	mpbid 234	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
91	13, 17, 63	expclzd 14108	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ∈ ℂ)
92	58	recnd 11168	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ)
93		mulass 11121	. . . . . . . 8 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))))
94	93	eqcomd 2747	. . . . . . 7 ⊢ (((𝐵↑2) ∈ ℂ ∧ (𝐵↑-2) ∈ ℂ ∧ (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ∈ ℂ) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
95	14, 91, 92, 94	syl3anc 1380	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
96		expneg 14026	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑-2) = (1 / (𝐵↑2)))
97	13, 61, 96	sylancl 593	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) = (1 / (𝐵↑2)))
98	97	oveq2d 7376	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = ((𝐵↑2) · (1 / (𝐵↑2))))
99	14, 20	recidd 11921	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (1 / (𝐵↑2))) = 1)
100	98, 99	eqtrd 2776	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (𝐵↑-2)) = 1)
101	100	oveq1d 7375	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐵↑2) · (𝐵↑-2)) · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))))
102	92	mullidd 11158	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 · (abs‘((𝐴 / 𝐵) + (√‘𝐷)))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
103	95, 101, 102	3eqtrd 2780	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) = (abs‘((𝐴 / 𝐵) + (√‘𝐷))))
104	41, 36	addcomd 11343	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = ((√‘𝐷) + (𝐴 / 𝐵)))
105		ppncan 11431	. . . . . . . . . 10 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = ((√‘𝐷) + (𝐴 / 𝐵)))
106	105	eqcomd 2747	. . . . . . . . 9 ⊢ (((√‘𝐷) ∈ ℂ ∧ (√‘𝐷) ∈ ℂ ∧ (𝐴 / 𝐵) ∈ ℂ) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
107	36, 36, 41, 106	syl3anc 1380	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (𝐴 / 𝐵)) = (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))))
108	36, 36	addcld 11159	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) ∈ ℂ)
109	108, 48	addcomd 11343	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))))
110		2times 12307	. . . . . . . . . . . 12 ⊢ ((√‘𝐷) ∈ ℂ → (2 · (√‘𝐷)) = ((√‘𝐷) + (√‘𝐷)))
111	110	eqcomd 2747	. . . . . . . . . . 11 ⊢ ((√‘𝐷) ∈ ℂ → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
112	36, 111	syl 17	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((√‘𝐷) + (√‘𝐷)) = (2 · (√‘𝐷)))
113	112	oveq2d 7376	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + ((√‘𝐷) + (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
114	109, 113	eqtrd 2776	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((√‘𝐷) + (√‘𝐷)) + ((𝐴 / 𝐵) − (√‘𝐷))) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
115	104, 107, 114	3eqtrd 2780	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐴 / 𝐵) + (√‘𝐷)) = (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))))
116	115	fveq2d 6835	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) = (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))))
117	47, 70	readdcld 11169	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℝ)
118	117	recnd 11168	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷))) ∈ ℂ)
119	118	abscld 15396	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ∈ ℝ)
120	70	recnd 11168	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (2 · (√‘𝐷)) ∈ ℂ)
121	120	abscld 15396	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) ∈ ℝ)
122	57, 121	readdcld 11169	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ∈ ℝ)
123	48, 120	abstrid 15416	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))))
124		0le2 12278	. . . . . . . . . . . 12 ⊢ 0 ≤ 2
125	124	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ 2)
126	30, 32	sqrtge0d 15378	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (√‘𝐷))
127	69, 35, 125, 126	mulge0d 11722	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 ≤ (2 · (√‘𝐷)))
128	70, 127	absidd 15380	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(2 · (√‘𝐷))) = (2 · (√‘𝐷)))
129	128	oveq2d 7376	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) = ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))))
130	1	nnsqcld 14201	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑2) ∈ ℕ)
131	130	nnge1d 12220	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 1 ≤ (𝐵↑2))
132		0lt1 11667	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
133	132	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → 0 < 1)
134		lerec 12034	. . . . . . . . . . . . . . 15 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((𝐵↑2) ∈ ℝ ∧ 0 < (𝐵↑2))) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
135	67, 133, 3, 87, 134	syl22anc 845	. . . . . . . . . . . . . 14 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 ≤ (𝐵↑2) ↔ (1 / (𝐵↑2)) ≤ (1 / 1)))
136	131, 135	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ (1 / 1))
137		1div1e1 11840	. . . . . . . . . . . . 13 ⊢ (1 / 1) = 1
138	136, 137	breqtrdi 5116	. . . . . . . . . . . 12 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (1 / (𝐵↑2)) ≤ 1)
139	97, 138	eqbrtrd 5097	. . . . . . . . . . 11 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (𝐵↑-2) ≤ 1)
140	57, 64, 67, 72, 139	ltletrd 11301	. . . . . . . . . 10 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < 1)
141	57, 67, 140	ltled 11289	. . . . . . . . 9 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) − (√‘𝐷))) ≤ 1)
142	57, 67, 70, 141	leadd1dd 11759	. . . . . . . 8 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (2 · (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
143	129, 142	eqbrtrd 5097	. . . . . . 7 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) + (abs‘(2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
144	119, 122, 71, 123, 143	letrd 11298	. . . . . 6 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) + (2 · (√‘𝐷)))) ≤ (1 + (2 · (√‘𝐷))))
145	116, 144	eqbrtrd 5097	. . . . 5 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴 / 𝐵) + (√‘𝐷))) ≤ (1 + (2 · (√‘𝐷))))
146	103, 145	eqbrtrd 5097	. . . 4 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((𝐵↑-2) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) ≤ (1 + (2 · (√‘𝐷))))
147	60, 66, 71, 90, 146	ltletrd 11301	. . 3 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · ((abs‘((𝐴 / 𝐵) − (√‘𝐷))) · (abs‘((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
148	56, 147	eqbrtrd 5097	. 2 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → ((𝐵↑2) · (abs‘(((𝐴 / 𝐵) − (√‘𝐷)) · ((𝐴 / 𝐵) + (√‘𝐷))))) < (1 + (2 · (√‘𝐷))))
149	54, 148	eqbrtrd 5097	1 ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 class class class wbr 5075 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 · cmul 11038 < clt 11174 ≤ cle 11175 − cmin 11372 -cneg 11373 / cdiv 11802 ℕcn 12169 2c2 12231 ℕ₀cn0 12432 ℤcz 12519 ↑cexp 14018 √csqrt 15190 abscabs 15191

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-sup 9349 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-seq 13959 df-exp 14019 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193

This theorem is referenced by: pellexlem3 43291

W3C validator