Theorem divsqrtsumlem

Description: Lemma for divsqrsum and divsqrtsum2 . (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypothesis	divsqrtsum.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
Assertion	divsqrtsumlem	⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		divsqrtsum.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
2		ioorp	⊢ ( 0 (,) +∞ ) = ℝ+
3	2	eqcomi	⊢ ℝ+ = ( 0 (,) +∞ )
4		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
5		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
6		0red	⊢ ( ⊤ → 0 ∈ ℝ )
7		1re	⊢ 1 ∈ ℝ
8		0nn0	⊢ 0 ∈ ℕ0
9	7 8	nn0addge2i	⊢ 1 ≤ ( 0 + 1 )
10	9	a1i	⊢ ( ⊤ → 1 ≤ ( 0 + 1 ) )
11		2re	⊢ 2 ∈ ℝ
12		rpsqrtcl	⊢ ( 𝑥 ∈ ℝ+ → ( √ ‘ 𝑥 ) ∈ ℝ+ )
13	12	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
14	13	rpred	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ )
15		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ 𝑥 ) ∈ ℝ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ )
16	11 14 15	sylancr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ )
17	13	rprecred	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( √ ‘ 𝑥 ) ) ∈ ℝ )
18		nnrp	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ+ )
19	18 17	sylan2	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℕ ) → ( 1 / ( √ ‘ 𝑥 ) ) ∈ ℝ )
20		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
21	20	a1i	⊢ ( ⊤ → ℝ ∈ { ℝ , ℂ } )
22	13	rpcnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℂ )
23		2rp	⊢ 2 ∈ ℝ+
24		rpmulcl	⊢ ( ( 2 ∈ ℝ+ ∧ ( √ ‘ 𝑥 ) ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ+ )
25	23 13 24	sylancr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℝ+ )
26	25	rpreccld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ∈ ℝ+ )
27		dvsqrt	⊢ ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) )
28	27	a1i	⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) )
29		2cnd	⊢ ( ⊤ → 2 ∈ ℂ )
30	21 22 26 28 29	dvmptcmul	⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( √ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) ) )
31		2cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
32		1cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
33	25	rpcnne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℂ ∧ ( 2 · ( √ ‘ 𝑥 ) ) ≠ 0 ) )
34		divass	⊢ ( ( 2 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℂ ∧ ( 2 · ( √ ‘ 𝑥 ) ) ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 2 · ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) )
35	31 32 33 34	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 2 · ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) )
36	13	rpcnne0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) )
37		rpcnne0	⊢ ( 2 ∈ ℝ+ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
38	23 37	mp1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
39		divcan5	⊢ ( ( 1 ∈ ℂ ∧ ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 2 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
40	32 36 38 39	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 1 ) / ( 2 · ( √ ‘ 𝑥 ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
41	35 40	eqtr3d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) = ( 1 / ( √ ‘ 𝑥 ) ) )
42	41	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 1 / ( 2 · ( √ ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) )
43	30 42	eqtrd	⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( √ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) )
44		fveq2	⊢ ( 𝑥 = 𝑛 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝑛 ) )
45	44	oveq2d	⊢ ( 𝑥 = 𝑛 → ( 1 / ( √ ‘ 𝑥 ) ) = ( 1 / ( √ ‘ 𝑛 ) ) )
46		simp3r	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → 𝑥 ≤ 𝑛 )
47		simp2l	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → 𝑥 ∈ ℝ+ )
48	47	rprege0d	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
49		simp2r	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → 𝑛 ∈ ℝ+ )
50	49	rprege0d	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
51		sqrtle	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ∧ ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) ) → ( 𝑥 ≤ 𝑛 ↔ ( √ ‘ 𝑥 ) ≤ ( √ ‘ 𝑛 ) ) )
52	48 50 51	syl2anc	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( 𝑥 ≤ 𝑛 ↔ ( √ ‘ 𝑥 ) ≤ ( √ ‘ 𝑛 ) ) )
53	46 52	mpbid	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( √ ‘ 𝑥 ) ≤ ( √ ‘ 𝑛 ) )
54	47	rpsqrtcld	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
55	49	rpsqrtcld	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( √ ‘ 𝑛 ) ∈ ℝ+ )
56	54 55	lerecd	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( ( √ ‘ 𝑥 ) ≤ ( √ ‘ 𝑛 ) ↔ ( 1 / ( √ ‘ 𝑛 ) ) ≤ ( 1 / ( √ ‘ 𝑥 ) ) ) )
57	53 56	mpbid	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 ≤ 𝑛 ) ) → ( 1 / ( √ ‘ 𝑛 ) ) ≤ ( 1 / ( √ ‘ 𝑥 ) ) )
58		sqrtlim	⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 0
59	58	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 0 )
60		fveq2	⊢ ( 𝑥 = 𝐴 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝐴 ) )
61	60	oveq2d	⊢ ( 𝑥 = 𝐴 → ( 1 / ( √ ‘ 𝑥 ) ) = ( 1 / ( √ ‘ 𝐴 ) ) )
62	3 4 5 6 10 6 16 17 19 43 45 57 1 59 61	dvfsumrlim3	⊢ ( ⊤ → ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ 0 ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) ) )
63	62	simp1d	⊢ ( ⊤ → 𝐹 : ℝ+ ⟶ ℝ )
64	63	mptru	⊢ 𝐹 : ℝ+ ⟶ ℝ
65	62	simp2d	⊢ ( ⊤ → 𝐹 ∈ dom ⇝𝑟 )
66	65	mptru	⊢ 𝐹 ∈ dom ⇝𝑟
67		rpge0	⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )
68	67	adantl	⊢ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → 0 ≤ 𝐴 )
69	62	simp3d	⊢ ( ⊤ → ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ 0 ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) )
70	69	mptru	⊢ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ 0 ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) )
71	68 70	mpd3an3	⊢ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) )
72	64 66 71	3pm3.2i	⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) )