divsqrtsumlem

		Ref	Expression
	Hypothesis	divsqrtsum.2	$⊢ F = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{\sqrt{n}}) - 2 \sqrt{x})$
	Assertion	divsqrtsumlem	$⊢ (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+}) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}}))$

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	$⊢ F = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} (\frac{1}{\sqrt{n}}) - 2 \sqrt{x})$
2		ioorp	$⊢ (0, +∞) = ℝ^{+}$
3	2	eqcomi	$⊢ ℝ^{+} = (0, +∞)$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ ⊤ \to 1 \in ℤ$
6		0red	$⊢ ⊤ \to 0 \in ℝ$
7		1re	$⊢ 1 \in ℝ$
8		0nn0	$⊢ 0 \in ℕ_{0}$
9	7 8	nn0addge2i	$⊢ 1 \leq 0 + 1$
10	9	a1i	$⊢ ⊤ \to 1 \leq 0 + 1$
11		2re	$⊢ 2 \in ℝ$
12		rpsqrtcl	$⊢ x \in ℝ^{+} \to \sqrt{x} \in ℝ^{+}$
13	12	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ^{+}$
14	13	rpred	$⊢ (⊤ \land x \in ℝ^{+}) \to \sqrt{x} \in ℝ$
15		remulcl	$⊢ (2 \in ℝ \land \sqrt{x} \in ℝ) \to 2 \sqrt{x} \in ℝ$
16	11 14 15	sylancr	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ$
17	13	rprecred	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{\sqrt{x}} \in ℝ$
18		nnrp	$⊢ x \in ℕ \to x \in ℝ^{+}$
19	18 17	sylan2	$⊢ (⊤ \land x \in ℕ) \to \frac{1}{\sqrt{x}} \in ℝ$
20		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
21	20	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
22	13	rpcnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \sqrt{x} \in ℂ$
23		2rp	$⊢ 2 \in ℝ^{+}$
24		rpmulcl	$⊢ (2 \in ℝ^{+} \land \sqrt{x} \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ^{+}$
25	23 13 24	sylancr	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \sqrt{x} \in ℝ^{+}$
26	25	rpreccld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{2 \sqrt{x}} \in ℝ^{+}$
27		dvsqrt	$⊢ \frac{d (x \in ℝ^{+}⟼ \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{x}})$
28	27	a1i	$⊢ ⊤ \to \frac{d (x \in ℝ^{+}⟼ \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{2 \sqrt{x}})$
29		2cnd	$⊢ ⊤ \to 2 \in ℂ$
30	21 22 26 28 29	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in ℝ^{+}⟼ 2 \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ 2 (\frac{1}{2 \sqrt{x}}))$
31		2cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 \in ℂ$
32		1cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℂ$
33	25	rpcnne0d	$⊢ (⊤ \land x \in ℝ^{+}) \to (2 \sqrt{x} \in ℂ \land 2 \sqrt{x} \neq 0)$
34		divass	$⊢ (2 \in ℂ \land 1 \in ℂ \land (2 \sqrt{x} \in ℂ \land 2 \sqrt{x} \neq 0)) \to \frac{2 \cdot 1}{2 \sqrt{x}} = 2 (\frac{1}{2 \sqrt{x}})$
35	31 32 33 34	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{2 \cdot 1}{2 \sqrt{x}} = 2 (\frac{1}{2 \sqrt{x}})$
36	13	rpcnne0d	$⊢ (⊤ \land x \in ℝ^{+}) \to (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)$
37		rpcnne0	$⊢ 2 \in ℝ^{+} \to (2 \in ℂ \land 2 \neq 0)$
38	23 37	mp1i	$⊢ (⊤ \land x \in ℝ^{+}) \to (2 \in ℂ \land 2 \neq 0)$
39		divcan5	$⊢ (1 \in ℂ \land (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot 1}{2 \sqrt{x}} = \frac{1}{\sqrt{x}}$
40	32 36 38 39	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{2 \cdot 1}{2 \sqrt{x}} = \frac{1}{\sqrt{x}}$
41	35 40	eqtr3d	$⊢ (⊤ \land x \in ℝ^{+}) \to 2 (\frac{1}{2 \sqrt{x}}) = \frac{1}{\sqrt{x}}$
42	41	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ 2 (\frac{1}{2 \sqrt{x}})) = (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}})$
43	30 42	eqtrd	$⊢ ⊤ \to \frac{d (x \in ℝ^{+}⟼ 2 \sqrt{x})}{d_{ℝ} x} = (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}})$
44		fveq2	$⊢ x = n \to \sqrt{x} = \sqrt{n}$
45	44	oveq2d	$⊢ x = n \to \frac{1}{\sqrt{x}} = \frac{1}{\sqrt{n}}$
46		simp3r	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to x \leq n$
47		simp2l	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to x \in ℝ^{+}$
48	47	rprege0d	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to (x \in ℝ \land 0 \leq x)$
49		simp2r	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to n \in ℝ^{+}$
50	49	rprege0d	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to (n \in ℝ \land 0 \leq n)$
51		sqrtle	$⊢ ((x \in ℝ \land 0 \leq x) \land (n \in ℝ \land 0 \leq n)) \to (x \leq n \leftrightarrow \sqrt{x} \leq \sqrt{n})$
52	48 50 51	syl2anc	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to (x \leq n \leftrightarrow \sqrt{x} \leq \sqrt{n})$
53	46 52	mpbid	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to \sqrt{x} \leq \sqrt{n}$
54	47	rpsqrtcld	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to \sqrt{x} \in ℝ^{+}$
55	49	rpsqrtcld	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to \sqrt{n} \in ℝ^{+}$
56	54 55	lerecd	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to (\sqrt{x} \leq \sqrt{n} \leftrightarrow \frac{1}{\sqrt{n}} \leq \frac{1}{\sqrt{x}})$
57	53 56	mpbid	$⊢ (⊤ \land (x \in ℝ^{+} \land n \in ℝ^{+}) \land (0 \leq x \land x \leq n)) \to \frac{1}{\sqrt{n}} \leq \frac{1}{\sqrt{x}}$
58		sqrtlim	$⊢ (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}}) \underset{ℝ}{⇝} 0$
59	58	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{\sqrt{x}}) \underset{ℝ}{⇝} 0$
60		fveq2	$⊢ x = A \to \sqrt{x} = \sqrt{A}$
61	60	oveq2d	$⊢ x = A \to \frac{1}{\sqrt{x}} = \frac{1}{\sqrt{A}}$
62	3 4 5 6 10 6 16 17 19 43 45 57 1 59 61	dvfsumrlim3	$⊢ ⊤ \to (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land 0 \leq A) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}}))$
63	62	simp1d	$⊢ ⊤ \to F : ℝ^{+} ⟶ ℝ$
64	63	mptru	$⊢ F : ℝ^{+} ⟶ ℝ$
65	62	simp2d	$⊢ ⊤ \to F \in dom \underset{ℝ}{⇝}$
66	65	mptru	$⊢ F \in dom \underset{ℝ}{⇝}$
67		rpge0	$⊢ A \in ℝ^{+} \to 0 \leq A$
68	67	adantl	$⊢ (F \underset{ℝ}{⇝} L \land A \in ℝ^{+}) \to 0 \leq A$
69	62	simp3d	$⊢ ⊤ \to ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land 0 \leq A) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}})$
70	69	mptru	$⊢ (F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land 0 \leq A) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}}$
71	68 70	mpd3an3	$⊢ (F \underset{ℝ}{⇝} L \land A \in ℝ^{+}) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}}$
72	64 66 71	3pm3.2i	$⊢ (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+}) \to \|F (A) - L\| \leq \frac{1}{\sqrt{A}}))$

Metamath Proof Explorer

Theorem divsqrtsumlem

Proof