Theorem jensen 25560

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 (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂ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 6509	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn 𝐴)
4		fnresdm 6460	. . . . . . . 8 ⊢ (𝑇 Fn 𝐴 → (𝑇 ↾ 𝐴) = 𝑇)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑇 ↾ 𝐴) = 𝑇)
6	5	oveq2d 7166	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑇 ↾ 𝐴)) = (ℂfld Σg 𝑇))
7	1, 6	breqtrrd 5086	. . . . 5 ⊢ (𝜑 → 0 < (ℂfld Σg (𝑇 ↾ 𝐴)))
8		ssid 3988	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
9	7, 8	jctil 522	. . . 4 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))))
10		jensen.4	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		sseq1 3991	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
12		reseq2 5842	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = (𝑇 ↾ ∅))
13		res0 5851	. . . . . . . . . . . . 13 ⊢ (𝑇 ↾ ∅) = ∅
14	12, 13	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = ∅)
15	14	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg ∅))
16		cnfld0 20563	. . . . . . . . . . . 12 ⊢ 0 = (0g‘ℂfld)
17	16	gsum0 17888	. . . . . . . . . . 11 ⊢ (ℂfld Σg ∅) = 0
18	15, 17	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂfld Σg (𝑇 ↾ 𝑎)) = 0)
19	18	breq2d 5070	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < 0))
20	11, 19	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ ∅))
22	21	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)))
23	22, 18	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0))
24		reseq2 5842	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅))
25	24	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)))
26	25, 18	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0))
27	26	breq2d 5070	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)))
28	27	rabbidv 3480	. . . . . . . . 9 ⊢ (𝑎 = ∅ → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
29	23, 28	eleq12d 2907	. . . . . . . 8 ⊢ (𝑎 = ∅ → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))
30	20, 29	imbi12d 347	. . . . . . 7 ⊢ (𝑎 = ∅ → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})))
31	30	imbi2d 343	. . . . . 6 ⊢ (𝑎 = ∅ → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))))
32		sseq1 3991	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (𝑎 ⊆ 𝐴 ↔ 𝑘 ⊆ 𝐴))
33		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝑘))
34	33	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ 𝑘)))
35	34	breq2d 5070	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))))
36	32, 35	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))))
37		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ 𝑘))
38	37	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)))
39	38, 34	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))))
40		reseq2 5842	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘))
41	40	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑘 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)))
42	41, 34	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))))
43	42	breq2d 5070	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
44	43	rabbidv 3480	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})
45	39, 44	eleq12d 2907	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}))
46	36, 45	imbi12d 347	. . . . . . 7 ⊢ (𝑎 = 𝑘 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))}) ↔ ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})))
47	46	imbi2d 343	. . . . . 6 ⊢ (𝑎 = 𝑘 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}))))
48		sseq1 3991	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎 ⊆ 𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇 ↾ 𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
50	49	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
51	50	breq2d 5070	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
52	48, 51	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})))
54	53	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
55	54, 50	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56		reseq2 5842	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})))
57	56	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))))
58	57, 50	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
59	58	breq2d 5070	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
60	59	rabbidv 3480	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
61	55, 60	eleq12d 2907	. . . . . . . 8 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
62	52, 61	imbi12d 347	. . . . . . 7 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))}) ↔ (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
63	62	imbi2d 343	. . . . . 6 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
64		sseq1 3991	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
65		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝐴))
66	65	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ 𝐴)))
67	66	breq2d 5070	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))))
68	64, 67	anbi12d 632	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴)))))
69		reseq2 5842	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ 𝐴))
70	69	oveq2d 7166	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)))
71	70, 66	oveq12d 7168	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))))
72		reseq2 5842	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴))
73	72	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)))
74	73, 66	oveq12d 7168	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))))
75	74	breq2d 5070	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))))
76	75	rabbidv 3480	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))})
77	71, 76	eleq12d 2907	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))}))
78	68, 77	imbi12d 347	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))}) ↔ ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))})))
79	78	imbi2d 343	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))}))))
80		0re 10637	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
81	80	ltnri 10743	. . . . . . . . 9 ⊢ ¬ 0 < 0
82	81	pm2.21i 119	. . . . . . . 8 ⊢ (0 < 0 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
83	82	adantl 484	. . . . . . 7 ⊢ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
84	83	a1i 11	. . . . . 6 ⊢ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))
85		impexp 453	. . . . . . . . . . . 12 ⊢ (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) ↔ (𝑘 ⊆ 𝐴 → (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})))
86		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
87	86	unssad 4162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ⊆ 𝐴)
88		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))
89		jensen.1	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
90	89	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝐷 ⊆ ℝ)
91		jensen.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
92	91	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝐹:𝐷⟶ℝ)
93		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝜑)
94		jensen.3	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
95	93, 94	sylan 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
96	93, 10	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝐴 ∈ Fin)
97	93, 2	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝑇:𝐴⟶(0[,)+∞))
98		jensen.6	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)
99	93, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝑋:𝐴⟶𝐷)
100	1	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 0 < (ℂfld Σg 𝑇))
101		jensen.8	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
102	93, 101	sylan 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
103		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ¬ 𝑐 ∈ 𝑘)
104	86	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
105		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld Σg (𝑇 ↾ 𝑘)) = (ℂfld Σg (𝑇 ↾ 𝑘))
106		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))
107		cnring 20561	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℂfld ∈ Ring
108		ringcmn 19325	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109	107, 108	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
110	10	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111	110, 87	ssfid 8735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
112		rege0subm 20595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
114	2	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
115	114, 87	fssresd 6539	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘):𝑘⟶(0[,)+∞))
116		c0ex 10629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
117	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
118	115, 111, 117	fdmfifsupp 8837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘) finSupp 0)
119	16, 109, 111, 113, 115, 118	gsumsubmcl 19033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞))
120		elrege0 12836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) ↔ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ ∧ 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘))))
121	120	simplbi 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
122	119, 121	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
123	122	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
124		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))
125	123, 124	elrpd 12422	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ+)
126		simprr 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})
127		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
128	127	breq1d 5068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
129	128	elrab 3679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))} ↔ (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
130	126, 129	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
131	130	simpld 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ 𝐷)
132	130	simprd 498	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))))
133	90, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 125, 131, 132	jensenlem2 25559	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
134		fveq2 6664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135	134	breq1d 5068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136	135	elrab 3679	. . . . . . . . . . . . . . . . 17 ⊢ (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))} ↔ (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
137	133, 136	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
138	137	expr 459	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))} → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
139	88, 138	embantd 59	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((0 < (ℂfld Σg (𝑇 ↾ 𝑘)) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
140		cnfldbas 20543	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = (Base‘ℂfld)
141		ringmnd 19300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
142	107, 141	mp1i 13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ℂfld ∈ Mnd)
143	110, 86	ssfid 8735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
144	143	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
145		ssun2 4148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐} ⊆ (𝑘 ∪ {𝑐})
146		vsnid 4595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑐 ∈ {𝑐}
147	145, 146	sselii 3963	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ (𝑘 ∪ {𝑐})
148	147	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
149		remulcl 10616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
150	149	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
151		rge0ssre 12838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
152		fss 6521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
153	2, 151, 152	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑇:𝐴⟶ℝ)
154	98, 89	fssd 6522	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋:𝐴⟶ℝ)
155		inidm 4194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝐴) = 𝐴
156	150, 153, 154, 10, 10, 155	off 7418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘f · 𝑋):𝐴⟶ℝ)
157		ax-resscn 10588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℝ ⊆ ℂ
158		fss 6521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘f · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
159	156, 157, 158	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
160	159	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
161	86	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
162	160, 161	fssresd 6539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
163	2	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
164	110	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐴 ∈ Fin)
165		fex 6983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V)
166	163, 164, 165	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇 ∈ V)
167	98	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶𝐷)
168		fex 6983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝐴 ∈ Fin) → 𝑋 ∈ V)
169	167, 164, 168	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋 ∈ V)
170		offres 7678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
171	166, 169, 170	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
172	171	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
173	151, 157	sstri 3975	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℂ
174		fss 6521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
175	163, 173, 174	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶ℂ)
176	175, 161	fssresd 6539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
177		eldifi 4102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
178	177	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
179	178	fvresd 6684	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥))
180		difun2 4428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
181		difss 4107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∖ {𝑐}) ⊆ 𝑘
182	180, 181	eqsstri 4000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
183	182	sseli 3962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ 𝑘)
184		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))
185	87	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑘 ⊆ 𝐴)
186	163, 185	feqresmpt 6728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ 𝑘) = (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥)))
187	186	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ 𝑘)) = (ℂfld Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))))
188	111	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑘 ∈ Fin)
189	185	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
190	163	ffvelrnda 6845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞))
191	189, 190	syldan 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ (0[,)+∞))
192	173, 191	sseldi 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℂ)
193	188, 192	gsumfsum 20606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))) = Σ𝑥 ∈ 𝑘 (𝑇‘𝑥))
194	184, 187, 193	3eqtrrd 2861	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
195		elrege0 12836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑇‘𝑥) ∈ (0[,)+∞) ↔ ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
196	191, 195	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
197	196	simpld 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℝ)
198	196	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 0 ≤ (𝑇‘𝑥))
199	188, 197, 198	fsum00 15147	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0))
200	194, 199	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
201	200	r19.21bi 3208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) = 0)
202	183, 201	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇‘𝑥) = 0)
203	179, 202	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
204	176, 203	suppss 7854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
205		mul02 10812	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
206	205	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
207	89	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℝ)
208	207, 157	sstrdi 3978	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℂ)
209	167, 208	fssd 6522	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶ℂ)
210	209, 161	fssresd 6539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
211	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 ∈ V)
212	204, 206, 176, 210, 144, 211	suppssof1 7857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
213	172, 212	eqsstrd 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
214	140, 16, 142, 144, 148, 162, 213	gsumpt 19076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
215	148	fvresd 6684	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘f · 𝑋)‘𝑐))
216	163	ffnd 6509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇 Fn 𝐴)
217	167	ffnd 6509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋 Fn 𝐴)
218	161, 148	sseldd 3967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ 𝐴)
219		fnfvof 7417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑇 Fn 𝐴 ∧ 𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘f · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
220	216, 217, 164, 218, 219	syl22anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
221	214, 215, 220	3eqtrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
222	140, 16, 142, 144, 148, 176, 204	gsumpt 19076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
223	148	fvresd 6684	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐))
224	222, 223	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇‘𝑐))
225	221, 224	oveq12d 7168	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)))
226	209, 218	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ ℂ)
227	175, 218	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ∈ ℂ)
228		simplrr 776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
229	228, 224	breqtrd 5084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (𝑇‘𝑐))
230	229	gt0ne0d 11198	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ≠ 0)
231	226, 227, 230	divcan3d 11415	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)) = (𝑋‘𝑐))
232	225, 231	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋‘𝑐))
233	167, 218	ffvelrnd 6846	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ 𝐷)
234	232, 233	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
235	91	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐹:𝐷⟶ℝ)
236	235, 233	ffvelrnd 6846	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℝ)
237	236	leidd 11200	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ≤ (𝐹‘(𝑋‘𝑐)))
238	232	fveq2d 6668	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋‘𝑐)))
239		fco 6525	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
240	91, 98, 239	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
241	150, 153, 240, 10, 10, 155	off 7418	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℝ)
242		fss 6521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
243	241, 157, 242	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
244	243	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
245	244, 161	fssresd 6539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
246	240	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
247		fex 6983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹 ∘ 𝑋) ∈ V)
248	246, 164, 247	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) ∈ V)
249		offres 7678	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ (𝐹 ∘ 𝑋) ∈ V) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
250	166, 248, 249	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
251	250	oveq1d 7165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
252		fss 6521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
253	246, 157, 252	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
254	253, 161	fssresd 6539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
255	204, 206, 176, 254, 144, 211	suppssof1 7857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
256	251, 255	eqsstrd 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
257	140, 16, 142, 144, 148, 245, 256	gsumpt 19076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
258	148	fvresd 6684	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐))
259	91	ffnd 6509	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn 𝐷)
260		fnfco 6537	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 Fn 𝐷 ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋) Fn 𝐴)
261	259, 98, 260	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∘ 𝑋) Fn 𝐴)
262	261	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) Fn 𝐴)
263		fnfvof 7417	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑇 Fn 𝐴 ∧ (𝐹 ∘ 𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
264	216, 262, 164, 218, 263	syl22anc 836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
265		fvco3 6754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝑐 ∈ 𝐴) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
266	167, 218, 265	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
267	266	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
268	264, 267	eqtrd 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
269	257, 258, 268	3eqtrd 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
270	269, 224	oveq12d 7168	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)))
271	236	recnd 10663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℂ)
272	271, 227, 230	divcan3d 11415	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)) = (𝐹‘(𝑋‘𝑐)))
273	270, 272	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋‘𝑐)))
274	237, 238, 273	3brtr4d 5090	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
275	135, 234, 274	elrabd 3681	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
276	275	a1d 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((0 < (ℂfld Σg (𝑇 ↾ 𝑘)) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
277	120	simprbi 499	. . . . . . . . . . . . . . . 16 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)))
278	119, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)))
279		leloe 10721	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))))
280	80, 122, 279	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))))
281	278, 280	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))))
282	139, 276, 281	mpjaodan 955	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((0 < (ℂfld Σg (𝑇 ↾ 𝑘)) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
283	87, 282	embantd 59	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((𝑘 ⊆ 𝐴 → (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
284	85, 283	syl5bi 244	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
285	284	ex 415	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
286	285	com23 86	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
287	286	expcom 416	. . . . . . . 8 ⊢ (¬ 𝑐 ∈ 𝑘 → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
288	287	adantl 484	. . . . . . 7 ⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
289	288	a2d 29	. . . . . 6 ⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → ((𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
290	31, 47, 63, 79, 84, 289	findcard2s 8753	. . . . 5 ⊢ (𝐴 ∈ Fin → (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))})))
291	10, 290	mpcom 38	. . . 4 ⊢ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))}))
292	9, 291	mpd 15	. . 3 ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))})
293	156	ffnd 6509	. . . . . 6 ⊢ (𝜑 → (𝑇 ∘f · 𝑋) Fn 𝐴)
294		fnresdm 6460	. . . . . 6 ⊢ ((𝑇 ∘f · 𝑋) Fn 𝐴 → ((𝑇 ∘f · 𝑋) ↾ 𝐴) = (𝑇 ∘f · 𝑋))
295	293, 294	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐴) = (𝑇 ∘f · 𝑋))
296	295	oveq2d 7166	. . . 4 ⊢ (𝜑 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇 ∘f · 𝑋)))
297	296, 6	oveq12d 7168	. . 3 ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)))
298	3, 261, 10, 10, 155	offn 7414	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)) Fn 𝐴)
299		fnresdm 6460	. . . . . . . 8 ⊢ ((𝑇 ∘f · (𝐹 ∘ 𝑋)) Fn 𝐴 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘f · (𝐹 ∘ 𝑋)))
300	298, 299	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘f · (𝐹 ∘ 𝑋)))
301	300	oveq2d 7166	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))))
302	301, 6	oveq12d 7168	. . . . 5 ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) = ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)))
303	302	breq2d 5070	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
304	303	rabbidv 3480	. . 3 ⊢ (𝜑 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))})
305	292, 297, 304	3eltr3d 2927	. 2 ⊢ (𝜑 → ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))})
306		fveq2 6664	. . . 4 ⊢ (𝑤 = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))))
307	306	breq1d 5068	. . 3 ⊢ (𝑤 = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
308	307	elrab 3679	. 2 ⊢ (((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))} ↔ (((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
309	305, 308	sylib 220	1 ⊢ (𝜑 → (((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  {crab 3142  Vcvv 3494   ∖ cdif 3932   ∪ cun 3933   ⊆ wss 3935  ∅c0 4290  {csn 4560   class class class wbr 5058   ↦ cmpt 5138   ↾ cres 5551   ∘ ccom 5553   Fn wfn 6344  ⟶wf 6345  ‘cfv 6349  (class class class)co 7150   ∘_f cof 7401   supp csupp 7824  Fincfn 8503  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  +∞cpnf 10666   < clt 10669   ≤ cle 10670   − cmin 10864   / cdiv 11291  [,)cico 12734  [,]cicc 12735  Σcsu 15036   Σ_g cgsu 16708  Mndcmnd 17905  SubMndcsubmnd 17949  CMndccmn 18900  Ringcrg 19291  ℂ_fldccnfld 20539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-inf2 9098  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609  ax-addf 10610  ax-mulf 10611

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-int 4869  df-iun 4913  df-iin 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7403  df-om 7575  df-1st 7683  df-2nd 7684  df-supp 7825  df-tpos 7886  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-fsupp 8828  df-sup 8900  df-oi 8968  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699  df-8 11700  df-9 11701  df-n0 11892  df-z 11976  df-dec 12093  df-uz 12238  df-rp 12384  df-ico 12738  df-icc 12739  df-fz 12887  df-fzo 13028  df-seq 13364  df-exp 13424  df-hash 13685  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-sum 15037  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-0g 16709  df-gsum 16710  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-grp 18100  df-minusg 18101  df-mulg 18219  df-subg 18270  df-cntz 18441  df-cmn 18902  df-abl 18903  df-mgp 19234  df-ur 19246  df-ring 19293  df-cring 19294  df-oppr 19367  df-dvdsr 19385  df-unit 19386  df-invr 19416  df-dvr 19427  df-drng 19498  df-subrg 19527  df-cnfld 20540  df-refld 20743

This theorem is referenced by:  amgmlem  25561  amgmwlem  44897