amgmlem - Metamath Proof Explorer

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

Theorem amgmlem 26484

Description: Lemma for amgm 26485. (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 20962	. . . . . . . 8 ⊢ 0 = (0_g‘ℂ_fld)
2		cnring 20960	. . . . . . . . 9 ⊢ ℂ_fld ∈ Ring
3		ringabl 20092	. . . . . . . . 9 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ Abel)
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ℂ_fld ∈ Abel)
5		amgm.2	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
6		resubdrg 21153	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) ∧ ℝ_fld ∈ DivRing)
7	6	simpli 485	. . . . . . . . 9 ⊢ ℝ ∈ (SubRing‘ℂ_fld)
8		subrgsubg 20362	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) → ℝ ∈ (SubGrp‘ℂ_fld))
9	7, 8	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → ℝ ∈ (SubGrp‘ℂ_fld))
10		amgm.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ⁺)
11	10	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ⁺)
12	11	relogcld 26123	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
13	12	renegcld 11638	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ)
14	13	fmpttd 7112	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ)
15		c0ex 11205	. . . . . . . . . 10 ⊢ 0 ∈ V
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ V)
17	14, 5, 16	fdmfifsupp 9370	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) finSupp 0)
18	1, 4, 5, 9, 14, 17	gsumsubgcl 19783	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℝ)
19	18	recnd 11239	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) ∈ ℂ)
20		amgm.3	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ ∅)
21		hashnncl 14323	. . . . . . . . 9 ⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
22	5, 21	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))
23	20, 22	mpbird 257	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐴) ∈ ℕ)
24	23	nncnd 12225	. . . . . 6 ⊢ (𝜑 → (♯‘𝐴) ∈ ℂ)
25	23	nnne0d 12259	. . . . . 6 ⊢ (𝜑 → (♯‘𝐴) ≠ 0)
26	19, 24, 25	divnegd 12000	. . . . 5 ⊢ (𝜑 → -((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = (-(ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
27	12	recnd 11239	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ)
28	5, 27	gsumfsum 21005	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘)))
29	27	negnegd 11559	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘(𝐹‘𝑘)) = (log‘(𝐹‘𝑘)))
30	29	sumeq2dv 15646	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = Σ𝑘 ∈ 𝐴 (log‘(𝐹‘𝑘)))
31	13	recnd 11239	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ)
32	5, 31	fsumneg 15730	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘(𝐹‘𝑘)) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
33	28, 30, 32	3eqtr2rd 2780	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))))
34	5, 31	gsumfsum 21005	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
35	34	negeqd 11451	. . . . . . . 8 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = -Σ𝑘 ∈ 𝐴 -(log‘(𝐹‘𝑘)))
36	10	feqmptd 6958	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
37		relogf1o 26067	. . . . . . . . . . . . 13 ⊢ (log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ
38		f1of 6831	. . . . . . . . . . . . 13 ⊢ ((log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
39	37, 38	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
40	39	feqmptd 6958	. . . . . . . . . . 11 ⊢ (𝜑 → (log ↾ ℝ⁺) = (𝑥 ∈ ℝ⁺ ↦ ((log ↾ ℝ⁺)‘𝑥)))
41		fvres 6908	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → ((log ↾ ℝ⁺)‘𝑥) = (log‘𝑥))
42	41	mpteq2ia 5251	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((log ↾ ℝ⁺)‘𝑥)) = (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥))
43	40, 42	eqtrdi 2789	. . . . . . . . . 10 ⊢ (𝜑 → (log ↾ ℝ⁺) = (𝑥 ∈ ℝ⁺ ↦ (log‘𝑥)))
44		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑥 = (𝐹‘𝑘) → (log‘𝑥) = (log‘(𝐹‘𝑘)))
45	11, 36, 43, 44	fmptco 7124	. . . . . . . . 9 ⊢ (𝜑 → ((log ↾ ℝ⁺) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘))))
46	45	oveq2d 7422	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘(𝐹‘𝑘)))))
47	33, 35, 46	3eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)))
48		amgm.1	. . . . . . . . . . . . . . 15 ⊢ 𝑀 = (mulGrp‘ℂ_fld)
49	48	oveq1i 7416	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↾_s (ℂ ∖ {0})) = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
50	49	rpmsubg 21002	. . . . . . . . . . . . 13 ⊢ ℝ⁺ ∈ (SubGrp‘(𝑀 ↾_s (ℂ ∖ {0})))
51		subgsubm 19023	. . . . . . . . . . . . 13 ⊢ (ℝ⁺ ∈ (SubGrp‘(𝑀 ↾_s (ℂ ∖ {0}))) → ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))))
52	50, 51	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0})))
53		cnfldbas 20941	. . . . . . . . . . . . . . 15 ⊢ ℂ = (Base‘ℂ_fld)
54		cndrng 20967	. . . . . . . . . . . . . . 15 ⊢ ℂ_fld ∈ DivRing
55	53, 1, 54	drngui 20314	. . . . . . . . . . . . . 14 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
56	55, 48	unitsubm 20193	. . . . . . . . . . . . 13 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
57		eqid 2733	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↾_s (ℂ ∖ {0})) = (𝑀 ↾_s (ℂ ∖ {0}))
58	57	subsubm 18694	. . . . . . . . . . . . 13 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))) ↔ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0}))))
59	2, 56, 58	mp2b 10	. . . . . . . . . . . 12 ⊢ (ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))) ↔ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0})))
60	52, 59	mpbi 229	. . . . . . . . . . 11 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0}))
61	60	simpli 485	. . . . . . . . . 10 ⊢ ℝ⁺ ∈ (SubMnd‘𝑀)
62		eqid 2733	. . . . . . . . . . 11 ⊢ (𝑀 ↾_s ℝ⁺) = (𝑀 ↾_s ℝ⁺)
63	62	submbas 18692	. . . . . . . . . 10 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → ℝ⁺ = (Base‘(𝑀 ↾_s ℝ⁺)))
64	61, 63	ax-mp 5	. . . . . . . . 9 ⊢ ℝ⁺ = (Base‘(𝑀 ↾_s ℝ⁺))
65		cnfld1 20963	. . . . . . . . . . . 12 ⊢ 1 = (1_r‘ℂ_fld)
66	48, 65	ringidval 20001	. . . . . . . . . . 11 ⊢ 1 = (0_g‘𝑀)
67	62, 66	subm0 18693	. . . . . . . . . 10 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → 1 = (0_g‘(𝑀 ↾_s ℝ⁺)))
68	61, 67	ax-mp 5	. . . . . . . . 9 ⊢ 1 = (0_g‘(𝑀 ↾_s ℝ⁺))
69		cncrng 20959	. . . . . . . . . . 11 ⊢ ℂ_fld ∈ CRing
70	48	crngmgp 20058	. . . . . . . . . . 11 ⊢ (ℂ_fld ∈ CRing → 𝑀 ∈ CMnd)
71	69, 70	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ CMnd)
72	62	submmnd 18691	. . . . . . . . . . 11 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → (𝑀 ↾_s ℝ⁺) ∈ Mnd)
73	61, 72	mp1i 13	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 ↾_s ℝ⁺) ∈ Mnd)
74	62	subcmn 19700	. . . . . . . . . 10 ⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾_s ℝ⁺) ∈ Mnd) → (𝑀 ↾_s ℝ⁺) ∈ CMnd)
75	71, 73, 74	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 ↾_s ℝ⁺) ∈ CMnd)
76		df-refld 21150	. . . . . . . . . . . 12 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
77	76	subrgring 20359	. . . . . . . . . . 11 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) → ℝ_fld ∈ Ring)
78	7, 77	ax-mp 5	. . . . . . . . . 10 ⊢ ℝ_fld ∈ Ring
79		ringmnd 20060	. . . . . . . . . 10 ⊢ (ℝ_fld ∈ Ring → ℝ_fld ∈ Mnd)
80	78, 79	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℝ_fld ∈ Mnd)
81	48	oveq1i 7416	. . . . . . . . . . . 12 ⊢ (𝑀 ↾_s ℝ⁺) = ((mulGrp‘ℂ_fld) ↾_s ℝ⁺)
82	81	reloggim 26099	. . . . . . . . . . 11 ⊢ (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpIso ℝ_fld)
83		gimghm 19133	. . . . . . . . . . 11 ⊢ ((log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpIso ℝ_fld) → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld))
84	82, 83	ax-mp 5	. . . . . . . . . 10 ⊢ (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld)
85		ghmmhm 19097	. . . . . . . . . 10 ⊢ ((log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld) → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) MndHom ℝ_fld))
86	84, 85	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) MndHom ℝ_fld))
87		1ex 11207	. . . . . . . . . . 11 ⊢ 1 ∈ V
88	87	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ V)
89	10, 5, 88	fdmfifsupp 9370	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 finSupp 1)
90	64, 68, 75, 80, 5, 86, 10, 89	gsummhm 19801	. . . . . . . 8 ⊢ (𝜑 → (ℝ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)) = ((log ↾ ℝ⁺)‘((𝑀 ↾_s ℝ⁺) Σ_g 𝐹)))
91		subgsubm 19023	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubGrp‘ℂ_fld) → ℝ ∈ (SubMnd‘ℂ_fld))
92	9, 91	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ℝ ∈ (SubMnd‘ℂ_fld))
93		fco 6739	. . . . . . . . . 10 ⊢ (((log ↾ ℝ⁺):ℝ⁺⟶ℝ ∧ 𝐹:𝐴⟶ℝ⁺) → ((log ↾ ℝ⁺) ∘ 𝐹):𝐴⟶ℝ)
94	39, 10, 93	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ((log ↾ ℝ⁺) ∘ 𝐹):𝐴⟶ℝ)
95	5, 92, 94, 76	gsumsubm 18713	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)) = (ℝ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)))
96	61	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ℝ⁺ ∈ (SubMnd‘𝑀))
97	5, 96, 10, 62	gsumsubm 18713	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 Σ_g 𝐹) = ((𝑀 ↾_s ℝ⁺) Σ_g 𝐹))
98	97	fveq2d 6893	. . . . . . . 8 ⊢ (𝜑 → ((log ↾ ℝ⁺)‘(𝑀 Σ_g 𝐹)) = ((log ↾ ℝ⁺)‘((𝑀 ↾_s ℝ⁺) Σ_g 𝐹)))
99	90, 95, 98	3eqtr4d 2783	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ 𝐹)) = ((log ↾ ℝ⁺)‘(𝑀 Σ_g 𝐹)))
100	66, 71, 5, 96, 10, 89	gsumsubmcl 19782	. . . . . . . 8 ⊢ (𝜑 → (𝑀 Σ_g 𝐹) ∈ ℝ⁺)
101	100	fvresd 6909	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ⁺)‘(𝑀 Σ_g 𝐹)) = (log‘(𝑀 Σ_g 𝐹)))
102	47, 99, 101	3eqtrd 2777	. . . . . 6 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (log‘(𝑀 Σ_g 𝐹)))
103	102	oveq1d 7421	. . . . 5 ⊢ (𝜑 → (-(ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((log‘(𝑀 Σ_g 𝐹)) / (♯‘𝐴)))
104	100	relogcld 26123	. . . . . . 7 ⊢ (𝜑 → (log‘(𝑀 Σ_g 𝐹)) ∈ ℝ)
105	104	recnd 11239	. . . . . 6 ⊢ (𝜑 → (log‘(𝑀 Σ_g 𝐹)) ∈ ℂ)
106	105, 24, 25	divrec2d 11991	. . . . 5 ⊢ (𝜑 → ((log‘(𝑀 Σ_g 𝐹)) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))))
107	26, 103, 106	3eqtrd 2777	. . . 4 ⊢ (𝜑 → -((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))))
108	36	oveq2d 7422	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g 𝐹) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))))
109	11	rpcnd 13015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ)
110	5, 109	gsumfsum 21005	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
111	108, 110	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g 𝐹) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘))
112	5, 20, 11	fsumrpcl 15680	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ ℝ⁺)
113	111, 112	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g 𝐹) ∈ ℝ⁺)
114	23	nnrpd 13011	. . . . . . 7 ⊢ (𝜑 → (♯‘𝐴) ∈ ℝ⁺)
115	113, 114	rpdivcld 13030	. . . . . 6 ⊢ (𝜑 → ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) ∈ ℝ⁺)
116	115	relogcld 26123	. . . . 5 ⊢ (𝜑 → (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ∈ ℝ)
117	18, 23	nndivred 12263	. . . . 5 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℝ)
118		rpssre 12978	. . . . . . . . 9 ⊢ ℝ⁺ ⊆ ℝ
119	118	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ⁺ ⊆ ℝ)
120		relogcl 26076	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ℝ⁺ → (log‘𝑤) ∈ ℝ)
121	120	adantl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (log‘𝑤) ∈ ℝ)
122	121	renegcld 11638	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → -(log‘𝑤) ∈ ℝ)
123	122	fmpttd 7112	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)):ℝ⁺⟶ℝ)
124		ioorp 13399	. . . . . . . . . . . 12 ⊢ (0(,)+∞) = ℝ⁺
125	124	eleq2i 2826	. . . . . . . . . . 11 ⊢ (𝑎 ∈ (0(,)+∞) ↔ 𝑎 ∈ ℝ⁺)
126	124	eleq2i 2826	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (0(,)+∞) ↔ 𝑏 ∈ ℝ⁺)
127		iccssioo2 13394	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
128	125, 126, 127	syl2anbr 600	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
129	128, 124	sseqtrdi 4032	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (𝑎[,]𝑏) ⊆ ℝ⁺)
130	129	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → (𝑎[,]𝑏) ⊆ ℝ⁺)
131	23	nnrecred 12260	. . . . . . . . . 10 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ)
132	114	rpreccld 13023	. . . . . . . . . . 11 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℝ⁺)
133	132	rpge0d 13017	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ (1 / (♯‘𝐴)))
134		elrege0 13428	. . . . . . . . . 10 ⊢ ((1 / (♯‘𝐴)) ∈ (0[,)+∞) ↔ ((1 / (♯‘𝐴)) ∈ ℝ ∧ 0 ≤ (1 / (♯‘𝐴))))
135	131, 133, 134	sylanbrc 584	. . . . . . . . 9 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ (0[,)+∞))
136		fconst6g 6778	. . . . . . . . 9 ⊢ ((1 / (♯‘𝐴)) ∈ (0[,)+∞) → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
137	135, 136	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶(0[,)+∞))
138		0lt1 11733	. . . . . . . . 9 ⊢ 0 < 1
139		fconstmpt 5737	. . . . . . . . . . 11 ⊢ (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))
140	139	oveq2i 7417	. . . . . . . . . 10 ⊢ (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))))
141		ringmnd 20060	. . . . . . . . . . . . 13 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ Mnd)
142	2, 141	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ_fld ∈ Mnd)
143	131	recnd 11239	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / (♯‘𝐴)) ∈ ℂ)
144		eqid 2733	. . . . . . . . . . . . 13 ⊢ (._g‘ℂ_fld) = (._g‘ℂ_fld)
145	53, 144	gsumconst 19797	. . . . . . . . . . . 12 ⊢ ((ℂ_fld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ (1 / (♯‘𝐴)) ∈ ℂ) → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(._g‘ℂ_fld)(1 / (♯‘𝐴))))
146	142, 5, 143, 145	syl3anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = ((♯‘𝐴)(._g‘ℂ_fld)(1 / (♯‘𝐴))))
147	23	nnzd 12582	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐴) ∈ ℤ)
148		cnfldmulg 20970	. . . . . . . . . . . 12 ⊢ (((♯‘𝐴) ∈ ℤ ∧ (1 / (♯‘𝐴)) ∈ ℂ) → ((♯‘𝐴)(._g‘ℂ_fld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
149	147, 143, 148	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴)(._g‘ℂ_fld)(1 / (♯‘𝐴))) = ((♯‘𝐴) · (1 / (♯‘𝐴))))
150	24, 25	recidd 11982	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘𝐴) · (1 / (♯‘𝐴))) = 1)
151	146, 149, 150	3eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = 1)
152	140, 151	eqtrid 2785	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})) = 1)
153	138, 152	breqtrrid 5186	. . . . . . . 8 ⊢ (𝜑 → 0 < (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))
154		logccv 26163	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
155	154	3adant1 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
156		ioossre 13382	. . . . . . . . . . . . . . 15 ⊢ (0(,)1) ⊆ ℝ
157		simp3 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0(,)1))
158	156, 157	sselid 3980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
159		simp21 1207	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ⁺)
160	159	relogcld 26123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
161	158, 160	remulcld 11241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
162		1re 11211	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
163		resubcl 11521	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
164	162, 158, 163	sylancr 588	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
165		simp22 1208	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ⁺)
166	165	relogcld 26123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
167	164, 166	remulcld 11241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
168	161, 167	readdcld 11240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
169		simp1 1137	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝜑)
170		ioossicc 13407	. . . . . . . . . . . . . . 15 ⊢ (0(,)1) ⊆ (0[,]1)
171	170, 157	sselid 3980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ (0[,]1))
172	119, 130	cvxcl 26479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ⁺)
173	169, 159, 165, 171, 172	syl13anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ⁺)
174	173	relogcld 26123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
175	168, 174	ltnegd 11789	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
176	155, 175	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
177		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
178	177	negeqd 11451	. . . . . . . . . . . 12 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
179		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))
180		negex 11455	. . . . . . . . . . . 12 ⊢ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
181	178, 179, 180	fvmpt 6996	. . . . . . . . . . 11 ⊢ (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
182	173, 181	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
183		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
184	183	negeqd 11451	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
185		negex 11455	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑥) ∈ V
186	184, 179, 185	fvmpt 6996	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
187	159, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
188	187	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
189	158	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
190	160	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
191	189, 190	mulneg2d 11665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
192	188, 191	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
193		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
194	193	negeqd 11451	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
195		negex 11455	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑦) ∈ V
196	194, 179, 195	fvmpt 6996	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
197	165, 196	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
198	197	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
199	164	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
200	166	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
201	199, 200	mulneg2d 11665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
202	198, 201	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
203	192, 202	oveq12d 7424	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
204	161	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
205	167	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
206	204, 205	negdid 11581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
207	203, 206	eqtr4d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
208	176, 182, 207	3brtr4d 5180	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))))
209	119, 123, 130, 208	scvxcvx 26480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ∧ 𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑣))))
210	119, 123, 130, 5, 137, 10, 153, 209	jensen 26483	. . . . . . 7 ⊢ (𝜑 → (((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))) ∈ ℝ⁺ ∧ ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))))
211	210	simprd 497	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))) ≤ ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))))
212	131	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈ ℝ)
213	139	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))))
214	5, 212, 11, 213, 36	offval2 7687	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘))))
215	214	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))))
216		cnfldmul 20943	. . . . . . . . . . . 12 ⊢ · = (._r‘ℂ_fld)
217	2	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ℂ_fld ∈ Ring)
218	109	fmpttd 7112	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)):𝐴⟶ℂ)
219	218, 5, 16	fdmfifsupp 9370	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) finSupp 0)
220	53, 1, 216, 217, 5, 143, 109, 219	gsummulc2 20123	. . . . . . . . . . 11 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · (𝐹‘𝑘)))) = ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))))
221		fss 6732	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶ℝ⁺ ∧ ℝ⁺ ⊆ ℝ) → 𝐹:𝐴⟶ℝ)
222	10, 118, 221	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)
223	10, 5, 16	fdmfifsupp 9370	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 finSupp 0)
224	1, 4, 5, 9, 222, 223	gsumsubgcl 19783	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (ℂ_fld Σ_g 𝐹) ∈ ℝ)
225	224	recnd 11239	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℂ_fld Σ_g 𝐹) ∈ ℂ)
226	225, 24, 25	divrec2d 11991	. . . . . . . . . . . 12 ⊢ (𝜑 → ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g 𝐹)))
227	108	oveq2d 7422	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g 𝐹)) = ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))))
228	226, 227	eqtr2d 2774	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))
229	215, 220, 228	3eqtrd 2777	. . . . . . . . . 10 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))
230	229, 152	oveq12d 7424	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) / 1))
231	224, 23	nndivred 12263	. . . . . . . . . . 11 ⊢ (𝜑 → ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) ∈ ℝ)
232	231	recnd 11239	. . . . . . . . . 10 ⊢ (𝜑 → ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) ∈ ℂ)
233	232	div1d 11979	. . . . . . . . 9 ⊢ (𝜑 → (((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) / 1) = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))
234	230, 233	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))
235	234	fveq2d 6893	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))) = ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
236		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑤 = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) → (log‘𝑤) = (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
237	236	negeqd 11451	. . . . . . . . 9 ⊢ (𝑤 = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) → -(log‘𝑤) = -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
238		negex 11455	. . . . . . . . 9 ⊢ -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ∈ V
239	237, 179, 238	fvmpt 6996	. . . . . . . 8 ⊢ (((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) = -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
240	115, 239	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) = -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
241	235, 240	eqtrd 2773	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · 𝐹)) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))})))) = -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
242	53, 1, 216, 217, 5, 143, 31, 17	gsummulc2 20123	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))) = ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
243		negex 11455	. . . . . . . . . . . 12 ⊢ -(log‘(𝐹‘𝑘)) ∈ V
244	243	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V)
245		eqidd 2734	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)))
246		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘)))
247	246	negeqd 11451	. . . . . . . . . . . 12 ⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘)))
248	11, 36, 245, 247	fmptco 7124	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
249	5, 212, 244, 213, 248	offval2 7687	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘)))))
250	249	oveq2d 7422	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((1 / (♯‘𝐴)) · -(log‘(𝐹‘𝑘))))))
251	19, 24, 25	divrec2d 11991	. . . . . . . . 9 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) = ((1 / (♯‘𝐴)) · (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
252	242, 250, 251	3eqtr4d 2783	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) = ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
253	252, 152	oveq12d 7424	. . . . . . 7 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))) = (((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1))
254	117	recnd 11239	. . . . . . . 8 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ∈ ℂ)
255	254	div1d 11979	. . . . . . 7 ⊢ (𝜑 → (((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) / 1) = ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
256	253, 255	eqtrd 2773	. . . . . 6 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝐴 × {(1 / (♯‘𝐴))}) ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g (𝐴 × {(1 / (♯‘𝐴))}))) = ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
257	211, 241, 256	3brtr3d 5179	. . . . 5 ⊢ (𝜑 → -(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ≤ ((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)))
258	116, 117, 257	lenegcon1d 11793	. . . 4 ⊢ (𝜑 → -((ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) / (♯‘𝐴)) ≤ (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
259	107, 258	eqbrtrrd 5172	. . 3 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))) ≤ (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))
260	131, 104	remulcld 11241	. . . 4 ⊢ (𝜑 → ((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))) ∈ ℝ)
261		efle 16058	. . . 4 ⊢ ((((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))) ∈ ℝ ∧ (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ∈ ℝ) → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))) ≤ (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹)))) ≤ (exp‘(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))))
262	260, 116, 261	syl2anc 585	. . 3 ⊢ (𝜑 → (((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹))) ≤ (log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))) ↔ (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹)))) ≤ (exp‘(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴))))))
263	259, 262	mpbid 231	. 2 ⊢ (𝜑 → (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹)))) ≤ (exp‘(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))))
264	100	rpcnd 13015	. . 3 ⊢ (𝜑 → (𝑀 Σ_g 𝐹) ∈ ℂ)
265	100	rpne0d 13018	. . 3 ⊢ (𝜑 → (𝑀 Σ_g 𝐹) ≠ 0)
266	264, 265, 143	cxpefd 26212	. 2 ⊢ (𝜑 → ((𝑀 Σ_g 𝐹)↑_𝑐(1 / (♯‘𝐴))) = (exp‘((1 / (♯‘𝐴)) · (log‘(𝑀 Σ_g 𝐹)))))
267	115	reeflogd 26124	. . 3 ⊢ (𝜑 → (exp‘(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))) = ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))
268	267	eqcomd 2739	. 2 ⊢ (𝜑 → ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)) = (exp‘(log‘((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))))
269	263, 266, 268	3brtr4d 5180	1 ⊢ (𝜑 → ((𝑀 Σ_g 𝐹)↑_𝑐(1 / (♯‘𝐴))) ≤ ((ℂ_fld Σ_g 𝐹) / (♯‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 Vcvv 3475 ∖ cdif 3945 ⊆ wss 3948 ∅c0 4322 {csn 4628 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 ↾ cres 5678 ∘ ccom 5680 ⟶wf 6537 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 ∘_f cof 7665 Fincfn 8936 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 +∞cpnf 11242 < clt 11245 ≤ cle 11246 − cmin 11441 -cneg 11442 / cdiv 11868 ℕcn 12209 ℤcz 12555 ℝ⁺crp 12971 (,)cioo 13321 [,)cico 13323 [,]cicc 13324 ♯chash 14287 Σcsu 15629 expce 16002 Basecbs 17141 ↾_s cress 17170 0_gc0g 17382 Σ_g cgsu 17383 Mndcmnd 18622 MndHom cmhm 18666 SubMndcsubmnd 18667 ._gcmg 18945 SubGrpcsubg 18995 GrpHom cghm 19084 GrpIso cgim 19126 CMndccmn 19643 Abelcabl 19644 mulGrpcmgp 19982 Ringcrg 20050 CRingccrg 20051 DivRingcdr 20308 SubRingcsubrg 20352 ℂ_fldccnfld 20937 ℝ_fldcrefld 21149 logclog 26055 ↑_𝑐ccxp 26056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-mhm 18668 df-submnd 18669 df-grp 18819 df-minusg 18820 df-mulg 18946 df-subg 18998 df-ghm 19085 df-gim 19128 df-cntz 19176 df-cmn 19645 df-abl 19646 df-mgp 19983 df-ur 20000 df-ring 20052 df-cring 20053 df-oppr 20143 df-dvdsr 20164 df-unit 20165 df-invr 20195 df-dvr 20208 df-drng 20310 df-subrg 20354 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-refld 21150 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-cmp 22883 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-limc 25375 df-dv 25376 df-log 26057 df-cxp 26058

This theorem is referenced by: amgm 26485 amgm2d 42936 amgm3d 42937 amgm4d 42938

W3C validator