gamcvg - Metamath Proof Explorer

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

Theorem gamcvg 25733

Description: The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.)

**Hypotheses**
Ref	Expression
lgamcvg.g	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
lgamcvg.a	⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))

**Assertion**
Ref	Expression
gamcvg	⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴))

Distinct variable groups: 𝐴,𝑚 𝜑,𝑚 Allowed substitution hint: 𝐺(𝑚)

Proof of Theorem gamcvg Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 12314	. . 3 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12045	. . 3 ⊢ (𝜑 → 1 ∈ ℤ)
3		efcn 25130	. . . 4 ⊢ exp ∈ (ℂ–cn→ℂ)
4	3	a1i 11	. . 3 ⊢ (𝜑 → exp ∈ (ℂ–cn→ℂ))
5		lgamcvg.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
6	5	eldifad 3871	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℂ)
7	6	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴 ∈ ℂ)
8		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
9	8	peano2nnd 11684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℕ)
10	9	nnrpd 12463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℝ⁺)
11	8	nnrpd 12463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ⁺)
12	10, 11	rpdivcld 12482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) / 𝑚) ∈ ℝ⁺)
13	12	relogcld 25306	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (log‘((𝑚 + 1) / 𝑚)) ∈ ℝ)
14	13	recnd 10700	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (log‘((𝑚 + 1) / 𝑚)) ∈ ℂ)
15	7, 14	mulcld 10692	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) ∈ ℂ)
16	8	nncnd 11683	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
17	8	nnne0d 11717	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ≠ 0)
18	7, 16, 17	divcld 11447	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐴 / 𝑚) ∈ ℂ)
19		1cnd 10667	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 1 ∈ ℂ)
20	18, 19	addcld 10691	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐴 / 𝑚) + 1) ∈ ℂ)
21	5	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
22	21, 8	dmgmdivn0 25705	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐴 / 𝑚) + 1) ≠ 0)
23	20, 22	logcld 25254	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (log‘((𝐴 / 𝑚) + 1)) ∈ ℂ)
24	15, 23	subcld 11028	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) ∈ ℂ)
25		lgamcvg.g	. . . . . 6 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
26	24, 25	fmptd 6870	. . . . 5 ⊢ (𝜑 → 𝐺:ℕ⟶ℂ)
27	26	ffvelrnda 6843	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℂ)
28	1, 2, 27	serf 13441	. . 3 ⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℂ)
29	25, 5	lgamcvg 25731	. . 3 ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))
30		lgamcl 25718	. . . . 5 ⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘𝐴) ∈ ℂ)
31	5, 30	syl 17	. . . 4 ⊢ (𝜑 → (log Γ‘𝐴) ∈ ℂ)
32	5	dmgmn0 25703	. . . . 5 ⊢ (𝜑 → 𝐴 ≠ 0)
33	6, 32	logcld 25254	. . . 4 ⊢ (𝜑 → (log‘𝐴) ∈ ℂ)
34	31, 33	addcld 10691	. . 3 ⊢ (𝜑 → ((log Γ‘𝐴) + (log‘𝐴)) ∈ ℂ)
35	1, 2, 4, 28, 29, 34	climcncf 23594	. 2 ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ (exp‘((log Γ‘𝐴) + (log‘𝐴))))
36		efadd 15488	. . . 4 ⊢ (((log Γ‘𝐴) ∈ ℂ ∧ (log‘𝐴) ∈ ℂ) → (exp‘((log Γ‘𝐴) + (log‘𝐴))) = ((exp‘(log Γ‘𝐴)) · (exp‘(log‘𝐴))))
37	31, 33, 36	syl2anc 588	. . 3 ⊢ (𝜑 → (exp‘((log Γ‘𝐴) + (log‘𝐴))) = ((exp‘(log Γ‘𝐴)) · (exp‘(log‘𝐴))))
38		eflgam 25722	. . . . 5 ⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴))
39	5, 38	syl 17	. . . 4 ⊢ (𝜑 → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴))
40		eflog 25260	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (exp‘(log‘𝐴)) = 𝐴)
41	6, 32, 40	syl2anc 588	. . . 4 ⊢ (𝜑 → (exp‘(log‘𝐴)) = 𝐴)
42	39, 41	oveq12d 7169	. . 3 ⊢ (𝜑 → ((exp‘(log Γ‘𝐴)) · (exp‘(log‘𝐴))) = ((Γ‘𝐴) · 𝐴))
43	37, 42	eqtrd 2794	. 2 ⊢ (𝜑 → (exp‘((log Γ‘𝐴) + (log‘𝐴))) = ((Γ‘𝐴) · 𝐴))
44	35, 43	breqtrd 5059	1 ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1539 ∈ wcel 2112 ≠ wne 2952 ∖ cdif 3856 class class class wbr 5033 ↦ cmpt 5113 ∘ ccom 5529 ‘cfv 6336 (class class class)co 7151 ℂcc 10566 0cc0 10568 1c1 10569 + caddc 10571 · cmul 10573 − cmin 10901 / cdiv 11328 ℕcn 11667 ℤcz 12013 seqcseq 13411 ⇝ cli 14882 expce 15456 –cn→ccncf 23570 logclog 25238 log Γclgam 25693 Γcgam 25694

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5157 ax-sep 5170 ax-nul 5177 ax-pow 5235 ax-pr 5299 ax-un 7460 ax-inf2 9130 ax-cnex 10624 ax-resscn 10625 ax-1cn 10626 ax-icn 10627 ax-addcl 10628 ax-addrcl 10629 ax-mulcl 10630 ax-mulrcl 10631 ax-mulcom 10632 ax-addass 10633 ax-mulass 10634 ax-distr 10635 ax-i2m1 10636 ax-1ne0 10637 ax-1rid 10638 ax-rnegex 10639 ax-rrecex 10640 ax-cnre 10641 ax-pre-lttri 10642 ax-pre-lttrn 10643 ax-pre-ltadd 10644 ax-pre-mulgt0 10645 ax-pre-sup 10646 ax-addf 10647 ax-mulf 10648

This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-nel 3057 df-ral 3076 df-rex 3077 df-reu 3078 df-rmo 3079 df-rab 3080 df-v 3412 df-sbc 3698 df-csb 3807 df-dif 3862 df-un 3864 df-in 3866 df-ss 3876 df-pss 3878 df-nul 4227 df-if 4422 df-pw 4497 df-sn 4524 df-pr 4526 df-tp 4528 df-op 4530 df-uni 4800 df-int 4840 df-iun 4886 df-iin 4887 df-br 5034 df-opab 5096 df-mpt 5114 df-tr 5140 df-id 5431 df-eprel 5436 df-po 5444 df-so 5445 df-fr 5484 df-se 5485 df-we 5486 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6127 df-ord 6173 df-on 6174 df-lim 6175 df-suc 6176 df-iota 6295 df-fun 6338 df-fn 6339 df-f 6340 df-f1 6341 df-fo 6342 df-f1o 6343 df-fv 6344 df-isom 6345 df-riota 7109 df-ov 7154 df-oprab 7155 df-mpo 7156 df-of 7406 df-om 7581 df-1st 7694 df-2nd 7695 df-supp 7837 df-wrecs 7958 df-recs 8019 df-rdg 8057 df-1o 8113 df-2o 8114 df-oadd 8117 df-er 8300 df-map 8419 df-pm 8420 df-ixp 8481 df-en 8529 df-dom 8530 df-sdom 8531 df-fin 8532 df-fsupp 8860 df-fi 8901 df-sup 8932 df-inf 8933 df-oi 9000 df-dju 9356 df-card 9394 df-pnf 10708 df-mnf 10709 df-xr 10710 df-ltxr 10711 df-le 10712 df-sub 10903 df-neg 10904 df-div 11329 df-nn 11668 df-2 11730 df-3 11731 df-4 11732 df-5 11733 df-6 11734 df-7 11735 df-8 11736 df-9 11737 df-n0 11928 df-z 12014 df-dec 12131 df-uz 12276 df-q 12382 df-rp 12424 df-xneg 12541 df-xadd 12542 df-xmul 12543 df-ioo 12776 df-ioc 12777 df-ico 12778 df-icc 12779 df-fz 12933 df-fzo 13076 df-fl 13204 df-mod 13280 df-seq 13412 df-exp 13473 df-fac 13677 df-bc 13706 df-hash 13734 df-shft 14467 df-cj 14499 df-re 14500 df-im 14501 df-sqrt 14635 df-abs 14636 df-limsup 14869 df-clim 14886 df-rlim 14887 df-sum 15084 df-ef 15462 df-sin 15464 df-cos 15465 df-tan 15466 df-pi 15467 df-struct 16536 df-ndx 16537 df-slot 16538 df-base 16540 df-sets 16541 df-ress 16542 df-plusg 16629 df-mulr 16630 df-starv 16631 df-sca 16632 df-vsca 16633 df-ip 16634 df-tset 16635 df-ple 16636 df-ds 16638 df-unif 16639 df-hom 16640 df-cco 16641 df-rest 16747 df-topn 16748 df-0g 16766 df-gsum 16767 df-topgen 16768 df-pt 16769 df-prds 16772 df-xrs 16826 df-qtop 16831 df-imas 16832 df-xps 16834 df-mre 16908 df-mrc 16909 df-acs 16911 df-mgm 17911 df-sgrp 17960 df-mnd 17971 df-submnd 18016 df-mulg 18285 df-cntz 18507 df-cmn 18968 df-psmet 20151 df-xmet 20152 df-met 20153 df-bl 20154 df-mopn 20155 df-fbas 20156 df-fg 20157 df-cnfld 20160 df-top 21587 df-topon 21604 df-topsp 21626 df-bases 21639 df-cld 21712 df-ntr 21713 df-cls 21714 df-nei 21791 df-lp 21829 df-perf 21830 df-cn 21920 df-cnp 21921 df-haus 22008 df-cmp 22080 df-tx 22255 df-hmeo 22448 df-fil 22539 df-fm 22631 df-flim 22632 df-flf 22633 df-xms 23015 df-ms 23016 df-tms 23017 df-cncf 23572 df-limc 24558 df-dv 24559 df-ulm 25064 df-log 25240 df-cxp 25241 df-lgam 25696 df-gam 25697

This theorem is referenced by: gamcvg2 25737

W3C validator