Theorem jensen 25574

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 6488	. . . . . . . 8 ⊢ (𝜑 → 𝑇 Fn 𝐴)
4		fnresdm 6438	. . . . . . . 8 ⊢ (𝑇 Fn 𝐴 → (𝑇 ↾ 𝐴) = 𝑇)
5	3, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑇 ↾ 𝐴) = 𝑇)
6	5	oveq2d 7151	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑇 ↾ 𝐴)) = (ℂfld Σg 𝑇))
7	1, 6	breqtrrd 5058	. . . . 5 ⊢ (𝜑 → 0 < (ℂfld Σg (𝑇 ↾ 𝐴)))
8		ssid 3937	. . . . 5 ⊢ 𝐴 ⊆ 𝐴
9	7, 8	jctil 523	. . . 4 ⊢ (𝜑 → (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))))
10		jensen.4	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ Fin)
11		sseq1 3940	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴))
12		reseq2 5813	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = (𝑇 ↾ ∅))
13		res0 5822	. . . . . . . . . . . . 13 ⊢ (𝑇 ↾ ∅) = ∅
14	12, 13	eqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = ∅)
15	14	oveq2d 7151	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg ∅))
16		cnfld0 20115	. . . . . . . . . . . 12 ⊢ 0 = (0g‘ℂfld)
17	16	gsum0 17886	. . . . . . . . . . 11 ⊢ (ℂfld Σg ∅) = 0
18	15, 17	eqtrdi 2849	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂfld Σg (𝑇 ↾ 𝑎)) = 0)
19	18	breq2d 5042	. . . . . . . . 9 ⊢ (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < 0))
20	11, 19	anbi12d 633	. . . . . . . 8 ⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ ∅))
22	21	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)))
23	22, 18	oveq12d 7153	. . . . . . . . 9 ⊢ (𝑎 = ∅ → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0))
24		reseq2 5813	. . . . . . . . . . . . 13 ⊢ (𝑎 = ∅ → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅))
25	24	oveq2d 7151	. . . . . . . . . . . 12 ⊢ (𝑎 = ∅ → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)))
26	25, 18	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑎 = ∅ → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0))
27	26	breq2d 5042	. . . . . . . . . 10 ⊢ (𝑎 = ∅ → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)))
28	27	rabbidv 3427	. . . . . . . . 9 ⊢ (𝑎 = ∅ → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
29	23, 28	eleq12d 2884	. . . . . . . 8 ⊢ (𝑎 = ∅ → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}))
30	20, 29	imbi12d 348	. . . . . . 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 344	. . . . . 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 3940	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (𝑎 ⊆ 𝐴 ↔ 𝑘 ⊆ 𝐴))
33		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝑘))
34	33	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ 𝑘)))
35	34	breq2d 5042	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))))
36	32, 35	anbi12d 633	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))))
37		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ 𝑘))
38	37	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)))
39	38, 34	oveq12d 7153	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))))
40		reseq2 5813	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑘 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘))
41	40	oveq2d 7151	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑘 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)))
42	41, 34	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))))
43	42	breq2d 5042	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
44	43	rabbidv 3427	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})
45	39, 44	eleq12d 2884	. . . . . . . 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 348	. . . . . . 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 344	. . . . . 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 3940	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎 ⊆ 𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇 ↾ 𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
50	49	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
51	50	breq2d 5042	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
52	48, 51	anbi12d 633	. . . . . . . 8 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})))
54	53	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
55	54, 50	oveq12d 7153	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56		reseq2 5813	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})))
57	56	oveq2d 7151	. . . . . . . . . . . 12 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))))
58	57, 50	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
59	58	breq2d 5042	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
60	59	rabbidv 3427	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
61	55, 60	eleq12d 2884	. . . . . . . 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 348	. . . . . . 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 344	. . . . . 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 3940	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴))
65		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝐴))
66	65	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld Σg (𝑇 ↾ 𝐴)))
67	66	breq2d 5042	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ 𝐴))))
68	64, 67	anbi12d 633	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝐴)))))
69		reseq2 5813	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘f · 𝑋) ↾ 𝑎) = ((𝑇 ∘f · 𝑋) ↾ 𝐴))
70	69	oveq2d 7151	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)))
71	70, 66	oveq12d 7153	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))))
72		reseq2 5813	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐴 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴))
73	72	oveq2d 7151	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)))
74	73, 66	oveq12d 7153	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) = ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))))
75	74	breq2d 5042	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))))
76	75	rabbidv 3427	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))})
77	71, 76	eleq12d 2884	. . . . . . . 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 348	. . . . . . 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 344	. . . . . 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 10632	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
81	80	ltnri 10738	. . . . . . . . 9 ⊢ ¬ 0 < 0
82	81	pm2.21i 119	. . . . . . . 8 ⊢ (0 < 0 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)})
83	82	adantl 485	. . . . . . 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 454	. . . . . . . . . . . 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 770	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
87	86	unssad 4114	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ⊆ 𝐴)
88		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))
89		jensen.1	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
90	89	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝐷 ⊆ ℝ)
91		jensen.2	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)
92	91	ad3antrrr 729	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 𝐹:𝐷⟶ℝ)
93		simplll 774	. . . . . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))
103		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → ¬ 𝑐 ∈ 𝑘)
104	86	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
105		eqid 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld Σg (𝑇 ↾ 𝑘)) = (ℂfld Σg (𝑇 ↾ 𝑘))
106		eqid 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))
107		cnring 20113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℂfld ∈ Ring
108		ringcmn 19327	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109	107, 108	mp1i 13	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
110	10	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111	110, 87	ssfid 8725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
112		rege0subm 20147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0[,)+∞) ∈ (SubMnd‘ℂfld)
113	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
114	2	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
115	114, 87	fssresd 6519	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘):𝑘⟶(0[,)+∞))
116		c0ex 10624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
117	116	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
118	115, 111, 117	fdmfifsupp 8827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘) finSupp 0)
119	16, 109, 111, 113, 115, 118	gsumsubmcl 19032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞))
120		elrege0 12832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) ↔ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ ∧ 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘))))
121	120	simplbi 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
122	119, 121	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
123	122	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ)
124		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → 0 < (ℂfld Σg (𝑇 ↾ 𝑘)))
125	123, 124	elrpd 12416	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))})) → (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ+)
126		simprr 772	. . . . . . . . . . . . . . . . . . . 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 6645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
128	127	breq1d 5040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇 ↾ 𝑘)))))
129	128	elrab 3628	. . . . . . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . . . . . 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 498	. . . . . . . . . . . . . . . . . 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 499	. . . . . . . . . . . . . . . . . 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 25573	. . . . . . . . . . . . . . . . 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 6645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135	134	breq1d 5040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136	135	elrab 3628	. . . . . . . . . . . . . . . . 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 237	. . . . . . . . . . . . . . . 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 460	. . . . . . . . . . . . . . 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 20095	. . . . . . . . . . . . . . . . . . . . 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 8725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
144	143	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
145		ssun2 4100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐} ⊆ (𝑘 ∪ {𝑐})
146		vsnid 4562	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑐 ∈ {𝑐}
147	145, 146	sselii 3912	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑐 ∈ (𝑘 ∪ {𝑐})
148	147	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
149		remulcl 10611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
150	149	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
151		rge0ssre 12834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℝ
152		fss 6501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
153	2, 151, 152	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑇:𝐴⟶ℝ)
154	98, 89	fssd 6502	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋:𝐴⟶ℝ)
155		inidm 4145	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝐴) = 𝐴
156	150, 153, 154, 10, 10, 155	off 7404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘f · 𝑋):𝐴⟶ℝ)
157		ax-resscn 10583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ℝ ⊆ ℂ
158		fss 6501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘f · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
159	156, 157, 158	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
160	159	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘f · 𝑋):𝐴⟶ℂ)
161	86	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
162	160, 161	fssresd 6519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
163	2	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
164	110	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐴 ∈ Fin)
165		fex 6966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V)
166	163, 164, 165	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇 ∈ V)
167	98	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶𝐷)
168		fex 6966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝐴 ∈ Fin) → 𝑋 ∈ V)
169	167, 164, 168	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋 ∈ V)
170		offres 7666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
171	166, 169, 170	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
172	171	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
173	151, 157	sstri 3924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0[,)+∞) ⊆ ℂ
174		fss 6501	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
175	163, 173, 174	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶ℂ)
176	175, 161	fssresd 6519	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
177		eldifi 4054	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
178	177	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
179	178	fvresd 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥))
180		difun2 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
181		difss 4059	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 ∖ {𝑐}) ⊆ 𝑘
182	180, 181	eqsstri 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
183	182	sseli 3911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ 𝑘)
184		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))
185	87	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑘 ⊆ 𝐴)
186	163, 185	feqresmpt 6709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ 𝑘) = (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥)))
187	186	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ 𝑘)) = (ℂfld Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))))
188	111	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑘 ∈ Fin)
189	185	sselda 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴)
190	163	ffvelrnda 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞))
191	189, 190	syldan 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ (0[,)+∞))
192	173, 191	sseldi 3913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℂ)
193	188, 192	gsumfsum 20158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))) = Σ𝑥 ∈ 𝑘 (𝑇‘𝑥))
194	184, 187, 193	3eqtrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
195		elrege0 12832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑇‘𝑥) ∈ (0[,)+∞) ↔ ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
196	191, 195	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥)))
197	196	simpld 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℝ)
198	196	simprd 499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 0 ≤ (𝑇‘𝑥))
199	188, 197, 198	fsum00 15145	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0))
200	194, 199	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)
201	200	r19.21bi 3173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) = 0)
202	183, 201	sylan2 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇‘𝑥) = 0)
203	179, 202	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
204	176, 203	suppss 7843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
205		mul02 10807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
206	205	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
207	89	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℝ)
208	207, 157	sstrdi 3927	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℂ)
209	167, 208	fssd 6502	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶ℂ)
210	209, 161	fssresd 6519	. . . . . . . . . . . . . . . . . . . . . . 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 7846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
213	172, 212	eqsstrd 3953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
214	140, 16, 142, 144, 148, 162, 213	gsumpt 19075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
215	148	fvresd 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘f · 𝑋)‘𝑐))
216	163	ffnd 6488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑇 Fn 𝐴)
217	167	ffnd 6488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑋 Fn 𝐴)
218	161, 148	sseldd 3916	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ 𝐴)
219		fnfvof 7403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑇 Fn 𝐴 ∧ 𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘f · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
220	216, 217, 164, 218, 219	syl22anc 837	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
221	214, 215, 220	3eqtrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝑋‘𝑐)))
222	140, 16, 142, 144, 148, 176, 204	gsumpt 19075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
223	148	fvresd 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐))
224	222, 223	eqtrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇‘𝑐))
225	221, 224	oveq12d 7153	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)))
226	209, 218	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ ℂ)
227	175, 218	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ∈ ℂ)
228		simplrr 777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
229	228, 224	breqtrd 5056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 0 < (𝑇‘𝑐))
230	229	gt0ne0d 11193	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ≠ 0)
231	226, 227, 230	divcan3d 11410	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)) = (𝑋‘𝑐))
232	225, 231	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋‘𝑐))
233	167, 218	ffvelrnd 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ 𝐷)
234	232, 233	eqeltrd 2890	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
235	91	ad3antrrr 729	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → 𝐹:𝐷⟶ℝ)
236	235, 233	ffvelrnd 6829	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℝ)
237	236	leidd 11195	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ≤ (𝐹‘(𝑋‘𝑐)))
238	232	fveq2d 6649	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋‘𝑐)))
239		fco 6505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
240	91, 98, 239	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
241	150, 153, 240, 10, 10, 155	off 7404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℝ)
242		fss 6501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
243	241, 157, 242	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
244	243	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘f · (𝐹 ∘ 𝑋)):𝐴⟶ℂ)
245	244, 161	fssresd 6519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
246	240	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℝ)
247		fex 6966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹 ∘ 𝑋) ∈ V)
248	246, 164, 247	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) ∈ V)
249		offres 7666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 ∈ V ∧ (𝐹 ∘ 𝑋) ∈ V) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
250	166, 248, 249	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))))
251	250	oveq1d 7150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
252		fss 6501	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
253	246, 157, 252	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℂ)
254	253, 161	fssresd 6519	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
255	204, 206, 176, 254, 144, 211	suppssof1 7846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
256	251, 255	eqsstrd 3953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
257	140, 16, 142, 144, 148, 245, 256	gsumpt 19075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
258	148	fvresd 6665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐))
259	91	ffnd 6488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹 Fn 𝐷)
260		fnfco 6517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹 Fn 𝐷 ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋) Fn 𝐴)
261	259, 98, 260	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐹 ∘ 𝑋) Fn 𝐴)
262	261	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) Fn 𝐴)
263		fnfvof 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑇 Fn 𝐴 ∧ (𝐹 ∘ 𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
264	216, 262, 164, 218, 263	syl22anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)))
265		fvco3 6737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝑐 ∈ 𝐴) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
266	167, 218, 265	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐)))
267	266	oveq2d 7151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
268	264, 267	eqtrd 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘f · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
269	257, 258, 268	3eqtrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))))
270	269, 224	oveq12d 7153	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)))
271	236	recnd 10658	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℂ)
272	271, 227, 230	divcan3d 11410	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)) = (𝐹‘(𝑋‘𝑐)))
273	270, 272	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋‘𝑐)))
274	237, 238, 273	3brtr4d 5062	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
275	135, 234, 274	elrabd 3630	. . . . . . . . . . . . . . 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 500	. . . . . . . . . . . . . . . 16 ⊢ ((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)))
278	119, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)))
279		leloe 10716	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))))
280	80, 122, 279	sylancr 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘)))))
281	278, 280	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld Σg (𝑇 ↾ 𝑘))))
282	139, 276, 281	mpjaodan 956	. . . . . . . . . . . . 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 245	. . . . . . . . . . 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 416	. . . . . . . . . 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 417	. . . . . . . 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 485	. . . . . . 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 8743	. . . . 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 6488	. . . . . 6 ⊢ (𝜑 → (𝑇 ∘f · 𝑋) Fn 𝐴)
294		fnresdm 6438	. . . . . 6 ⊢ ((𝑇 ∘f · 𝑋) Fn 𝐴 → ((𝑇 ∘f · 𝑋) ↾ 𝐴) = (𝑇 ∘f · 𝑋))
295	293, 294	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑇 ∘f · 𝑋) ↾ 𝐴) = (𝑇 ∘f · 𝑋))
296	295	oveq2d 7151	. . . 4 ⊢ (𝜑 → (ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇 ∘f · 𝑋)))
297	296, 6	oveq12d 7153	. . 3 ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)))
298	3, 261, 10, 10, 155	offn 7400	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∘f · (𝐹 ∘ 𝑋)) Fn 𝐴)
299		fnresdm 6438	. . . . . . . 8 ⊢ ((𝑇 ∘f · (𝐹 ∘ 𝑋)) Fn 𝐴 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘f · (𝐹 ∘ 𝑋)))
300	298, 299	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘f · (𝐹 ∘ 𝑋)))
301	300	oveq2d 7151	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))))
302	301, 6	oveq12d 7153	. . . . 5 ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) = ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)))
303	302	breq2d 5042	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴))) ↔ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
304	303	rabbidv 3427	. . 3 ⊢ (𝜑 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇 ↾ 𝐴)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))})
305	292, 297, 304	3eltr3d 2904	. 2 ⊢ (𝜑 → ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))})
306		fveq2 6645	. . . 4 ⊢ (𝑤 = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) → (𝐹‘𝑤) = (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))))
307	306	breq1d 5040	. . 3 ⊢ (𝑤 = ((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹‘𝑤) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
308	307	elrab 3628	. 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 221	1 ⊢ (𝜑 → (((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  {csn 4525   class class class wbr 5030   ↦ cmpt 5110   ↾ cres 5521   ∘ ccom 5523   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135   ∘_f cof 7387   supp csupp 7813  Fincfn 8492  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661   < clt 10664   ≤ cle 10665   − cmin 10859   / cdiv 11286  [,)cico 12728  [,]cicc 12729  Σcsu 15034   Σ_g cgsu 16706  Mndcmnd 17903  SubMndcsubmnd 17947  CMndccmn 18898  Ringcrg 19290  ℂ_fldccnfld 20091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-tpos 7875  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-sup 8890  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-0g 16707  df-gsum 16708  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-grp 18098  df-minusg 18099  df-mulg 18217  df-subg 18268  df-cntz 18439  df-cmn 18900  df-abl 18901  df-mgp 19233  df-ur 19245  df-ring 19292  df-cring 19293  df-oppr 19369  df-dvdsr 19387  df-unit 19388  df-invr 19418  df-dvr 19429  df-drng 19497  df-subrg 19526  df-cnfld 20092  df-refld 20294

This theorem is referenced by:  amgmlem  25575  amgmwlem  45330