Theorem amgmlem 25253

Description: Lemma for amgm 25254. (Contributed by Mario Carneiro, 21-Jun-2015.)

Hypotheses

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

Assertion

Ref	Expression
amgmlem	⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))

Proof of Theorem amgmlem

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

Step	Hyp	Ref	Expression
1		cnfld0 20255	. . . . . . . 8 ⊢ 0 = (0g‘ℂfld)
2		cnring 20253	. . . . . . . . 9 ⊢ ℂfld ∈ Ring
3		ringabl 19024	. . . . . . . . 9 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Abel)
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ℂfld ∈ Abel)
5		amgm.2	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		resubdrg 20438	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
7	6	simpli 484	. . . . . . . . 9 ⊢ ℝ ∈ (SubRing‘ℂfld)
8		subrgsubg 19235	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
9	7, 8	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ℝ ∈ (SubGrp‘ℂfld))
10		amgm.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)
11	10	ffvelrnda 6723	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ+)
12	11	relogcld 24891	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
13	12	renegcld 10921	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ)
14	13	fmpttd 6749	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ)
15		c0ex 10488	. . . . . . . . . 10 ⊢ 0 ∈ V
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
17	14, 5, 16	fdmfifsupp 8696	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) finSupp 0)
18	1, 4, 5, 9, 14, 17	gsumsubgcl 18764	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℝ)
19	18	recnd 10522	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℂ)
20		amgm.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ ∅)
21		hashnncl 13581	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
22	5, 21	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
23	20, 22	mpbird 258	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
24	23	nncnd 11508	. . . . . 6 ⊢ (𝜑 → (♯‘𝐴) ∈ ℂ)
25	23	nnne0d 11541	. . . . . 6 ⊢ (𝜑 → (♯‘𝐴) ≠ 0)
26	19, 24, 25	divnegd 11283	. . . . 5 ⊢ (𝜑 → -((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = (-(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
27	12	recnd 10522	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ)
28	5, 27	gsumfsum 20298	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘)))
29	27	negnegd 10842	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘(𝐹‘𝑘)) = (log‘(𝐹‘𝑘)))
30	29	sumeq2dv 14897	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘)))
31	13	recnd 10522	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ)
32	5, 31	fsumneg 14979	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
33	28, 30, 32	3eqtr2rd 2840	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))))
34	5, 31	gsumfsum 20298	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
35	34	negeqd 10733	. . . . . . . 8 ⊢ (𝜑 → -(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
36	10	feqmptd 6608	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
37		relogf1o 24835	. . . . . . . . . . . . 13 ⊢ (log ↾ ℝ+):ℝ+–1-1-onto→ℝ
38		f1of 6490	. . . . . . . . . . . . 13 ⊢ ((log ↾ ℝ+):ℝ+–1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
39	37, 38	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
40	39	feqmptd 6608	. . . . . . . . . . 11 ⊢ (𝜑 → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)))
41		fvres 6564	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → ((log ↾ ℝ+)‘𝑥) = (log‘𝑥))
42	41	mpteq2ia 5058	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ ↦ ((log ↾ ℝ+)‘𝑥)) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥))
43	40, 42	syl6eq 2849	. . . . . . . . . 10 ⊢ (𝜑 → (log ↾ ℝ+) = (𝑥 ∈ ℝ+ ↦ (log‘𝑥)))
44		fveq2 6545	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑘) → (log‘𝑥) = (log‘(𝐹‘𝑘)))
45	11, 36, 43, 44	fmptco 6761	. . . . . . . . 9 ⊢ (𝜑 → ((log ↾ ℝ+) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))
46	45	oveq2d 7039	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))))
47	33, 35, 46	3eqtr4d 2843	. . . . . . 7 ⊢ (𝜑 → -(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)))
48		amgm.1	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = (mulGrp‘ℂfld)
49	48	oveq1i 7033	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
50	49	rpmsubg 20295	. . . . . . . . . . . . 13 ⊢ ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
51		subgsubm 18059	. . . . . . . . . . . . 13 ⊢ (ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))))
52	50, 51	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
53		cnfldbas 20235	. . . . . . . . . . . . . . 15 ⊢ ℂ = (Base‘ℂfld)
54		cndrng 20260	. . . . . . . . . . . . . . 15 ⊢ ℂfld ∈ DivRing
55	53, 1, 54	drngui 19202	. . . . . . . . . . . . . 14 ⊢ (ℂ ∖ {0}) = (Unit‘ℂfld)
56	55, 48	unitsubm 19114	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
57		eqid 2797	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↾s (ℂ ∖ {0})) = (𝑀 ↾s (ℂ ∖ {0}))
58	57	subsubm 17800	. . . . . . . . . . . . 13 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
59	2, 56, 58	mp2b 10	. . . . . . . . . . . 12 ⊢ (ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
60	52, 59	mpbi 231	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
61	60	simpli 484	. . . . . . . . . 10 ⊢ ℝ+ ∈ (SubMnd‘𝑀)
62		eqid 2797	. . . . . . . . . . 11 ⊢ (𝑀 ↾s ℝ+) = (𝑀 ↾s ℝ+)
63	62	submbas 17798	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀 ↾s ℝ+)))
64	61, 63	ax-mp 5	. . . . . . . . 9 ⊢ ℝ+ = (Base‘(𝑀 ↾s ℝ+))
65		cnfld1 20256	. . . . . . . . . . . 12 ⊢ 1 = (1r‘ℂfld)
66	48, 65	ringidval 18947	. . . . . . . . . . 11 ⊢ 1 = (0g‘𝑀)
67	62, 66	subm0 17799	. . . . . . . . . 10 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → 1 = (0g‘(𝑀 ↾s ℝ+)))
68	61, 67	ax-mp 5	. . . . . . . . 9 ⊢ 1 = (0g‘(𝑀 ↾s ℝ+))
69		cncrng 20252	. . . . . . . . . . 11 ⊢ ℂfld ∈ CRing
70	48	crngmgp 18999	. . . . . . . . . . 11 ⊢ (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
71	69, 70	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ CMnd)
72	62	submmnd 17797	. . . . . . . . . . 11 ⊢ (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+) ∈ Mnd)
73	61, 72	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 ↾s ℝ+) ∈ Mnd)
74	62	subcmn 18686	. . . . . . . . . 10 ⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+) ∈ CMnd)
75	71, 73, 74	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ↾s ℝ+) ∈ CMnd)
76		df-refld 20435	. . . . . . . . . . . 12 ⊢ ℝfld = (ℂfld ↾s ℝ)
77	76	subrgring 19232	. . . . . . . . . . 11 ⊢ (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
78	7, 77	ax-mp 5	. . . . . . . . . 10 ⊢ ℝfld ∈ Ring
79		ringmnd 19000	. . . . . . . . . 10 ⊢ (ℝfld ∈ Ring → ℝfld ∈ Mnd)
80	78, 79	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℝfld ∈ Mnd)
81	48	oveq1i 7033	. . . . . . . . . . . 12 ⊢ (𝑀 ↾s ℝ+) = ((mulGrp‘ℂfld) ↾s ℝ+)
82	81	reloggim 24867	. . . . . . . . . . 11 ⊢ (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpIso ℝfld)
83		gimghm 18149	. . . . . . . . . . 11 ⊢ ((log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld))
84	82, 83	ax-mp 5	. . . . . . . . . 10 ⊢ (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld)
85		ghmmhm 18113	. . . . . . . . . 10 ⊢ ((log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) MndHom ℝfld))
86	84, 85	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → (log ↾ ℝ+) ∈ ((𝑀 ↾s ℝ+) MndHom ℝfld))
87		1ex 10490	. . . . . . . . . . 11 ⊢ 1 ∈ V
88	87	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ V)
89	10, 5, 88	fdmfifsupp 8696	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 finSupp 1)
90	64, 68, 75, 80, 5, 86, 10, 89	gsummhm 18782	. . . . . . . 8 ⊢ (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾ ℝ+)‘((𝑀 ↾s ℝ+) Σg 𝐹)))
91		subgsubm 18059	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
92	9, 91	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
93		fco 6406	. . . . . . . . . 10 ⊢ (((log ↾ ℝ+):ℝ+⟶ℝ ∧ 𝐹:𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ)
94	39, 10, 93	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((log ↾ ℝ+) ∘ 𝐹):𝐴⟶ℝ)
95	5, 92, 94, 76	gsumsubm 17816	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = (ℝfld Σg ((log ↾ ℝ+) ∘ 𝐹)))
96	61	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
97	5, 96, 10, 62	gsumsubm 17816	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 ↾s ℝ+) Σg 𝐹))
98	97	fveq2d 6549	. . . . . . . 8 ⊢ (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)) = ((log ↾ ℝ+)‘((𝑀 ↾s ℝ+) Σg 𝐹)))
99	90, 95, 98	3eqtr4d 2843	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ 𝐹)) = ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)))
100	66, 71, 5, 96, 10, 89	gsumsubmcl 18763	. . . . . . . 8 ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ ℝ+)
101	100	fvresd 6565	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg 𝐹)) = (log‘(𝑀 Σg 𝐹)))
102	47, 99, 101	3eqtrd 2837	. . . . . 6 ⊢ (𝜑 → -(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (log‘(𝑀 Σg 𝐹)))
103	102	oveq1d 7038	. . . . 5 ⊢ (𝜑 → (-(ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((log‘(𝑀 Σg 𝐹)) / (♯‘𝐴)))
104	100	relogcld 24891	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑀 Σg 𝐹)) ∈ ℝ)
105	104	recnd 10522	. . . . . 6 ⊢ (𝜑 → (log‘(𝑀 Σg 𝐹)) ∈ ℂ)
106	105, 24, 25	divrec2d 11274	. . . . 5 ⊢ (𝜑 → ((log‘(𝑀 Σg 𝐹)) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))))
107	26, 103, 106	3eqtrd 2837	. . . 4 ⊢ (𝜑 → -((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))))
108	36	oveq2d 7039	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg 𝐹) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))
109	11	rpcnd 12287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ)
110	5, 109	gsumfsum 20298	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
111	108, 110	eqtrd 2833	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg 𝐹) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
112	5, 20, 11	fsumrpcl 14931	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ ℝ+)
113	111, 112	eqeltrd 2885	. . . . . . 7 ⊢ (𝜑 → (ℂfld Σg 𝐹) ∈ ℝ+)
114	23	nnrpd 12283	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ+)
115	113, 114	rpdivcld 12302	. . . . . 6 ⊢ (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ+)
116	115	relogcld 24891	. . . . 5 ⊢ (𝜑 → (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ)
117	18, 23	nndivred 11545	. . . . 5 ⊢ (𝜑 → ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℝ)
118		rpssre 12250	. . . . . . . . 9 ⊢ ℝ+ ⊆ ℝ
119	118	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
120		relogcl 24844	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℝ+ → (log‘𝑤) ∈ ℝ)
121	120	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
122	121	renegcld 10921	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
123	122	fmpttd 6749	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
124		ioorp 12668	. . . . . . . . . . . 12 ⊢ (0(,)+∞) = ℝ+
125	124	eleq2i 2876	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (0(,)+∞) ↔ 𝑎 ∈ ℝ+)
126	124	eleq2i 2876	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (0(,)+∞) ↔ 𝑏 ∈ ℝ+)
127		iccssioo2 12663	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
128	125, 126, 127	syl2anbr 598	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
129	128, 124	syl6sseq 3944	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
130	129	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
131	23	nnrecred 11542	. . . . . . . . . 10 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ)
132	114	rpreccld 12295	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ+)
133	132	rpge0d 12289	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (1 / (♯‘𝐴)))
134		elrege0 12696	. . . . . . . . . 10 ⊢ ((1 / (♯‘𝐴)) ∈ (0[,)+∞) ↔ ((1 / (♯‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (♯‘𝐴))))
135	131, 133, 134	sylanbrc 583	. . . . . . . . 9 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ (0[,)+∞))
136		fconst6g 6443	. . . . . . . . 9 ⊢ ((1 / (♯‘𝐴)) ∈ (0[,)+∞) → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
137	135, 136	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
138		0lt1 11016	. . . . . . . . 9 ⊢ 0 < 1
139		fconstmpt 5507	. . . . . . . . . . 11 ⊢ (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))
140	139	oveq2i 7034	. . . . . . . . . 10 ⊢ (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))))
141		ringmnd 19000	. . . . . . . . . . . . 13 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
142	2, 141	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂfld ∈ Mnd)
143	131	recnd 10522	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℂ)
144		eqid 2797	. . . . . . . . . . . . 13 ⊢ (.g‘ℂfld) = (.g‘ℂfld)
145	53, 144	gsumconst 18778	. . . . . . . . . . . 12 ⊢ ((ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ (1 / (♯‘𝐴)) ∈ ℂ) → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))))
146	142, 5, 143, 145	syl3anc 1364	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))))
147	23	nnzd 11940	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
148		cnfldmulg 20263	. . . . . . . . . . . 12 ⊢ (((♯‘𝐴) ∈ ℤ ∧ (1 / (♯‘𝐴)) ∈ ℂ) → ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
149	147, 143, 148	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴)(.g‘ℂfld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
150	24, 25	recidd 11265	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) · (1 / (♯‘𝐴))) = 1)
151	146, 149, 150	3eqtrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = 1)
152	140, 151	syl5eq 2845	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})) = 1)
153	138, 152	breqtrrid 5006	. . . . . . . 8 ⊢ (𝜑 → 0 < (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))
154		logccv 24931	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
155	154	3adant1 1123	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
156		ioossre 12652	. . . . . . . . . . . . . . 15 ⊢ (0(,)1) ⊆ ℝ
157		simp3 1131	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
158	156, 157	sseldi 3893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
159		simp21 1199	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
160	159	relogcld 24891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
161	158, 160	remulcld 10524	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
162		1re 10494	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
163		resubcl 10804	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
164	162, 158, 163	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
165		simp22 1200	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
166	165	relogcld 24891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
167	164, 166	remulcld 10524	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
168	161, 167	readdcld 10523	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
169		simp1 1129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝜑)
170		ioossicc 12676	. . . . . . . . . . . . . . 15 ⊢ (0(,)1) ⊆ (0[,]1)
171	170, 157	sseldi 3893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0[,]1))
172	119, 130	cvxcl 25248	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
173	169, 159, 165, 171, 172	syl13anc 1365	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
174	173	relogcld 24891	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
175	168, 174	ltnegd 11072	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
176	155, 175	mpbid 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
177		fveq2 6545	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
178	177	negeqd 10733	. . . . . . . . . . . 12 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
179		eqid 2797	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
180		negex 10737	. . . . . . . . . . . 12 ⊢ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
181	178, 179, 180	fvmpt 6642	. . . . . . . . . . 11 ⊢ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
182	173, 181	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
183		fveq2 6545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
184	183	negeqd 10733	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
185		negex 10737	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑥) ∈ V
186	184, 179, 185	fvmpt 6642	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
187	159, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
188	187	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
189	158	recnd 10522	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
190	160	recnd 10522	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
191	189, 190	mulneg2d 10948	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
192	188, 191	eqtrd 2833	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
193		fveq2 6545	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
194	193	negeqd 10733	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
195		negex 10737	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑦) ∈ V
196	194, 179, 195	fvmpt 6642	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
197	165, 196	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
198	197	oveq2d 7039	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
199	164	recnd 10522	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
200	166	recnd 10522	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
201	199, 200	mulneg2d 10948	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
202	198, 201	eqtrd 2833	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
203	192, 202	oveq12d 7041	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
204	161	recnd 10522	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
205	167	recnd 10522	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
206	204, 205	negdid 10864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
207	203, 206	eqtr4d 2836	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
208	176, 182, 207	3brtr4d 5000	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
209	119, 123, 130, 208	scvxcvx 25249	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℝ+ ∧ 𝑣 ∈ ℝ+ ∧ 𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
210	119, 123, 130, 5, 137, 10, 153, 209	jensen 25252	. . . . . . 7 ⊢ (𝜑 → (((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))))
211	210	simprd 496	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))))
212	131	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈ ℝ)
213	139	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))))
214	5, 212, 11, 213, 36	offval2 7291	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘))))
215	214	oveq2d 7039	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))))
216		cnfldadd 20236	. . . . . . . . . . . 12 ⊢ + = (+g‘ℂfld)
217		cnfldmul 20237	. . . . . . . . . . . 12 ⊢ · = (.r‘ℂfld)
218	2	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂfld ∈ Ring)
219	109	fmpttd 6749	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)):𝐴⟶ℂ)
220	219, 5, 16	fdmfifsupp 8696	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) finSupp 0)
221	53, 1, 216, 217, 218, 5, 143, 109, 220	gsummulc2 19051	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))))
222		fss 6402	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝐹:𝐴⟶ℝ)
223	10, 118, 222	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
224	10, 5, 16	fdmfifsupp 8696	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 finSupp 0)
225	1, 4, 5, 9, 223, 224	gsumsubgcl 18764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂfld Σg 𝐹) ∈ ℝ)
226	225	recnd 10522	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂfld Σg 𝐹) ∈ ℂ)
227	226, 24, 25	divrec2d 11274	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld Σg 𝐹)))
228	108	oveq2d 7039	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (ℂfld Σg 𝐹)) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))))
229	227, 228	eqtr2d 2834	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
230	215, 221, 229	3eqtrd 2837	. . . . . . . . . 10 ⊢ (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
231	230, 152	oveq12d 7041	. . . . . . . . 9 ⊢ (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂfld Σg 𝐹) / (♯‘𝐴)) / 1))
232	225, 23	nndivred 11545	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ)
233	232	recnd 10522	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℂ)
234	233	div1d 11262	. . . . . . . . 9 ⊢ (𝜑 → (((ℂfld Σg 𝐹) / (♯‘𝐴)) / 1) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
235	231, 234	eqtrd 2833	. . . . . . . 8 ⊢ (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
236	235	fveq2d 6549	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
237		fveq2 6545	. . . . . . . . . 10 ⊢ (𝑤 = ((ℂfld Σg 𝐹) / (♯‘𝐴)) → (log‘𝑤) = (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
238	237	negeqd 10733	. . . . . . . . 9 ⊢ (𝑤 = ((ℂfld Σg 𝐹) / (♯‘𝐴)) → -(log‘𝑤) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
239		negex 10737	. . . . . . . . 9 ⊢ -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ V
240	238, 179, 239	fvmpt 6642	. . . . . . . 8 ⊢ (((ℂfld Σg 𝐹) / (♯‘𝐴)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
241	115, 240	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg 𝐹) / (♯‘𝐴))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
242	236, 241	eqtrd 2833	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · 𝐹)) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))})))) = -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
243	53, 1, 216, 217, 218, 5, 143, 31, 17	gsummulc2 19051	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
244		negex 10737	. . . . . . . . . . . 12 ⊢ -(log‘(𝐹‘𝑘)) ∈ V
245	244	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V)
246		eqidd 2798	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
247		fveq2 6545	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘)))
248	247	negeqd 10733	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘)))
249	11, 36, 246, 248	fmptco 6761	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
250	5, 212, 245, 213, 249	offval2 7291	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘)))))
251	250	oveq2d 7039	. . . . . . . . 9 ⊢ (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))))
252	19, 24, 25	divrec2d 11274	. . . . . . . . 9 ⊢ (𝜑 → ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
253	243, 251, 252	3eqtr4d 2843	. . . . . . . 8 ⊢ (𝜑 → (ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
254	253, 152	oveq12d 7041	. . . . . . 7 ⊢ (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1))
255	117	recnd 10522	. . . . . . . 8 ⊢ (𝜑 → ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℂ)
256	255	div1d 11262	. . . . . . 7 ⊢ (𝜑 → (((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1) = ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
257	254, 256	eqtrd 2833	. . . . . 6 ⊢ (𝜑 → ((ℂfld Σg ((𝐴 × {(1 / (♯‘𝐴))}) ∘𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
258	211, 242, 257	3brtr3d 4999	. . . . 5 ⊢ (𝜑 → -(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ≤ ((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
259	116, 117, 258	lenegcon1d 11076	. . . 4 ⊢ (𝜑 → -((ℂfld Σg (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
260	107, 259	eqbrtrrd 4992	. . 3 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))
261	131, 104	remulcld 10524	. . . 4 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ∈ ℝ)
262		efle 15308	. . . 4 ⊢ ((((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ∈ ℝ ∧ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ∈ ℝ) → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))))
263	261, 116, 262	syl2anc 584	. . 3 ⊢ (𝜑 → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹))) ≤ (log‘((ℂfld Σg 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴))))))
264	260, 263	mpbid 233	. 2 ⊢ (𝜑 → (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))) ≤ (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))
265	100	rpcnd 12287	. . 3 ⊢ (𝜑 → (𝑀 Σg 𝐹) ∈ ℂ)
266	100	rpne0d 12290	. . 3 ⊢ (𝜑 → (𝑀 Σg 𝐹) ≠ 0)
267	265, 266, 143	cxpefd 24980	. 2 ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) = (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σg 𝐹)))))
268	115	reeflogd 24892	. . 3 ⊢ (𝜑 → (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))) = ((ℂfld Σg 𝐹) / (♯‘𝐴)))
269	268	eqcomd 2803	. 2 ⊢ (𝜑 → ((ℂfld Σg 𝐹) / (♯‘𝐴)) = (exp‘(log‘((ℂfld Σg 𝐹) / (♯‘𝐴)))))
270	264, 267, 269	3brtr4d 5000	1 ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083   ≠ wne 2986  Vcvv 3440   ∖ cdif 3862   ⊆ wss 3865  ∅c0 4217  {csn 4478   class class class wbr 4968   ↦ cmpt 5047   × cxp 5448   ↾ cres 5452   ∘ ccom 5454  ⟶wf 6228  –1-1-onto→wf1o 6231  ‘cfv 6232  (class class class)co 7023   ∘_𝑓 cof 7272  Fincfn 8364  ℂcc 10388  ℝcr 10389  0cc0 10390  1c1 10391   + caddc 10393   · cmul 10395  +∞cpnf 10525   < clt 10528   ≤ cle 10529   − cmin 10723  -cneg 10724   / cdiv 11151  ℕcn 11492  ℤcz 11835  ℝ⁺crp 12243  (,)cioo 12592  [,)cico 12594  [,]cicc 12595  ♯chash 13544  Σcsu 14880  expce 15252  Basecbs 16316   ↾_s cress 16317  0_gc0g 16546   Σ_g cgsu 16547  Mndcmnd 17737   MndHom cmhm 17776  SubMndcsubmnd 17777  ._gcmg 17985  SubGrpcsubg 18031   GrpHom cghm 18100   GrpIso cgim 18142  CMndccmn 18637  Abelcabl 18638  mulGrpcmgp 18933  Ringcrg 18991  CRingccrg 18992  DivRingcdr 19196  SubRingcsubrg 19225  ℂ_fldccnfld 20231  ℝ_fldcrefld 20434  logclog 24823  ↑_𝑐ccxp 24824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468  ax-addf 10469  ax-mulf 10470

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-om 7444  df-1st 7552  df-2nd 7553  df-supp 7689  df-tpos 7750  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-ixp 8318  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fsupp 8687  df-fi 8728  df-sup 8759  df-inf 8760  df-oi 8827  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-z 11836  df-dec 11953  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-ioc 12597  df-ico 12598  df-icc 12599  df-fz 12747  df-fzo 12888  df-fl 13016  df-mod 13092  df-seq 13224  df-exp 13284  df-fac 13488  df-bc 13517  df-hash 13545  df-shft 14264  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-limsup 14666  df-clim 14683  df-rlim 14684  df-sum 14881  df-ef 15258  df-sin 15260  df-cos 15261  df-pi 15263  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-sca 16414  df-vsca 16415  df-ip 16416  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-hom 16422  df-cco 16423  df-rest 16529  df-topn 16530  df-0g 16548  df-gsum 16549  df-topgen 16550  df-pt 16551  df-prds 16554  df-xrs 16608  df-qtop 16613  df-imas 16614  df-xps 16616  df-mre 16690  df-mrc 16691  df-acs 16693  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-mhm 17778  df-submnd 17779  df-grp 17868  df-minusg 17869  df-mulg 17986  df-subg 18034  df-ghm 18101  df-gim 18144  df-cntz 18192  df-cmn 18639  df-abl 18640  df-mgp 18934  df-ur 18946  df-ring 18993  df-cring 18994  df-oppr 19067  df-dvdsr 19085  df-unit 19086  df-invr 19116  df-dvr 19127  df-drng 19198  df-subrg 19227  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-fbas 20228  df-fg 20229  df-cnfld 20232  df-refld 20435  df-top 21190  df-topon 21207  df-topsp 21229  df-bases 21242  df-cld 21315  df-ntr 21316  df-cls 21317  df-nei 21394  df-lp 21432  df-perf 21433  df-cn 21523  df-cnp 21524  df-haus 21611  df-cmp 21683  df-tx 21858  df-hmeo 22051  df-fil 22142  df-fm 22234  df-flim 22235  df-flf 22236  df-xms 22617  df-ms 22618  df-tms 22619  df-cncf 23173  df-limc 24151  df-dv 24152  df-log 24825  df-cxp 24826

This theorem is referenced by:  amgm  25254  amgm2d  40058  amgm3d  40059  amgm4d  40060