Theorem amgmwlem 42357

Description: Weighted version of amgmlem 24516. (Contributed by Kunhao Zheng, 19-Jun-2021.)

Hypotheses

Ref	Expression
amgmwlem.0	⊢ 𝑀 = (mulGrp‘ℂfld)
amgmwlem.1	⊢ (𝜑 → 𝐴 ∈ Fin)
amgmwlem.2	⊢ (𝜑 → 𝐴 ≠ ∅)
amgmwlem.3	⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)
amgmwlem.4	⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)
amgmwlem.5	⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)

Assertion

Ref	Expression
amgmwlem	⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))

Proof of Theorem amgmwlem

Dummy variables 𝑎 𝑏 𝑠 𝑢 𝑣 𝑘 𝑦 𝑤 𝑥 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		amgmwlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
2		amgmwlem.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)
3	2	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
4		amgmwlem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:𝐴⟶ℝ+)
5	4	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
6	5	rpred 11748	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ)
7	3, 6	rpcxpcld 24276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)) ∈ ℝ+)
8	7	relogcld 24173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ)
9	8	recnd 9947	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℂ)
10	1, 9	gsumfsum 19632	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
11	2	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
12	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
13	12	rpred 11748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ)
14	11, 13	rpcxpcld 24276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)) ∈ ℝ+)
15	14	relogcld 24173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ)
16	15	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℂ)
17	16	negnegd 10262	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
18	17	sumeq2dv 14281	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
19	2	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
20	4	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
21	20	rpred 11748	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ)
22	19, 21	rpcxpcld 24276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)) ∈ ℝ+)
23	22	relogcld 24173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ)
24	23	renegcld 10336	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℝ)
25	24	recnd 9947	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) ∈ ℂ)
26	1, 25	fsumneg 14361	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
27	2	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
28	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
29	28	rpred 11748	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ)
30	27, 29	logcxpd 24277	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = ((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
31	30	negeqd 10154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
32	31	sumeq2dv 14281	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
33	32	negeqd 10154	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
34	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
35	34	rpcnd 11750	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℂ)
36	2	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
37	36	relogcld 24173	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
38	37	recnd 9947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ)
39	35, 38	mulneg2d 10363	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
40	39	eqcomd 2616	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
41	40	sumeq2dv 14281	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
42	41	negeqd 10154	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
43	26, 33, 42	3eqtrd 2648	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
44	10, 18, 43	3eqtr2rd 2651	. . . . . 6 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))))
45	4	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
46		negex 10158	. . . . . . . . . . 11 ⊢ -(log‘(𝐹‘𝑘)) ∈ V
47	46	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V)
48	4	feqmptd 6159	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
49		eqidd 2611	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
50	1, 45, 47, 48, 49	offval2 6812	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))))
51	50	oveq2d 6565	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))))
52	4	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
53	52	rpcnd 11750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℂ)
54	2	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
55	54	relogcld 24173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
56	55	recnd 9947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ)
57	56	negcld 10258	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ)
58	53, 57	mulcld 9939	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) ∈ ℂ)
59	1, 58	gsumfsum 19632	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
60	51, 59	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
61	60	negeqd 10154	. . . . . 6 ⊢ (𝜑 → -(ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
62		relogf1o 24117	. . . . . . . . . 10 ⊢ (log ↾ ℝ+):ℝ+–1-1-onto→ℝ
63		f1of 6050	. . . . . . . . . 10 ⊢ ((log ↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
64	62, 63	ax-mp 5	. . . . . . . . 9 ⊢ (log ↾ ℝ+):ℝ+⟶ℝ
65		rpre 11715	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
66	65	anim2i 591	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
67	66	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
68		rpcxpcl 24222	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
69	67, 68	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
70		inidm 3784	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝐴) = 𝐴
71	69, 2, 4, 1, 1, 70	off 6810	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
72		fcompt 6306	. . . . . . . . 9 ⊢ (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘))))
73	64, 71, 72	sylancr 694	. . . . . . . 8 ⊢ (𝜑 → ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘))))
74		rpre 11715	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
75	74	anim2i 591	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
76	75	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
77		rpcxpcl 24222	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
78	76, 77	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
79		inidm 3784	. . . . . . . . . . . . 13 ⊢ (𝐴 ∩ 𝐴) = 𝐴
80	78, 2, 4, 1, 1, 79	off 6810	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
81	80	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘) ∈ ℝ+)
82		fvres 6117	. . . . . . . . . . 11 ⊢ (((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘) ∈ ℝ+ → ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)))
83	81, 82	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)))
84	2	ffnd 5959	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝐴)
85	4	ffnd 5959	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 Fn 𝐴)
86		inidm 3784	. . . . . . . . . . . 12 ⊢ (𝐴 ∩ 𝐴) = 𝐴
87		eqidd 2611	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) = (𝐹‘𝑘))
88		eqidd 2611	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) = (𝑊‘𝑘))
89	84, 85, 1, 1, 86, 87, 88	ofval 6804	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘) = ((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))
90	89	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
91	83, 90	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))
92	91	mpteq2dva 4672	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ+)‘((𝐹 ∘𝑓 ↑𝑐𝑊)‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))))
93	73, 92	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘)))))
94	93	oveq2d 6565	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑𝑐(𝑊‘𝑘))))))
95	44, 61, 94	3eqtr4d 2654	. . . . 5 ⊢ (𝜑 → -(ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))))
96		amgmwlem.0	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘ℂfld)
97	96	oveq1i 6559	. . . . . . . . . . . 12 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
98	97	rpmsubg 19629	. . . . . . . . . . 11 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
99		subgsubm 17439	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
100	98, 99	ax-mp 5	. . . . . . . . . 10 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
101		cnring 19587	. . . . . . . . . . 11 ⊢ ℂfld ∈ Ring
102		cnfldbas 19571	. . . . . . . . . . . . 13 ⊢ ℂ = (Base‘ℂfld)
103		cnfld0 19589	. . . . . . . . . . . . 13 ⊢ 0 = (0g‘ℂfld)
104		cndrng 19594	. . . . . . . . . . . . 13 ⊢ ℂfld ∈ DivRing
105	102, 103, 104	drngui 18576	. . . . . . . . . . . 12 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
106	105, 96	unitsubm 18493	. . . . . . . . . . 11 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
107		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
108	107	subsubm 17180	. . . . . . . . . . 11 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
109	101, 106, 108	mp2b 10	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
110	100, 109	mpbi 219	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
111	110	simpli 473	. . . . . . . 8 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
112		eqid 2610	. . . . . . . . 9 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
113	112	submbas 17178	. . . . . . . 8 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀 ↾s ℝ+)))
114	111, 113	ax-mp 5	. . . . . . 7 ⊢ ℝ+ = (Base‘(𝑀 ↾s ℝ+))
115		cnfld1 19590	. . . . . . . . 9 ⊢ 1 = (1r‘ℂfld)
116	96, 115	ringidval 18326	. . . . . . . 8 ⊢ 1 = (0g‘𝑀)
117	96	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
118	117	rpmsubg 19629	. . . . . . . . . . . 12 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
119		subgsubm 17439	. . . . . . . . . . . 12 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
120	118, 119	ax-mp 5	. . . . . . . . . . 11 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
121	102, 103, 104	drngui 18576	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
122	121, 96	unitsubm 18493	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
123		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
124	123	subsubm 17180	. . . . . . . . . . . 12 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
125	101, 122, 124	mp2b 10	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
126	120, 125	mpbi 219	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
127	126	simpli 473	. . . . . . . . 9 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
128		eqid 2610	. . . . . . . . . 10 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
129		eqid 2610	. . . . . . . . . 10 ⊢ (0g‘𝑀) = (0g‘𝑀)
130	128, 129	subm0 17179	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → (0g‘𝑀) = (0g‘(𝑀 ↾s ℝ+)))
131	127, 130	ax-mp 5	. . . . . . . 8 ⊢ (0g‘𝑀) = (0g‘(𝑀 ↾s ℝ+))
132	116, 131	eqtri 2632	. . . . . . 7 ⊢ 1 = (0g‘(𝑀 ↾s ℝ+))
133		cncrng 19586	. . . . . . . . 9 ⊢ ℂfld ∈ CRing
134	96	crngmgp 18378	. . . . . . . . 9 ⊢ (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
135	133, 134	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ CMnd)
136	96	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
137	136	rpmsubg 19629	. . . . . . . . . . . 12 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
138		subgsubm 17439	. . . . . . . . . . . 12 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
139	137, 138	ax-mp 5	. . . . . . . . . . 11 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
140	102, 103, 104	drngui 18576	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
141	140, 96	unitsubm 18493	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
142		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
143	142	subsubm 17180	. . . . . . . . . . . 12 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
144	101, 141, 143	mp2b 10	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
145	139, 144	mpbi 219	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
146	145	simpli 473	. . . . . . . . 9 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
147		eqid 2610	. . . . . . . . . 10 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
148	147	submmnd 17177	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+) ∈ Mnd)
149	146, 148	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ↾s ℝ+) ∈ Mnd)
150		eqid 2610	. . . . . . . . 9 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
151	150	subcmn 18065	. . . . . . . 8 ⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+) ∈ CMnd)
152	135, 149, 151	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (𝑀 ↾s ℝ+) ∈ CMnd)
153		resubdrg 19773	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
154	153	simpli 473	. . . . . . . . 9 ⊢ ℝ ∈ (SubRing‘ℂfld)
155		df-refld 19770	. . . . . . . . . 10 ⊢ ℝfld = (ℂfld ↾s ℝ)
156	155	subrgring 18606	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
157	154, 156	ax-mp 5	. . . . . . . 8 ⊢ ℝfld ∈ Ring
158		ringmnd 18379	. . . . . . . 8 ⊢ (ℝfld ∈ Ring → ℝfld ∈ Mnd)
159	157, 158	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ℝfld ∈ Mnd)
160	96	oveq1i 6559	. . . . . . . . . 10 ⊢ (𝑀 ↾s ℝ+) = ((mulGrp‘ℂfld) ↾s ℝ+)
161	160	reloggim 24149	. . . . . . . . 9 ⊢ (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpIso ℝfld)
162		gimghm 17529	. . . . . . . . 9 ⊢ ((log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld))
163	161, 162	ax-mp 5	. . . . . . . 8 ⊢ (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld)
164		ghmmhm 17493	. . . . . . . 8 ⊢ ((log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) MndHom ℝfld))
165	163, 164	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) MndHom ℝfld))
166		rpre 11715	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
167	166	anim2i 591	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
168	167	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
169		rpcxpcl 24222	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
170	168, 169	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
171		inidm 3784	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐴) = 𝐴
172	170, 2, 4, 1, 1, 171	off 6810	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
173		rpre 11715	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
174	173	anim2i 591	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
175	174	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
176		rpcxpcl 24222	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
177	175, 176	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
178		inidm 3784	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐴) = 𝐴
179	177, 2, 4, 1, 1, 178	off 6810	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
180		1red 9934	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
181	179, 1, 180	fdmfifsupp 8168	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊) finSupp 1)
182	114, 132, 152, 159, 1, 165, 172, 181	gsummhm 18161	. . . . . 6 ⊢ (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀 ↾s ℝ+) Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
183	153	simpli 473	. . . . . . . . . 10 ⊢ ℝ ∈ (SubRing‘ℂfld)
184		subrgsubg 18609	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
185	183, 184	ax-mp 5	. . . . . . . . 9 ⊢ ℝ ∈ (SubGrp‘ℂfld)
186		subgsubm 17439	. . . . . . . . 9 ⊢ (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
187	185, 186	ax-mp 5	. . . . . . . 8 ⊢ ℝ ∈ (SubMnd‘ℂfld)
188	187	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
189		f1of 6050	. . . . . . . . 9 ⊢ ((log ↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
190	62, 189	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
191		rpre 11715	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
192	191	anim2i 591	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
193	192	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
194		rpcxpcl 24222	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
195	193, 194	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
196		inidm 3784	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐴) = 𝐴
197	195, 2, 4, 1, 1, 196	off 6810	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
198		fco 5971	. . . . . . . 8 ⊢ (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊)):𝐴⟶ℝ)
199	190, 197, 198	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊)):𝐴⟶ℝ)
200	1, 188, 199, 155	gsumsubm 17196	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))) = (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))))
201	96	oveq1i 6559	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
202	201	rpmsubg 19629	. . . . . . . . . . . 12 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
203		subgsubm 17439	. . . . . . . . . . . 12 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
204	202, 203	ax-mp 5	. . . . . . . . . . 11 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
205	102, 103, 104	drngui 18576	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
206	205, 96	unitsubm 18493	. . . . . . . . . . . 12 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
207		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
208	207	subsubm 17180	. . . . . . . . . . . 12 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
209	101, 206, 208	mp2b 10	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
210	204, 209	mpbi 219	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
211	210	simpli 473	. . . . . . . . 9 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
212	211	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
213		rpre 11715	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
214	213	anim2i 591	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
215	214	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
216		rpcxpcl 24222	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
217	215, 216	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
218		inidm 3784	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐴) = 𝐴
219	217, 2, 4, 1, 1, 218	off 6810	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
220		eqid 2610	. . . . . . . 8 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
221	1, 212, 219, 220	gsumsubm 17196	. . . . . . 7 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) = ((𝑀 ↾s ℝ+) Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))
222	221	fveq2d 6107	. . . . . 6 ⊢ (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀 ↾s ℝ+) Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
223	182, 200, 222	3eqtr4d 2654	. . . . 5 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹 ∘𝑓 ↑𝑐𝑊))) = ((log ↾ ℝ+)‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
224	96, 115	ringidval 18326	. . . . . . 7 ⊢ 1 = (0g‘𝑀)
225	96	crngmgp 18378	. . . . . . . 8 ⊢ (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
226	133, 225	mp1i 13	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ CMnd)
227	96	oveq1i 6559	. . . . . . . . . . . 12 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
228	227	rpmsubg 19629	. . . . . . . . . . 11 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
229		subgsubm 17439	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
230	228, 229	ax-mp 5	. . . . . . . . . 10 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
231	102, 103, 104	drngui 18576	. . . . . . . . . . . 12 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
232	231, 96	unitsubm 18493	. . . . . . . . . . 11 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
233		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
234	233	subsubm 17180	. . . . . . . . . . 11 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
235	101, 232, 234	mp2b 10	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
236	230, 235	mpbi 219	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
237	236	simpli 473	. . . . . . . 8 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
238	237	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
239		rpre 11715	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
240	239	anim2i 591	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
241	240	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
242		rpcxpcl 24222	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
243	241, 242	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
244		inidm 3784	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐴) = 𝐴
245	243, 2, 4, 1, 1, 244	off 6810	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
246		rpre 11715	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
247	246	anim2i 591	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
248	247	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
249		rpcxpcl 24222	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
250	248, 249	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
251		inidm 3784	. . . . . . . . 9 ⊢ (𝐴 ∩ 𝐴) = 𝐴
252	250, 2, 4, 1, 1, 251	off 6810	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
253		1red 9934	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
254	252, 1, 253	fdmfifsupp 8168	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊) finSupp 1)
255	224, 226, 1, 238, 245, 254	gsumsubmcl 18142	. . . . . 6 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ∈ ℝ+)
256		fvres 6117	. . . . . 6 ⊢ ((𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ∈ ℝ+ → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) = (log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
257	255, 256	syl 17	. . . . 5 ⊢ (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) = (log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
258	95, 223, 257	3eqtrd 2648	. . . 4 ⊢ (𝜑 → -(ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))))
259		simprl 790	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
260	259	rpcnd 11750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
261		simprr 792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
262	261	rpcnd 11750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
263	260, 262	mulcomd 9940	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
264	1, 4, 2, 263	caofcom 6827	. . . . . . . 8 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝐹 ∘𝑓 · 𝑊))
265	264	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))
266	4	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
267	2	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
268	4	feqmptd 6159	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
269	2	feqmptd 6159	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
270	1, 266, 267, 268, 269	offval2 6812	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
271	270	oveq2d 6565	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
272	4	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
273	2	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
274	272, 273	rpmulcld 11764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
275	274	rpcnd 11750	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
276	1, 275	gsumfsum 19632	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
277	271, 276	eqtrd 2644	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
278		amgmwlem.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
279	4	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
280	2	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
281	279, 280	rpmulcld 11764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
282	1, 278, 281	fsumrpcl 14315	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
283	277, 282	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+)
284	265, 283	eqeltrrd 2689	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)) ∈ ℝ+)
285	284	relogcld 24173	. . . . 5 ⊢ (𝜑 → (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ∈ ℝ)
286		ringcmn 18404	. . . . . . 7 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
287	101, 286	mp1i 13	. . . . . 6 ⊢ (𝜑 → ℂfld ∈ CMnd)
288	153	simpli 473	. . . . . . . . 9 ⊢ ℝ ∈ (SubRing‘ℂfld)
289		subrgsubg 18609	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
290	288, 289	ax-mp 5	. . . . . . . 8 ⊢ ℝ ∈ (SubGrp‘ℂfld)
291		subgsubm 17439	. . . . . . . 8 ⊢ (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
292	290, 291	ax-mp 5	. . . . . . 7 ⊢ ℝ ∈ (SubMnd‘ℂfld)
293	292	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
294		remulcl 9900	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
295	294	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
296		rpssre 11719	. . . . . . . 8 ⊢ ℝ+ ⊆ ℝ
297		fss 5969	. . . . . . . 8 ⊢ ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
298	4, 296, 297	sylancl 693	. . . . . . 7 ⊢ (𝜑 → 𝑊:𝐴⟶ℝ)
299	2	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
300	299	relogcld 24173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
301	300	renegcld 10336	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ)
302		eqid 2610	. . . . . . . 8 ⊢ (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))
303	301, 302	fmptd 6292	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ)
304		inidm 3784	. . . . . . 7 ⊢ (𝐴 ∩ 𝐴) = 𝐴
305	295, 298, 303, 1, 1, 304	off 6810	. . . . . 6 ⊢ (𝜑 → (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))):𝐴⟶ℝ)
306		remulcl 9900	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
307	306	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
308		fss 5969	. . . . . . . . 9 ⊢ ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
309	4, 296, 308	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → 𝑊:𝐴⟶ℝ)
310	2	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
311	310	relogcld 24173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
312	311	renegcld 10336	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ)
313		eqid 2610	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))
314	312, 313	fmptd 6292	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ)
315		inidm 3784	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐴) = 𝐴
316	307, 309, 314, 1, 1, 315	off 6810	. . . . . . 7 ⊢ (𝜑 → (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))):𝐴⟶ℝ)
317		0red 9920	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ)
318	316, 1, 317	fdmfifsupp 8168	. . . . . 6 ⊢ (𝜑 → (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) finSupp 0)
319	103, 287, 1, 293, 305, 318	gsumsubmcl 18142	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ∈ ℝ)
320	296	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
321		simpr 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
322	321	relogcld 24173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
323	322	renegcld 10336	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
324		eqid 2610	. . . . . . . . 9 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
325	323, 324	fmptd 6292	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
326		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
327		ioorp 12122	. . . . . . . . . . . 12 ⊢ (0(,)+∞) = ℝ+
328	326, 327	syl6eleqr 2699	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
329		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
330	329, 327	syl6eleqr 2699	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
331		iccssioo2 12117	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
332	328, 330, 331	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
333	332, 327	syl6sseq 3614	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
334	333	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
335		ioossico 12133	. . . . . . . . . 10 ⊢ (0(,)+∞) ⊆ (0[,)+∞)
336	327, 335	eqsstr3i 3599	. . . . . . . . 9 ⊢ ℝ+ ⊆ (0[,)+∞)
337		fss 5969	. . . . . . . . 9 ⊢ ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞))
338	4, 336, 337	sylancl 693	. . . . . . . 8 ⊢ (𝜑 → 𝑊:𝐴⟶(0[,)+∞))
339		0lt1 10429	. . . . . . . . 9 ⊢ 0 < 1
340		amgmwlem.5	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg 𝑊) = 1)
341	339, 340	syl5breqr 4621	. . . . . . . 8 ⊢ (𝜑 → 0 < (ℂfld Σg 𝑊))
342	296	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
343		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
344	343	relogcld 24173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
345	344	renegcld 10336	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
346		eqid 2610	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
347	345, 346	fmptd 6292	. . . . . . . . 9 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
348		simpl 472	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
349	348, 327	syl6eleqr 2699	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
350		simpr 476	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
351	350, 327	syl6eleqr 2699	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
352		iccssioo2 12117	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
353	349, 351, 352	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
354	353, 327	syl6sseq 3614	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
355	354	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
356		logccv 24209	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
357	356	3adant1 1072	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
358		elioore 12076	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
359	358	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
360		simp21 1087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
361	360	relogcld 24173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
362	359, 361	remulcld 9949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
363		1red 9934	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
364		elioore 12076	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
365	363, 364	resubcld 10337	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
366	365	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
367		simp22 1088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
368	367	relogcld 24173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
369	366, 368	remulcld 9949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
370	362, 369	readdcld 9948	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
371		elioore 12076	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
372		eliooord 12104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
373	372	simpld 474	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 0 < 𝑡)
374	371, 373	elrpd 11745	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
375	374	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
376		simp21 1087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
377	375, 376	rpmulcld 11764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
378		1red 9934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
379		elioore 12076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
380	378, 379	resubcld 10337	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
381		elioore 12076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
382		1red 9934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
383		0red 9920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
384		eliooord 12104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
385	384	simprd 478	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < 1)
386		1m0e1 11008	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 − 0) = 1
387	385, 386	syl6breqr 4625	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
388	381, 382, 383, 387	ltsub13d 10512	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
389	380, 388	elrpd 11745	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
390	389	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
391		simp22 1088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
392	390, 391	rpmulcld 11764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
393		rpaddcl 11730	. . . . . . . . . . . . . 14 ⊢ (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
394	377, 392, 393	syl2anc 691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
395	394	relogcld 24173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
396	370, 395	ltnegd 10484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
397	357, 396	mpbid 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
398		eqidd 2611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
399		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
400	399	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
401	400	negeqd 10154	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
402		elioore 12076	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
403		eliooord 12104	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
404	403	simpld 474	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 0 < 𝑡)
405	402, 404	elrpd 11745	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
406	405	3ad2ant3 1077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
407		simp21 1087	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
408	406, 407	rpmulcld 11764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
409		1red 9934	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
410		elioore 12076	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
411	409, 410	resubcld 10337	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
412		elioore 12076	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
413		1red 9934	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
414		0red 9920	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
415		eliooord 12104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
416	415	simprd 478	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < 1)
417	416, 386	syl6breqr 4625	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
418	412, 413, 414, 417	ltsub13d 10512	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
419	411, 418	elrpd 11745	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
420	419	3ad2ant3 1077	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
421		simp22 1088	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
422	420, 421	rpmulcld 11764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
423		rpaddcl 11730	. . . . . . . . . . . 12 ⊢ (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
424	408, 422, 423	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
425		negex 10158	. . . . . . . . . . . 12 ⊢ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
426	425	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V)
427	398, 401, 424, 426	fvmptd 6197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
428		simp21 1087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
429		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
430	429	negeqd 10154	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
431		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
432		negex 10158	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑤) ∈ V
433	430, 431, 432	fvmpt3i 6196	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
434	428, 433	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
435	434	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
436		elioore 12076	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
437	436	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
438	437	recnd 9947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
439		simp21 1087	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
440	439	relogcld 24173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
441	440	recnd 9947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
442	438, 441	mulneg2d 10363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
443	435, 442	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
444		simp22 1088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
445		fveq2 6103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
446	445	negeqd 10154	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
447		eqid 2610	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
448		negex 10158	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑤) ∈ V
449	446, 447, 448	fvmpt3i 6196	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
450	444, 449	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
451	450	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
452		1red 9934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
453		elioore 12076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
454	452, 453	resubcld 10337	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
455		elioore 12076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
456		1red 9934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
457		0red 9920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
458		eliooord 12104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
459	458	simprd 478	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < 1)
460	459, 386	syl6breqr 4625	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
461	455, 456, 457, 460	ltsub13d 10512	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
462	454, 461	elrpd 11745	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
463	462	3ad2ant3 1077	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
464	463	rpcnd 11750	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
465		simp22 1088	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
466	465	relogcld 24173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
467	466	recnd 9947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
468	464, 467	mulneg2d 10363	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
469	451, 468	eqtrd 2644	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
470	443, 469	oveq12d 6567	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
471		elioore 12076	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
472	471	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
473		simp21 1087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
474	473	relogcld 24173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
475	472, 474	remulcld 9949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
476	475	recnd 9947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
477		1red 9934	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
478		elioore 12076	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
479	477, 478	resubcld 10337	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
480	479	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
481		simp22 1088	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
482	481	relogcld 24173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
483	480, 482	remulcld 9949	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
484	483	recnd 9947	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
485	476, 484	negdid 10284	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
486	470, 485	eqtr4d 2647	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
487	397, 427, 486	3brtr4d 4615	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
488	342, 347, 355, 487	scvxcvx 24512	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ∧ 𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
489	320, 325, 334, 1, 338, 2, 341, 488	jensen 24515	. . . . . . 7 ⊢ (𝜑 → (((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊)) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊))))
490	489	simprd 478	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)))
491	340	oveq2d 6565	. . . . . . . 8 ⊢ (𝜑 → ((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / 1))
492	491	fveq2d 6107	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / 1)))
493	4	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
494	2	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
495	4	feqmptd 6159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
496	2	feqmptd 6159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
497	1, 493, 494, 495, 496	offval2 6812	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
498	497	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
499	4	ffvelrnda 6267	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
500	2	ffvelrnda 6267	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
501	499, 500	rpmulcld 11764	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
502	501	rpcnd 11750	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
503	1, 502	gsumfsum 19632	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
504	498, 503	eqtrd 2644	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
505	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
506	2	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
507	505, 506	rpmulcld 11764	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
508	1, 278, 507	fsumrpcl 14315	. . . . . . . . . . 11 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
509	504, 508	eqeltrd 2688	. . . . . . . . . 10 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+)
510	509	rpcnd 11750	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℂ)
511	510	div1d 10672	. . . . . . . 8 ⊢ (𝜑 → ((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / 1) = (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)))
512	511	fveq2d 6107	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / 1)) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))))
513	4	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
514	2	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
515	4	feqmptd 6159	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
516	2	feqmptd 6159	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
517	1, 513, 514, 515, 516	offval2 6812	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
518	517	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
519	4	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
520	2	ffvelrnda 6267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
521	519, 520	rpmulcld 11764	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
522	521	rpcnd 11750	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
523	1, 522	gsumfsum 19632	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
524	518, 523	eqtrd 2644	. . . . . . . . . 10 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
525	4	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
526	2	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
527	525, 526	rpmulcld 11764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
528	1, 278, 527	fsumrpcl 14315	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
529	524, 528	eqeltrd 2688	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+)
530		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑤 = (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) → (log‘𝑤) = (log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))))
531	530	negeqd 10154	. . . . . . . . . 10 ⊢ (𝑤 = (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) → -(log‘𝑤) = -(log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))))
532		eqid 2610	. . . . . . . . . 10 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
533		negex 10158	. . . . . . . . . 10 ⊢ -(log‘𝑤) ∈ V
534	531, 532, 533	fvmpt3i 6196	. . . . . . . . 9 ⊢ ((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))))
535	529, 534	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))))
536		simprl 790	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
537	536	rpcnd 11750	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
538		simprr 792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
539	538	rpcnd 11750	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
540	537, 539	mulcomd 9940	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
541	1, 4, 2, 540	caofcom 6827	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝐹 ∘𝑓 · 𝑊))
542	541	oveq2d 6565	. . . . . . . . . 10 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))
543	542	fveq2d 6107	. . . . . . . . 9 ⊢ (𝜑 → (log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))) = (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
544	543	negeqd 10154	. . . . . . . 8 ⊢ (𝜑 → -(log‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
545	535, 544	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊 ∘𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
546	492, 512, 545	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) = -(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
547	340	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1))
548		ringcmn 18404	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
549	101, 548	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℂfld ∈ CMnd)
550		ringmnd 18379	. . . . . . . . . . 11 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
551	101, 550	ax-mp 5	. . . . . . . . . 10 ⊢ ℂfld ∈ Mnd
552	102	submid 17174	. . . . . . . . . 10 ⊢ (ℂfld ∈ Mnd → ℂ ∈ (SubMnd‘ℂfld))
553	551, 552	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ (SubMnd‘ℂfld))
554		mulcl 9899	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
555	554	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
556		rpcn 11717	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ)
557	556	ssriv 3572	. . . . . . . . . . . 12 ⊢ ℝ+ ⊆ ℂ
558	557	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ+ ⊆ ℂ)
559	4, 558	fssd 5970	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊:𝐴⟶ℂ)
560		simpr 476	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
561	560	relogcld 24173	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
562	561	recnd 9947	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
563	562	negcld 10258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
564		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
565	563, 564	fmptd 6292	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
566		fco 5971	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
567	565, 2, 566	syl2anc 691	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
568		inidm 3784	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝐴) = 𝐴
569	555, 559, 567, 1, 1, 568	off 6810	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
570		mulcl 9899	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
571	570	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
572		rpcn 11717	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ)
573	572	ssriv 3572	. . . . . . . . . . . . 13 ⊢ ℝ+ ⊆ ℂ
574	573	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℝ+ ⊆ ℂ)
575	4, 574	fssd 5970	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊:𝐴⟶ℂ)
576		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
577	576	relogcld 24173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
578	577	recnd 9947	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
579	578	negcld 10258	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
580		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
581	579, 580	fmptd 6292	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
582		fco 5971	. . . . . . . . . . . 12 ⊢ (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
583	581, 2, 582	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
584		inidm 3784	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐴) = 𝐴
585	571, 575, 583, 1, 1, 584	off 6810	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
586		0red 9920	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
587	585, 1, 586	fdmfifsupp 8168	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) finSupp 0)
588	103, 549, 1, 553, 569, 587	gsumsubmcl 18142	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) ∈ ℂ)
589	588	div1d 10672	. . . . . . 7 ⊢ (𝜑 → ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1) = (ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))))
590	2	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
591	2	feqmptd 6159	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
592		eqidd 2611	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
593		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘)))
594	593	negeqd 10154	. . . . . . . . . 10 ⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘)))
595	590, 591, 592, 594	fmptco 6303	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
596	595	oveq2d 6565	. . . . . . . 8 ⊢ (𝜑 → (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))
597	596	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
598	547, 589, 597	3eqtrd 2648	. . . . . 6 ⊢ (𝜑 → ((ℂfld Σg (𝑊 ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
599	490, 546, 598	3brtr3d 4614	. . . . 5 ⊢ (𝜑 → -(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ≤ (ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
600	285, 319, 599	lenegcon1d 10488	. . . 4 ⊢ (𝜑 → -(ℂfld Σg (𝑊 ∘𝑓 · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ≤ (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
601	258, 600	eqbrtrrd 4607	. . 3 ⊢ (𝜑 → (log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))
602	96, 115	ringidval 18326	. . . . . 6 ⊢ 1 = (0g‘𝑀)
603	96	crngmgp 18378	. . . . . . 7 ⊢ (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
604	133, 603	mp1i 13	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ CMnd)
605	96	oveq1i 6559	. . . . . . . . . . 11 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
606	605	rpmsubg 19629	. . . . . . . . . 10 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
607		subgsubm 17439	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
608	606, 607	ax-mp 5	. . . . . . . . 9 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
609	102, 103, 104	drngui 18576	. . . . . . . . . . 11 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
610	609, 96	unitsubm 18493	. . . . . . . . . 10 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
611		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
612	611	subsubm 17180	. . . . . . . . . 10 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
613	101, 610, 612	mp2b 10	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
614	608, 613	mpbi 219	. . . . . . . 8 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
615	614	simpli 473	. . . . . . 7 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
616	615	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
617		rpre 11715	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
618	617	anim2i 591	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
619	618	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
620		rpcxpcl 24222	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
621	619, 620	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
622		inidm 3784	. . . . . . 7 ⊢ (𝐴 ∩ 𝐴) = 𝐴
623	621, 2, 4, 1, 1, 622	off 6810	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
624		rpre 11715	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
625	624	anim2i 591	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
626	625	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
627		rpcxpcl 24222	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
628	626, 627	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
629		inidm 3784	. . . . . . . 8 ⊢ (𝐴 ∩ 𝐴) = 𝐴
630	628, 2, 4, 1, 1, 629	off 6810	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
631		1red 9934	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℝ)
632	630, 1, 631	fdmfifsupp 8168	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊) finSupp 1)
633	602, 604, 1, 616, 623, 632	gsumsubmcl 18142	. . . . 5 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ∈ ℝ+)
634	633	relogcld 24173	. . . 4 ⊢ (𝜑 → (log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) ∈ ℝ)
635		simprl 790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
636	635	rpcnd 11750	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
637		simprr 792	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
638	637	rpcnd 11750	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
639	636, 638	mulcomd 9940	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
640	1, 4, 2, 639	caofcom 6827	. . . . . . 7 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝐹 ∘𝑓 · 𝑊))
641	640	oveq2d 6565	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))
642	4	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
643	2	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
644	4	feqmptd 6159	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
645	2	feqmptd 6159	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
646	1, 642, 643, 644, 645	offval2 6812	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
647	646	oveq2d 6565	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
648	4	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
649	2	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
650	648, 649	rpmulcld 11764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
651	650	rpcnd 11750	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
652	1, 651	gsumfsum 19632	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
653	647, 652	eqtrd 2644	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
654	4	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
655	2	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
656	654, 655	rpmulcld 11764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
657	1, 278, 656	fsumrpcl 14315	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
658	653, 657	eqeltrd 2688	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+)
659	641, 658	eqeltrrd 2689	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)) ∈ ℝ+)
660	659	relogcld 24173	. . . 4 ⊢ (𝜑 → (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ∈ ℝ)
661		efle 14687	. . . 4 ⊢ (((log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) ∈ ℝ ∧ (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ∈ ℝ) → ((log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))))
662	634, 660, 661	syl2anc 691	. . 3 ⊢ (𝜑 → ((log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊))))))
663	601, 662	mpbid 221	. 2 ⊢ (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))))
664	96, 115	ringidval 18326	. . . . 5 ⊢ 1 = (0g‘𝑀)
665	96	crngmgp 18378	. . . . . 6 ⊢ (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
666	133, 665	mp1i 13	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ CMnd)
667	96	oveq1i 6559	. . . . . . . . . 10 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
668	667	rpmsubg 19629	. . . . . . . . 9 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
669		subgsubm 17439	. . . . . . . . 9 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
670	668, 669	ax-mp 5	. . . . . . . 8 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
671	102, 103, 104	drngui 18576	. . . . . . . . . 10 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
672	671, 96	unitsubm 18493	. . . . . . . . 9 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
673		eqid 2610	. . . . . . . . . 10 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
674	673	subsubm 17180	. . . . . . . . 9 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
675	101, 672, 674	mp2b 10	. . . . . . . 8 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
676	670, 675	mpbi 219	. . . . . . 7 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
677	676	simpli 473	. . . . . 6 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
678	677	a1i 11	. . . . 5 ⊢ (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
679		rpre 11715	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
680	679	anim2i 591	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
681	680	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
682		rpcxpcl 24222	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
683	681, 682	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
684		inidm 3784	. . . . . 6 ⊢ (𝐴 ∩ 𝐴) = 𝐴
685	683, 2, 4, 1, 1, 684	off 6810	. . . . 5 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
686		rpre 11715	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
687	686	anim2i 591	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
688	687	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ))
689		rpcxpcl 24222	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ) → (𝑥↑𝑐𝑦) ∈ ℝ+)
690	688, 689	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥↑𝑐𝑦) ∈ ℝ+)
691		inidm 3784	. . . . . . 7 ⊢ (𝐴 ∩ 𝐴) = 𝐴
692	690, 2, 4, 1, 1, 691	off 6810	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊):𝐴⟶ℝ+)
693		1red 9934	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
694	692, 1, 693	fdmfifsupp 8168	. . . . 5 ⊢ (𝜑 → (𝐹 ∘𝑓 ↑𝑐𝑊) finSupp 1)
695	664, 666, 1, 678, 685, 694	gsumsubmcl 18142	. . . 4 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ∈ ℝ+)
696	695	reeflogd 24174	. . 3 ⊢ (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))) = (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))
697	696	eqcomd 2616	. 2 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) = (exp‘(log‘(𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)))))
698		simprl 790	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
699	698	rpcnd 11750	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
700		simprr 792	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
701	700	rpcnd 11750	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
702	699, 701	mulcomd 9940	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
703	1, 4, 2, 702	caofcom 6827	. . . . . 6 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝐹 ∘𝑓 · 𝑊))
704	703	oveq2d 6565	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))
705	4	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
706	2	ffvelrnda 6267	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
707	4	feqmptd 6159	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
708	2	feqmptd 6159	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
709	1, 705, 706, 707, 708	offval2 6812	. . . . . . . 8 ⊢ (𝜑 → (𝑊 ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
710	709	oveq2d 6565	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
711	4	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
712	2	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
713	711, 712	rpmulcld 11764	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
714	713	rpcnd 11750	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
715	1, 714	gsumfsum 19632	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
716	710, 715	eqtrd 2644	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
717	4	ffvelrnda 6267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ+)
718	2	ffvelrnda 6267	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
719	717, 718	rpmulcld 11764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
720	1, 278, 719	fsumrpcl 14315	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ+)
721	716, 720	eqeltrd 2688	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝑊 ∘𝑓 · 𝐹)) ∈ ℝ+)
722	704, 721	eqeltrrd 2689	. . . 4 ⊢ (𝜑 → (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)) ∈ ℝ+)
723	722	reeflogd 24174	. . 3 ⊢ (𝜑 → (exp‘(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))) = (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))
724	723	eqcomd 2616	. 2 ⊢ (𝜑 → (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)) = (exp‘(log‘(ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))))
725	663, 697, 724	3brtr4d 4615	1 ⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓 ↑𝑐𝑊)) ≤ (ℂfld Σg (𝐹 ∘𝑓 · 𝑊)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  ℝ⁺crp 11708  (,)cioo 12046  [,)cico 12048  [,]cicc 12049  Σcsu 14264  expce 14631  Basecbs 15695   ↾_s cress 15696  0_gc0g 15923   Σ_g cgsu 15924  Mndcmnd 17117   MndHom cmhm 17156  SubMndcsubmnd 17157  SubGrpcsubg 17411   GrpHom cghm 17480   GrpIso cgim 17522  CMndccmn 18016  mulGrpcmgp 18312  Ringcrg 18370  CRingccrg 18371  DivRingcdr 18570  SubRingcsubrg 18599  ℂ_fldccnfld 19567  ℝ_fldcrefld 19769  logclog 24105  ↑_𝑐ccxp 24106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ioc 12051  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-fac 12923  df-bc 12952  df-hash 12980  df-shft 13655  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-limsup 14050  df-clim 14067  df-rlim 14068  df-sum 14265  df-ef 14637  df-sin 14639  df-cos 14640  df-pi 14642  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-hom 15793  df-cco 15794  df-rest 15906  df-topn 15907  df-0g 15925  df-gsum 15926  df-topgen 15927  df-pt 15928  df-prds 15931  df-xrs 15985  df-qtop 15990  df-imas 15991  df-xps 15993  df-mre 16069  df-mrc 16070  df-acs 16072  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-submnd 17159  df-grp 17248  df-minusg 17249  df-mulg 17364  df-subg 17414  df-ghm 17481  df-gim 17524  df-cntz 17573  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-oppr 18446  df-dvdsr 18464  df-unit 18465  df-invr 18495  df-dvr 18506  df-drng 18572  df-subrg 18601  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-fbas 19564  df-fg 19565  df-cnfld 19568  df-refld 19770  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cld 20633  df-ntr 20634  df-cls 20635  df-nei 20712  df-lp 20750  df-perf 20751  df-cn 20841  df-cnp 20842  df-haus 20929  df-cmp 21000  df-tx 21175  df-hmeo 21368  df-fil 21460  df-fm 21552  df-flim 21553  df-flf 21554  df-xms 21935  df-ms 21936  df-tms 21937  df-cncf 22489  df-limc 23436  df-dv 23437  df-log 24107  df-cxp 24108

This theorem is referenced by:  amgmlemALT  42358  amgmw2d  42359