MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  emcllem5 Structured version   Visualization version   GIF version

Theorem emcllem5 24917
Description: Lemma for emcl 24920. The partial sums of the series 𝑇, which is used in the definition df-em 24910, is in fact the same as 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.)
Hypotheses
Ref Expression
emcl.1 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))
emcl.2 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))
emcl.3 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))
emcl.4 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))
Assertion
Ref Expression
emcllem5 𝐺 = seq1( + , 𝑇)
Distinct variable groups:   𝑚,𝐻   𝑚,𝑛,𝑇
Allowed substitution hints:   𝐹(𝑚,𝑛)   𝐺(𝑚,𝑛)   𝐻(𝑛)

Proof of Theorem emcllem5
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elfznn 12555 . . . . . . . . . . . . 13 (𝑚 ∈ (1...𝑛) → 𝑚 ∈ ℕ)
21adantl 473 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → 𝑚 ∈ ℕ)
32nncnd 11220 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → 𝑚 ∈ ℂ)
4 1cnd 10240 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → 1 ∈ ℂ)
52nnne0d 11249 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → 𝑚 ≠ 0)
63, 4, 3, 5divdird 11023 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((𝑚 + 1) / 𝑚) = ((𝑚 / 𝑚) + (1 / 𝑚)))
73, 5dividd 10983 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (𝑚 / 𝑚) = 1)
87oveq1d 6820 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((𝑚 / 𝑚) + (1 / 𝑚)) = (1 + (1 / 𝑚)))
96, 8eqtrd 2786 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((𝑚 + 1) / 𝑚) = (1 + (1 / 𝑚)))
109fveq2d 6348 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (log‘((𝑚 + 1) / 𝑚)) = (log‘(1 + (1 / 𝑚))))
11 peano2nn 11216 . . . . . . . . . . 11 (𝑚 ∈ ℕ → (𝑚 + 1) ∈ ℕ)
122, 11syl 17 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (𝑚 + 1) ∈ ℕ)
1312nnrpd 12055 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (𝑚 + 1) ∈ ℝ+)
142nnrpd 12055 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → 𝑚 ∈ ℝ+)
1513, 14relogdivd 24563 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (log‘((𝑚 + 1) / 𝑚)) = ((log‘(𝑚 + 1)) − (log‘𝑚)))
1610, 15eqtr3d 2788 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (log‘(1 + (1 / 𝑚))) = ((log‘(𝑚 + 1)) − (log‘𝑚)))
1716sumeq2dv 14624 . . . . . 6 (𝑛 ∈ ℕ → Σ𝑚 ∈ (1...𝑛)(log‘(1 + (1 / 𝑚))) = Σ𝑚 ∈ (1...𝑛)((log‘(𝑚 + 1)) − (log‘𝑚)))
18 fveq2 6344 . . . . . . 7 (𝑥 = 𝑚 → (log‘𝑥) = (log‘𝑚))
19 fveq2 6344 . . . . . . 7 (𝑥 = (𝑚 + 1) → (log‘𝑥) = (log‘(𝑚 + 1)))
20 fveq2 6344 . . . . . . 7 (𝑥 = 1 → (log‘𝑥) = (log‘1))
21 fveq2 6344 . . . . . . 7 (𝑥 = (𝑛 + 1) → (log‘𝑥) = (log‘(𝑛 + 1)))
22 nnz 11583 . . . . . . 7 (𝑛 ∈ ℕ → 𝑛 ∈ ℤ)
23 peano2nn 11216 . . . . . . . 8 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
24 nnuz 11908 . . . . . . . 8 ℕ = (ℤ‘1)
2523, 24syl6eleq 2841 . . . . . . 7 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ (ℤ‘1))
26 elfznn 12555 . . . . . . . . . . 11 (𝑥 ∈ (1...(𝑛 + 1)) → 𝑥 ∈ ℕ)
2726adantl 473 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℕ)
2827nnrpd 12055 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ (1...(𝑛 + 1))) → 𝑥 ∈ ℝ+)
2928relogcld 24560 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘𝑥) ∈ ℝ)
3029recnd 10252 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑥 ∈ (1...(𝑛 + 1))) → (log‘𝑥) ∈ ℂ)
3118, 19, 20, 21, 22, 25, 30telfsum2 14728 . . . . . 6 (𝑛 ∈ ℕ → Σ𝑚 ∈ (1...𝑛)((log‘(𝑚 + 1)) − (log‘𝑚)) = ((log‘(𝑛 + 1)) − (log‘1)))
32 log1 24523 . . . . . . . 8 (log‘1) = 0
3332oveq2i 6816 . . . . . . 7 ((log‘(𝑛 + 1)) − (log‘1)) = ((log‘(𝑛 + 1)) − 0)
3423nnrpd 12055 . . . . . . . . . 10 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℝ+)
3534relogcld 24560 . . . . . . . . 9 (𝑛 ∈ ℕ → (log‘(𝑛 + 1)) ∈ ℝ)
3635recnd 10252 . . . . . . . 8 (𝑛 ∈ ℕ → (log‘(𝑛 + 1)) ∈ ℂ)
3736subid1d 10565 . . . . . . 7 (𝑛 ∈ ℕ → ((log‘(𝑛 + 1)) − 0) = (log‘(𝑛 + 1)))
3833, 37syl5eq 2798 . . . . . 6 (𝑛 ∈ ℕ → ((log‘(𝑛 + 1)) − (log‘1)) = (log‘(𝑛 + 1)))
3917, 31, 383eqtrd 2790 . . . . 5 (𝑛 ∈ ℕ → Σ𝑚 ∈ (1...𝑛)(log‘(1 + (1 / 𝑚))) = (log‘(𝑛 + 1)))
4039oveq2d 6821 . . . 4 (𝑛 ∈ ℕ → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − Σ𝑚 ∈ (1...𝑛)(log‘(1 + (1 / 𝑚)))) = (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))
41 fzfid 12958 . . . . . 6 (𝑛 ∈ ℕ → (1...𝑛) ∈ Fin)
422nnrecred 11250 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (1 / 𝑚) ∈ ℝ)
4342recnd 10252 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (1 / 𝑚) ∈ ℂ)
44 1rp 12021 . . . . . . . . 9 1 ∈ ℝ+
4514rpreccld 12067 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (1 / 𝑚) ∈ ℝ+)
46 rpaddcl 12039 . . . . . . . . 9 ((1 ∈ ℝ+ ∧ (1 / 𝑚) ∈ ℝ+) → (1 + (1 / 𝑚)) ∈ ℝ+)
4744, 45, 46sylancr 698 . . . . . . . 8 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (1 + (1 / 𝑚)) ∈ ℝ+)
4847relogcld 24560 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (log‘(1 + (1 / 𝑚))) ∈ ℝ)
4948recnd 10252 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (log‘(1 + (1 / 𝑚))) ∈ ℂ)
5041, 43, 49fsumsub 14711 . . . . 5 (𝑛 ∈ ℕ → Σ𝑚 ∈ (1...𝑛)((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))) = (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − Σ𝑚 ∈ (1...𝑛)(log‘(1 + (1 / 𝑚)))))
51 oveq2 6813 . . . . . . . . 9 (𝑛 = 𝑚 → (1 / 𝑛) = (1 / 𝑚))
5251oveq2d 6821 . . . . . . . . . 10 (𝑛 = 𝑚 → (1 + (1 / 𝑛)) = (1 + (1 / 𝑚)))
5352fveq2d 6348 . . . . . . . . 9 (𝑛 = 𝑚 → (log‘(1 + (1 / 𝑛))) = (log‘(1 + (1 / 𝑚))))
5451, 53oveq12d 6823 . . . . . . . 8 (𝑛 = 𝑚 → ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))) = ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))))
55 emcl.4 . . . . . . . 8 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))
56 ovex 6833 . . . . . . . 8 ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))) ∈ V
5754, 55, 56fvmpt 6436 . . . . . . 7 (𝑚 ∈ ℕ → (𝑇𝑚) = ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))))
582, 57syl 17 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → (𝑇𝑚) = ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))))
59 id 22 . . . . . . 7 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ)
6059, 24syl6eleq 2841 . . . . . 6 (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ‘1))
6142, 48resubcld 10642 . . . . . . 7 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))) ∈ ℝ)
6261recnd 10252 . . . . . 6 ((𝑛 ∈ ℕ ∧ 𝑚 ∈ (1...𝑛)) → ((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))) ∈ ℂ)
6358, 60, 62fsumser 14652 . . . . 5 (𝑛 ∈ ℕ → Σ𝑚 ∈ (1...𝑛)((1 / 𝑚) − (log‘(1 + (1 / 𝑚)))) = (seq1( + , 𝑇)‘𝑛))
6450, 63eqtr3d 2788 . . . 4 (𝑛 ∈ ℕ → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − Σ𝑚 ∈ (1...𝑛)(log‘(1 + (1 / 𝑚)))) = (seq1( + , 𝑇)‘𝑛))
6540, 64eqtr3d 2788 . . 3 (𝑛 ∈ ℕ → (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))) = (seq1( + , 𝑇)‘𝑛))
6665mpteq2ia 4884 . 2 (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1)))) = (𝑛 ∈ ℕ ↦ (seq1( + , 𝑇)‘𝑛))
67 emcl.2 . 2 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))
68 1z 11591 . . . . 5 1 ∈ ℤ
69 seqfn 12999 . . . . 5 (1 ∈ ℤ → seq1( + , 𝑇) Fn (ℤ‘1))
7068, 69ax-mp 5 . . . 4 seq1( + , 𝑇) Fn (ℤ‘1)
7124fneq2i 6139 . . . 4 (seq1( + , 𝑇) Fn ℕ ↔ seq1( + , 𝑇) Fn (ℤ‘1))
7270, 71mpbir 221 . . 3 seq1( + , 𝑇) Fn ℕ
73 dffn5 6395 . . 3 (seq1( + , 𝑇) Fn ℕ ↔ seq1( + , 𝑇) = (𝑛 ∈ ℕ ↦ (seq1( + , 𝑇)‘𝑛)))
7472, 73mpbi 220 . 2 seq1( + , 𝑇) = (𝑛 ∈ ℕ ↦ (seq1( + , 𝑇)‘𝑛))
7566, 67, 743eqtr4i 2784 1 𝐺 = seq1( + , 𝑇)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1624  wcel 2131  cmpt 4873   Fn wfn 6036  cfv 6041  (class class class)co 6805  0cc0 10120  1c1 10121   + caddc 10123  cmin 10450   / cdiv 10868  cn 11204  cz 11561  cuz 11871  +crp 12017  ...cfz 12511  seqcseq 12987  Σcsu 14607  logclog 24492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-supp 7456  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ioc 12365  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-mod 12855  df-seq 12988  df-exp 13047  df-fac 13247  df-bc 13276  df-hash 13304  df-shft 13998  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-limsup 14393  df-clim 14410  df-rlim 14411  df-sum 14608  df-ef 14989  df-sin 14991  df-cos 14992  df-pi 14994  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-sca 16151  df-vsca 16152  df-ip 16153  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-hom 16160  df-cco 16161  df-rest 16277  df-topn 16278  df-0g 16296  df-gsum 16297  df-topgen 16298  df-pt 16299  df-prds 16302  df-xrs 16356  df-qtop 16361  df-imas 16362  df-xps 16364  df-mre 16440  df-mrc 16441  df-acs 16443  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-submnd 17529  df-mulg 17734  df-cntz 17942  df-cmn 18387  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-fbas 19937  df-fg 19938  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-cld 21017  df-ntr 21018  df-cls 21019  df-nei 21096  df-lp 21134  df-perf 21135  df-cn 21225  df-cnp 21226  df-haus 21313  df-tx 21559  df-hmeo 21752  df-fil 21843  df-fm 21935  df-flim 21936  df-flf 21937  df-xms 22318  df-ms 22319  df-tms 22320  df-cncf 22874  df-limc 23821  df-dv 23822  df-log 24494
This theorem is referenced by:  emcllem6  24918
  Copyright terms: Public domain W3C validator