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