jensen - Metamath Proof Explorer

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

Theorem jensen 25127

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.) (Proof shortened by AV, 27-Jul-2019.)

**Hypotheses**
Ref	Expression
jensen.1	⊢ (𝜑 → 𝐷 ⊆ ℝ)
jensen.2	⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
jensen.3	⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
jensen.4	⊢ (𝜑 → 𝐴 ∈ Fin)
jensen.5	⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))
jensen.6	⊢ (𝜑 → 𝑋:𝐴⟶𝐷)
jensen.7	⊢ (𝜑 → 0 < (ℂ_fld Σ_g 𝑇))
jensen.8	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))

**Assertion**
Ref	Expression
jensen	⊢ (𝜑 → (((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇))) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))))

Distinct variable groups: 𝑎,𝑏,𝑡,𝑥,𝑦,𝐴 𝐷,𝑎,𝑏,𝑡,𝑥,𝑦 𝜑,𝑎,𝑏,𝑡,𝑥,𝑦 𝐹,𝑎,𝑏,𝑡,𝑥,𝑦 𝑇,𝑎,𝑏,𝑡,𝑥,𝑦 𝑋,𝑎,𝑏,𝑡,𝑥,𝑦

Proof of Theorem jensen Dummy variables 𝑐 𝑘 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		jensen.7	. . . . . 6 ⊢ (𝜑 → 0 < (ℂ_fld Σ_g 𝑇))
2		jensen.5	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))
3	2	ffnd 6278	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn 𝐴)
4		fnresdm 6232	. . . . . . . 8 ⊢ (𝑇 Fn 𝐴 → (𝑇 ↾ 𝐴) = 𝑇)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑇 ↾ 𝐴) = 𝑇)
6	5	oveq2d 6920	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑇 ↾ 𝐴)) = (ℂ_fld Σ_g 𝑇))
7	1, 6	breqtrrd 4900	. . . . 5 ⊢ (𝜑 → 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))
8		ssid 3847	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
9	7, 8	jctil 517	. . . 4 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))))
10		jensen.4	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		sseq1 3850	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
12		reseq2 5623	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = (𝑇 ↾ ∅))
13		res0 5632	. . . . . . . . . . . . 13 ⊢ (𝑇 ↾ ∅) = ∅
14	12, 13	syl6eq 2876	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = ∅)
15	14	oveq2d 6920	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) = (ℂ_fld Σ_g ∅))
16		cnfld0 20129	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘ℂ_fld)
17	16	gsum0 17630	. . . . . . . . . . 11 ⊢ (ℂ_fld Σ_g ∅) = 0
18	15, 17	syl6eq 2876	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) = 0)
19	18	breq2d 4884	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) ↔ 0 < 0))
20	11, 19	anbi12d 626	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅))
22	21	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)))
23	22, 18	oveq12d 6922	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0))
24		reseq2 5623	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅))
25	24	oveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)))
26	25, 18	oveq12d 6922	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0))
27	26	breq2d 4884	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)))
28	27	rabbidv 3401	. . . . . . . . 9 ⊢ (𝑎 = ∅ → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
29	23, 28	eleq12d 2899	. . . . . . . 8 ⊢ (𝑎 = ∅ → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} ↔ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))
30	20, 29	imbi12d 336	. . . . . . 7 ⊢ (𝑎 = ∅ → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})))
31	30	imbi2d 332	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))))
32		sseq1 3850	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (𝑎 ⊆ 𝐴 ↔ 𝑘 ⊆ 𝐴))
33		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝑘))
34	33	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) = (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
35	34	breq2d 4884	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) ↔ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
36	32, 35	anbi12d 626	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
37		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘))
38	37	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)))
39	38, 34	oveq12d 6922	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
40		reseq2 5623	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘))
41	40	oveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑘 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)))
42	41, 34	oveq12d 6922	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
43	42	breq2d 4884	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
44	43	rabbidv 3401	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})
45	39, 44	eleq12d 2899	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} ↔ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}))
46	36, 45	imbi12d 336	. . . . . . 7 ⊢ (𝑎 = 𝑘 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))}) ↔ ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})))
47	46	imbi2d 332	. . . . . 6 ⊢ (𝑎 = 𝑘 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}))))
48		sseq1 3850	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎 ⊆ 𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇 ↾ 𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
50	49	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) = (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))
51	50	breq2d 4884	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) ↔ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))))
52	48, 51	anbi12d 626	. . . . . . . 8 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})))
54	53	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
55	54, 50	oveq12d 6922	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56		reseq2 5623	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})))
57	56	oveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))))
58	57, 50	oveq12d 6922	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))))
59	58	breq2d 4884	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
60	59	rabbidv 3401	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
61	55, 60	eleq12d 2899	. . . . . . . 8 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} ↔ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
62	52, 61	imbi12d 336	. . . . . . 7 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))}) ↔ (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
63	62	imbi2d 332	. . . . . 6 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
64		sseq1 3850	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
65		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝐴))
66	65	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) = (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))
67	66	breq2d 4884	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎)) ↔ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))))
68	64, 67	anbi12d 626	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))))
69		reseq2 5623	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴))
70	69	oveq2d 6920	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)))
71	70, 66	oveq12d 6922	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))))
72		reseq2 5623	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴))
73	72	oveq2d 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)))
74	73, 66	oveq12d 6922	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))))
75	74	breq2d 4884	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))))
76	75	rabbidv 3401	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))})
77	71, 76	eleq12d 2899	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))} ↔ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))}))
78	68, 77	imbi12d 336	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))}) ↔ ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))})))
79	78	imbi2d 332	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))}))))
80		0re 10357	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
81	80	ltnri 10464	. . . . . . . . 9 ⊢ ¬ 0 < 0
82	81	pm2.21i 117	. . . . . . . 8 ⊢ (0 < 0 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
83	82	adantl 475	. . . . . . 7 ⊢ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
84	83	a1i 11	. . . . . 6 ⊢ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))
85		impexp 443	. . . . . . . . . . . 12 ⊢ (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) ↔ (𝑘 ⊆ 𝐴 → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})))
86		simprl 789	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
87	86	unssad 4016	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ⊆ 𝐴)
88		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
89		jensen.1	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
90	89	ad3antrrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝐷 ⊆ ℝ)
91		jensen.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
92	91	ad3antrrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝐹:𝐷⟶ℝ)
93		simplll 793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝜑)
94		jensen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
95	93, 94	sylan 577	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
96	93, 10	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝐴 ∈ Fin)
97	93, 2	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝑇:𝐴⟶(0[,)+∞))
98		jensen.6	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)
99	93, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 𝑋:𝐴⟶𝐷)
100	1	ad3antrrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 0 < (ℂ_fld Σ_g 𝑇))
101		jensen.8	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
102	93, 101	sylan 577	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
103		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → ¬ 𝑐 ∈ 𝑘)
104	86	adantr 474	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
105		eqid 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))
106		eqid 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))
107		cnring 20127	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℂ_fld ∈ Ring
108		ringcmn 18934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
109	107, 108	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂ_fld ∈ CMnd)
110	10	ad2antrr 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111		ssfi 8448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin)
112	110, 87, 111	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
113		rege0subm 20161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,)+∞) ∈ (SubMnd‘ℂ_fld)
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂ_fld))
115	2	ad2antrr 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
116	115, 87	fssresd 6307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘):𝑘⟶(0[,)+∞))
117		c0ex 10349	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
118	117	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
119	116, 112, 118	fdmfifsupp 8553	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘) finSupp 0)
120	16, 109, 112, 114, 116, 119	gsumsubmcl 18671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ (0[,)+∞))
121		elrege0 12567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) ↔ ((ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ ∧ 0 ≤ (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
122	121	simplbi 493	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ)
123	120, 122	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ)
124	123	adantr 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ)
125		simprl 789	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
126	124, 125	elrpd 12152	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ⁺)
127		simprr 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})
128		fveq2 6432	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘𝑤) = (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
129	128	breq1d 4882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ↔ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
130	129	elrab 3584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))} ↔ (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
131	127, 130	sylib 210	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
132	131	simpld 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ 𝐷)
133	131	simprd 491	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
134	90, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 126, 132, 133	jensenlem2 25126	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135		fveq2 6432	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹‘𝑤) = (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136	135	breq1d 4882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
137	136	elrab 3584	. . . . . . . . . . . . . . . . 17 ⊢ (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))} ↔ (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
138	134, 137	sylibr 226	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∧ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
139	138	expr 450	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))} → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
140	88, 139	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
141		cnfldbas 20109	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = (Base‘ℂ_fld)
142		ringmnd 18909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ Mnd)
143	107, 142	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ℂ_fld ∈ Mnd)
144		ssfi 8448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ Fin ∧ (𝑘 ∪ {𝑐}) ⊆ 𝐴) → (𝑘 ∪ {𝑐}) ∈ Fin)
145	110, 86, 144	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
146	145	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
147		ssun2 4003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐} ⊆ (𝑘 ∪ {𝑐})
148		vsnid 4429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑐 ∈ {𝑐}
149	147, 148	sselii 3823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ (𝑘 ∪ {𝑐})
150	149	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
151		remulcl 10336	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
152	151	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
153		rge0ssre 12569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
154		fss 6290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
155	2, 153, 154	sylancl 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑇:𝐴⟶ℝ)
156	98, 89	fssd 6291	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋:𝐴⟶ℝ)
157		inidm 4046	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝐴) = 𝐴
158	152, 155, 156, 10, 10, 157	off 7171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘_𝑓 · 𝑋):𝐴⟶ℝ)
159		ax-resscn 10308	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℝ ⊆ ℂ
160		fss 6290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘_𝑓 · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘_𝑓 · 𝑋):𝐴⟶ℂ)
161	158, 159, 160	sylancl 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘_𝑓 · 𝑋):𝐴⟶ℂ)
162	161	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇 ∘_𝑓 · 𝑋):𝐴⟶ℂ)
163	86	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
164	162, 163	fssresd 6307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
165	2	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
166	110	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝐴 ∈ Fin)
167		fex 6744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V)
168	165, 166, 167	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑇 ∈ V)
169	98	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶𝐷)
170		fex 6744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝐴 ∈ Fin) → 𝑋 ∈ V)
171	169, 166, 170	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑋 ∈ V)
172		offres 7422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
173	168, 171, 172	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
174	173	oveq1d 6919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
175	153, 159	sstri 3835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℂ
176		fss 6290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
177	165, 175, 176	sylancl 582	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶ℂ)
178	177, 163	fssresd 6307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
179		eldifi 3958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
180	179	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
181		fvres 6451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥))
182	180, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥))
183		difun2 4270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
184		difss 3963	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∖ {𝑐}) ⊆ 𝑘
185	183, 184	eqsstri 3859	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
186	185	sseli 3822	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ 𝑘)
187		simpr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
188	87	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑘 ⊆ 𝐴)
189	165, 188	feqresmpt 6496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇 ↾ 𝑘) = (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥)))
190	189	oveq2d 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) = (ℂ_fld Σ_g (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))))
191	112	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑘 ∈ Fin)
192	188	sselda 3826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
193	165	ffvelrnda 6607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞))
194	192, 193	syldan 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ (0[,)+∞))
195	175, 194	sseldi 3824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℂ)
196	191, 195	gsumfsum 20172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))) = Σ𝑥 ∈ 𝑘 (𝑇‘𝑥))
197	187, 190, 196	3eqtrrd 2865	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
198		elrege0 12567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑇‘𝑥) ∈ (0[,)+∞) ↔ ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
199	194, 198	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
200	199	simpld 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℝ)
201	199	simprd 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 0 ≤ (𝑇‘𝑥))
202	191, 200, 201	fsum00 14903	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0))
203	197, 202	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
204	203	r19.21bi 3140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) = 0)
205	186, 204	sylan2 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇‘𝑥) = 0)
206	182, 205	eqtrd 2860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
207	178, 206	suppss 7589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
208		mul02 10532	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
209	208	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
210	89	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℝ)
211	210, 159	syl6ss 3838	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℂ)
212	169, 211	fssd 6291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶ℂ)
213	212, 163	fssresd 6307	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
214	117	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 0 ∈ V)
215	207, 209, 178, 213, 146, 214	suppssof1 7592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
216	174, 215	eqsstrd 3863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
217	141, 16, 143, 146, 150, 164, 216	gsumpt 18713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
218		fvres 6451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘_𝑓 · 𝑋)‘𝑐))
219	150, 218	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘_𝑓 · 𝑋)‘𝑐))
220	165	ffnd 6278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑇 Fn 𝐴)
221	169	ffnd 6278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑋 Fn 𝐴)
222	163, 150	sseldd 3827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝑐 ∈ 𝐴)
223		fnfvof 7170	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑇 Fn 𝐴 ∧ 𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘_𝑓 · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
224	220, 221, 166, 222, 223	syl22anc 874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
225	217, 219, 224	3eqtrd 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
226	141, 16, 143, 146, 150, 178, 207	gsumpt 18713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
227		fvres 6451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐))
228	150, 227	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐))
229	226, 228	eqtrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇‘𝑐))
230	225, 229	oveq12d 6922	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)))
231	212, 222	ffvelrnd 6608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ ℂ)
232	177, 222	ffvelrnd 6608	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ∈ ℂ)
233		simplrr 798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))
234	233, 229	breqtrd 4898	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 0 < (𝑇‘𝑐))
235	234	gt0ne0d 10915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ≠ 0)
236	231, 232, 235	divcan3d 11131	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)) = (𝑋‘𝑐))
237	230, 236	eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋‘𝑐))
238	169, 222	ffvelrnd 6608	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ 𝐷)
239	237, 238	eqeltrd 2905	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
240	91	ad3antrrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → 𝐹:𝐷⟶ℝ)
241	240, 238	ffvelrnd 6608	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℝ)
242	241	leidd 10917	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ≤ (𝐹‘(𝑋‘𝑐)))
243	237	fveq2d 6436	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋‘𝑐)))
244		fco 6294	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
245	91, 98, 244	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
246	152, 155, 245, 10, 10, 157	off 7171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℝ)
247		fss 6290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
248	246, 159, 247	sylancl 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
249	248	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
250	249, 163	fssresd 6307	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
251	245	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
252		fex 6744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹 ∘ 𝑋) ∈ V)
253	251, 166, 252	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) ∈ V)
254		offres 7422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ (𝐹 ∘ 𝑋) ∈ V) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
255	168, 253, 254	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
256	255	oveq1d 6919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
257		fss 6290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
258	251, 159, 257	sylancl 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
259	258, 163	fssresd 6307	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
260	207, 209, 178, 259, 146, 214	suppssof1 7592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘_𝑓 · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
261	256, 260	eqsstrd 3863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
262	141, 16, 143, 146, 150, 250, 261	gsumpt 18713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
263		fvres 6451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))‘𝑐))
264	150, 263	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))‘𝑐))
265	91	ffnd 6278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn 𝐷)
266		fnfco 6305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 Fn 𝐷 ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋) Fn 𝐴)
267	265, 98, 266	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∘ 𝑋) Fn 𝐴)
268	267	ad3antrrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) Fn 𝐴)
269		fnfvof 7170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑇 Fn 𝐴 ∧ (𝐹 ∘ 𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
270	220, 268, 166, 222, 269	syl22anc 874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
271		fvco3 6521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝑐 ∈ 𝐴) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
272	169, 222, 271	syl2anc 581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
273	272	oveq2d 6920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
274	270, 273	eqtrd 2860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
275	262, 264, 274	3eqtrd 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
276	275, 229	oveq12d 6922	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)))
277	241	recnd 10384	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℂ)
278	277, 232, 235	divcan3d 11131	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)) = (𝐹‘(𝑋‘𝑐)))
279	276, 278	eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋‘𝑐)))
280	242, 243, 279	3brtr4d 4904	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → (𝐹‘((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))))
281	239, 280, 137	sylanbrc 580	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
282	281	a1d 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
283	121	simprbi 492	. . . . . . . . . . . . . . . 16 ⊢ ((ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
284	120, 283	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))
285		leloe 10442	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∈ ℝ) → (0 ≤ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ↔ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∨ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
286	80, 123, 285	sylancr 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ↔ (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∨ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))))
287	284, 286	mpbid 224	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) ∨ 0 = (ℂ_fld Σ_g (𝑇 ↾ 𝑘))))
288	140, 282, 287	mpjaodan 988	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
289	87, 288	embantd 59	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((𝑘 ⊆ 𝐴 → (0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘)) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
290	85, 289	syl5bi 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
291	290	ex 403	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
292	291	com23 86	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
293	292	expcom 404	. . . . . . . 8 ⊢ (¬ 𝑐 ∈ 𝑘 → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
294	293	adantl 475	. . . . . . 7 ⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
295	294	a2d 29	. . . . . 6 ⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → ((𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂ_fld Σ_g (𝑇 ↾ 𝑘)))})) → (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂ_fld Σ_g (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
296	31, 47, 63, 79, 84, 295	findcard2s 8469	. . . . 5 ⊢ (𝐴 ∈ Fin → (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))})))
297	10, 296	mpcom 38	. . . 4 ⊢ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))}))
298	9, 297	mpd 15	. . 3 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))})
299	158	ffnd 6278	. . . . . 6 ⊢ (𝜑 → (𝑇 ∘_𝑓 · 𝑋) Fn 𝐴)
300		fnresdm 6232	. . . . . 6 ⊢ ((𝑇 ∘_𝑓 · 𝑋) Fn 𝐴 → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴) = (𝑇 ∘_𝑓 · 𝑋))
301	299, 300	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴) = (𝑇 ∘_𝑓 · 𝑋))
302	301	oveq2d 6920	. . . 4 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) = (ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)))
303	302, 6	oveq12d 6922	. . 3 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · 𝑋) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) = ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)))
304	3, 267, 10, 10, 157	offn 7167	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) Fn 𝐴)
305		fnresdm 6232	. . . . . . . 8 ⊢ ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) Fn 𝐴 → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)))
306	304, 305	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)))
307	306	oveq2d 6920	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) = (ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))))
308	307, 6	oveq12d 6922	. . . . 5 ⊢ (𝜑 → ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) = ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇)))
309	308	breq2d 4884	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴))) ↔ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))))
310	309	rabbidv 3401	. . 3 ⊢ (𝜑 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g ((𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂ_fld Σ_g (𝑇 ↾ 𝐴)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))})
311	298, 303, 310	3eltr3d 2919	. 2 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))})
312		fveq2 6432	. . . 4 ⊢ (𝑤 = ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) → (𝐹‘𝑤) = (𝐹‘((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇))))
313	312	breq1d 4882	. . 3 ⊢ (𝑤 = ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) → ((𝐹‘𝑤) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇)) ↔ (𝐹‘((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇))) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))))
314	313	elrab 3584	. 2 ⊢ (((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))} ↔ (((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇))) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))))
315	311, 314	sylib 210	1 ⊢ (𝜑 → (((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂ_fld Σ_g (𝑇 ∘_𝑓 · 𝑋)) / (ℂ_fld Σ_g 𝑇))) ≤ ((ℂ_fld Σ_g (𝑇 ∘_𝑓 · (𝐹 ∘ 𝑋))) / (ℂ_fld Σ_g 𝑇))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 880 ∧ w3a 1113 = wceq 1658 ∈ wcel 2166 ∀wral 3116 {crab 3120 Vcvv 3413 ∖ cdif 3794 ∪ cun 3795 ⊆ wss 3797 ∅c0 4143 {csn 4396 class class class wbr 4872 ↦ cmpt 4951 ↾ cres 5343 ∘ ccom 5345 Fn wfn 6117 ⟶wf 6118 ‘cfv 6122 (class class class)co 6904 ∘_𝑓 cof 7154 supp csupp 7558 Fincfn 8221 ℂcc 10249 ℝcr 10250 0cc0 10251 1c1 10252 + caddc 10254 · cmul 10256 +∞cpnf 10387 < clt 10390 ≤ cle 10391 − cmin 10584 / cdiv 11008 [,)cico 12464 [,]cicc 12465 Σcsu 14792 Σ_g cgsu 16453 Mndcmnd 17646 SubMndcsubmnd 17686 CMndccmn 18545 Ringcrg 18900 ℂ_fldccnfld 20105

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-rep 4993 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 ax-inf2 8814 ax-cnex 10307 ax-resscn 10308 ax-1cn 10309 ax-icn 10310 ax-addcl 10311 ax-addrcl 10312 ax-mulcl 10313 ax-mulrcl 10314 ax-mulcom 10315 ax-addass 10316 ax-mulass 10317 ax-distr 10318 ax-i2m1 10319 ax-1ne0 10320 ax-1rid 10321 ax-rnegex 10322 ax-rrecex 10323 ax-cnre 10324 ax-pre-lttri 10325 ax-pre-lttrn 10326 ax-pre-ltadd 10327 ax-pre-mulgt0 10328 ax-pre-sup 10329 ax-addf 10330 ax-mulf 10331

This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-fal 1672 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-nel 3102 df-ral 3121 df-rex 3122 df-reu 3123 df-rmo 3124 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-pss 3813 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-tp 4401 df-op 4403 df-uni 4658 df-int 4697 df-iun 4741 df-iin 4742 df-br 4873 df-opab 4935 df-mpt 4952 df-tr 4975 df-id 5249 df-eprel 5254 df-po 5262 df-so 5263 df-fr 5300 df-se 5301 df-we 5302 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-rn 5352 df-res 5353 df-ima 5354 df-pred 5919 df-ord 5965 df-on 5966 df-lim 5967 df-suc 5968 df-iota 6085 df-fun 6124 df-fn 6125 df-f 6126 df-f1 6127 df-fo 6128 df-f1o 6129 df-fv 6130 df-isom 6131 df-riota 6865 df-ov 6907 df-oprab 6908 df-mpt2 6909 df-of 7156 df-om 7326 df-1st 7427 df-2nd 7428 df-supp 7559 df-tpos 7616 df-wrecs 7671 df-recs 7733 df-rdg 7771 df-1o 7825 df-oadd 7829 df-er 8008 df-en 8222 df-dom 8223 df-sdom 8224 df-fin 8225 df-fsupp 8544 df-sup 8616 df-oi 8683 df-card 9077 df-pnf 10392 df-mnf 10393 df-xr 10394 df-ltxr 10395 df-le 10396 df-sub 10586 df-neg 10587 df-div 11009 df-nn 11350 df-2 11413 df-3 11414 df-4 11415 df-5 11416 df-6 11417 df-7 11418 df-8 11419 df-9 11420 df-n0 11618 df-z 11704 df-dec 11821 df-uz 11968 df-rp 12112 df-ico 12468 df-icc 12469 df-fz 12619 df-fzo 12760 df-seq 13095 df-exp 13154 df-hash 13410 df-cj 14215 df-re 14216 df-im 14217 df-sqrt 14351 df-abs 14352 df-clim 14595 df-sum 14793 df-struct 16223 df-ndx 16224 df-slot 16225 df-base 16227 df-sets 16228 df-ress 16229 df-plusg 16317 df-mulr 16318 df-starv 16319 df-tset 16323 df-ple 16324 df-ds 16326 df-unif 16327 df-0g 16454 df-gsum 16455 df-mre 16598 df-mrc 16599 df-acs 16601 df-mgm 17594 df-sgrp 17636 df-mnd 17647 df-submnd 17688 df-grp 17778 df-minusg 17779 df-mulg 17894 df-subg 17941 df-cntz 18099 df-cmn 18547 df-abl 18548 df-mgp 18843 df-ur 18855 df-ring 18902 df-cring 18903 df-oppr 18976 df-dvdsr 18994 df-unit 18995 df-invr 19025 df-dvr 19036 df-drng 19104 df-subrg 19133 df-cnfld 20106 df-refld 20311

This theorem is referenced by: amgmlem 25128 amgmwlem 43443

W3C validator