This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 / ( √ ‘ 𝐴 ) ) ) )