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

Theorem jensen 25494
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.
StepHypRef Expression
1 jensen.7 . . . . . 6 (𝜑 → 0 < (ℂfld Σg 𝑇))
2 jensen.5 . . . . . . . . 9 (𝜑𝑇:𝐴⟶(0[,)+∞))
32ffnd 6509 . . . . . . . 8 (𝜑𝑇 Fn 𝐴)
4 fnresdm 6460 . . . . . . . 8 (𝑇 Fn 𝐴 → (𝑇𝐴) = 𝑇)
53, 4syl 17 . . . . . . 7 (𝜑 → (𝑇𝐴) = 𝑇)
65oveq2d 7161 . . . . . 6 (𝜑 → (ℂfld Σg (𝑇𝐴)) = (ℂfld Σg 𝑇))
71, 6breqtrrd 5086 . . . . 5 (𝜑 → 0 < (ℂfld Σg (𝑇𝐴)))
8 ssid 3988 . . . . 5 𝐴𝐴
97, 8jctil 520 . . . 4 (𝜑 → (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))))
10 jensen.4 . . . . 5 (𝜑𝐴 ∈ Fin)
11 sseq1 3991 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
12 reseq2 5842 . . . . . . . . . . . . 13 (𝑎 = ∅ → (𝑇𝑎) = (𝑇 ↾ ∅))
13 res0 5851 . . . . . . . . . . . . 13 (𝑇 ↾ ∅) = ∅
1412, 13syl6eq 2872 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑇𝑎) = ∅)
1514oveq2d 7161 . . . . . . . . . . 11 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg ∅))
16 cnfld0 20499 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
1716gsum0 17884 . . . . . . . . . . 11 (ℂfld Σg ∅) = 0
1815, 17syl6eq 2872 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = 0)
1918breq2d 5070 . . . . . . . . 9 (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < 0))
2011, 19anbi12d 630 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21 reseq2 5842 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ ∅))
2221oveq2d 7161 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)))
2322, 18oveq12d 7163 . . . . . . . . 9 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0))
24 reseq2 5842 . . . . . . . . . . . . 13 (𝑎 = ∅ → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ ∅))
2524oveq2d 7161 . . . . . . . . . . . 12 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)))
2625, 18oveq12d 7163 . . . . . . . . . . 11 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0))
2726breq2d 5070 . . . . . . . . . 10 (𝑎 = ∅ → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)))
2827rabbidv 3481 . . . . . . . . 9 (𝑎 = ∅ → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
2923, 28eleq12d 2907 . . . . . . . 8 (𝑎 = ∅ → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)}))
3020, 29imbi12d 346 . . . . . . 7 (𝑎 = ∅ → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})))
3130imbi2d 342 . . . . . 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 (𝑎 = 𝑘 → (𝑇𝑎) = (𝑇𝑘))
3433oveq2d 7161 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝑘)))
3534breq2d 5070 . . . . . . . . 9 (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝑘))))
3632, 35anbi12d 630 . . . . . . . 8 (𝑎 = 𝑘 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘)))))
37 reseq2 5842 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝑘))
3837oveq2d 7161 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)))
3938, 34oveq12d 7163 . . . . . . . . 9 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
40 reseq2 5842 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝑘))
4140oveq2d 7161 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)))
4241, 34oveq12d 7163 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
4342breq2d 5070 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
4443rabbidv 3481 . . . . . . . . 9 (𝑎 = 𝑘 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})
4539, 44eleq12d 2907 . . . . . . . 8 (𝑎 = 𝑘 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))
4636, 45imbi12d 346 . . . . . . 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 (𝑇𝑘)))})))
4746imbi2d 342 . . . . . 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 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
5049oveq2d 7161 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
5150breq2d 5070 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5248, 51anbi12d 630 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53 reseq2 5842 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})))
5453oveq2d 7161 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
5554, 50oveq12d 7163 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56 reseq2 5842 . . . . . . . . . . . . 13 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})))
5756oveq2d 7161 . . . . . . . . . . . 12 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))))
5857, 50oveq12d 7163 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5958breq2d 5070 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
6059rabbidv 3481 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
6155, 60eleq12d 2907 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
6252, 61imbi12d 346 . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
6362imbi2d 342 . . . . . 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 (𝑎 = 𝐴 → (𝑇𝑎) = (𝑇𝐴))
6665oveq2d 7161 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝐴)))
6766breq2d 5070 . . . . . . . . 9 (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝐴))))
6864, 67anbi12d 630 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴)))))
69 reseq2 5842 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝐴))
7069oveq2d 7161 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)))
7170, 66oveq12d 7163 . . . . . . . . 9 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
72 reseq2 5842 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝐴))
7372oveq2d 7161 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)))
7473, 66oveq12d 7163 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
7574breq2d 5070 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))))
7675rabbidv 3481 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
7771, 76eleq12d 2907 . . . . . . . 8 (𝑎 = 𝐴 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
7868, 77imbi12d 346 . . . . . . 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 (𝑇𝐴)))})))
7978imbi2d 342 . . . . . 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 ∈ ℝ
8180ltnri 10738 . . . . . . . . 9 ¬ 0 < 0
8281pm2.21i 119 . . . . . . . 8 (0 < 0 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
8382adantl 482 . . . . . . 7 ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
8483a1i 11 . . . . . 6 (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)}))
85 impexp 451 . . . . . . . . . . . 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 767 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
8786unssad 4162 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘𝐴)
88 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇𝑘)))
89 jensen.1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ⊆ ℝ)
9089ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐷 ⊆ ℝ)
91 jensen.2 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐷⟶ℝ)
9291ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐹:𝐷⟶ℝ)
93 simplll 771 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝜑)
94 jensen.3 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
9593, 94sylan 580 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
9693, 10syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐴 ∈ Fin)
9793, 2syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝑇:𝐴⟶(0[,)+∞))
98 jensen.6 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋:𝐴𝐷)
9993, 98syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝑋:𝐴𝐷)
1001ad3antrrr 726 . . . . . . . . . . . . . . . . . 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 − 𝑡) · (𝐹𝑦))))
10293, 101sylan 580 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) ∧ (𝑥𝐷𝑦𝐷𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
103 simpllr 772 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ¬ 𝑐𝑘)
10486adantr 481 . . . . . . . . . . . . . . . . . 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 20497 . . . . . . . . . . . . . . . . . . . . . . 23 fld ∈ Ring
108 ringcmn 19262 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109107, 108mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
11010ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111110, 87ssfid 8730 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
112 rege0subm 20531 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,)+∞) ∈ (SubMnd‘ℂfld)
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
1142ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
115114, 87fssresd 6539 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘):𝑘⟶(0[,)+∞))
116 c0ex 10624 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
118115, 111, 117fdmfifsupp 8832 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘) finSupp 0)
11916, 109, 111, 113, 115, 118gsumsubmcl 18970 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞))
120 elrege0 12832 . . . . . . . . . . . . . . . . . . . . . 22 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) ↔ ((ℂfld Σg (𝑇𝑘)) ∈ ℝ ∧ 0 ≤ (ℂfld Σg (𝑇𝑘))))
121120simplbi 498 . . . . . . . . . . . . . . . . . . . . 21 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
122119, 121syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
123122adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
124 simprl 767 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 0 < (ℂfld Σg (𝑇𝑘)))
125123, 124elrpd 12418 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ+)
126 simprr 769 . . . . . . . . . . . . . . . . . . . 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 (𝑇𝑘)))))
128127breq1d 5068 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
129128elrab 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 (𝑇𝑘)))))
130126, 129sylib 219 . . . . . . . . . . . . . . . . . . 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 (𝑇𝑘)))))
131130simpld 495 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ 𝐷)
132130simprd 496 . . . . . . . . . . . . . . . . . 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 (𝑇𝑘))))
13390, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 125, 131, 132jensenlem2 25493 . . . . . . . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135134breq1d 5068 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136135elrab 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
137133, 136sylibr 235 . . . . . . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
138137expr 457 . . . . . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
13988, 138embantd 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 20479 . . . . . . . . . . . . . . . . . . . . 21 ℂ = (Base‘ℂfld)
141 ringmnd 19237 . . . . . . . . . . . . . . . . . . . . . 22 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
142107, 141mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ℂfld ∈ Mnd)
143110, 86ssfid 8730 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
144143adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
145 ssun2 4148 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐} ⊆ (𝑘 ∪ {𝑐})
146 vsnid 4594 . . . . . . . . . . . . . . . . . . . . . . 23 𝑐 ∈ {𝑐}
147145, 146sselii 3963 . . . . . . . . . . . . . . . . . . . . . 22 𝑐 ∈ (𝑘 ∪ {𝑐})
148147a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
149 remulcl 10611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
150149adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
151 rge0ssre 12834 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
152 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
1532, 151, 152sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇:𝐴⟶ℝ)
15498, 89fssd 6522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋:𝐴⟶ℝ)
155 inidm 4194 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝐴) = 𝐴
156150, 153, 154, 10, 10, 155off 7413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℝ)
157 ax-resscn 10583 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ ⊆ ℂ
158 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · 𝑋):𝐴⟶ℂ)
159156, 157, 158sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℂ)
160159ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · 𝑋):𝐴⟶ℂ)
16186adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
162160, 161fssresd 6539 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
1632ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
164110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐴 ∈ Fin)
165 fex 6981 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V)
166163, 164, 165syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 ∈ V)
16798ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴𝐷)
168 fex 6981 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋:𝐴𝐷𝐴 ∈ Fin) → 𝑋 ∈ V)
169167, 164, 168syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 ∈ V)
170 offres 7675 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
171166, 169, 170syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
172171oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
173151, 157sstri 3975 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℂ
174 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
175163, 173, 174sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶ℂ)
176175, 161fssresd 6539 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
177 eldifi 4102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
178177adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
179178fvresd 6684 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇𝑥))
180 difun2 4427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
181 difss 4107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∖ {𝑐}) ⊆ 𝑘
182180, 181eqsstri 4000 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
183182sseli 3962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥𝑘)
184 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 = (ℂfld Σg (𝑇𝑘)))
18587adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘𝐴)
186163, 185feqresmpt 6728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑘) = (𝑥𝑘 ↦ (𝑇𝑥)))
187186oveq2d 7161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))))
188111adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘 ∈ Fin)
189185sselda 3966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 𝑥𝐴)
190163ffvelrnda 6844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝐴) → (𝑇𝑥) ∈ (0[,)+∞))
191189, 190syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ (0[,)+∞))
192173, 191sseldi 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℂ)
193188, 192gsumfsum 20542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))) = Σ𝑥𝑘 (𝑇𝑥))
194184, 187, 1933eqtrrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → Σ𝑥𝑘 (𝑇𝑥) = 0)
195 elrege0 12832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑇𝑥) ∈ (0[,)+∞) ↔ ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
196191, 195sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
197196simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℝ)
198196simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 0 ≤ (𝑇𝑥))
199188, 197, 198fsum00 15143 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (Σ𝑥𝑘 (𝑇𝑥) = 0 ↔ ∀𝑥𝑘 (𝑇𝑥) = 0))
200194, 199mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ∀𝑥𝑘 (𝑇𝑥) = 0)
201200r19.21bi 3208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) = 0)
202183, 201sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇𝑥) = 0)
203179, 202eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
204176, 203suppss 7851 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
205 mul02 10807 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
206205adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
20789ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℝ)
208207, 157sstrdi 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℂ)
209167, 208fssd 6522 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴⟶ℂ)
210209, 161fssresd 6539 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
211116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 ∈ V)
212204, 206, 176, 210, 144, 211suppssof1 7854 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
213172, 212eqsstrd 4004 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
214140, 16, 142, 144, 148, 162, 213gsumpt 19013 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
215148fvresd 6684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · 𝑋)‘𝑐))
216163ffnd 6509 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 Fn 𝐴)
217167ffnd 6509 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 Fn 𝐴)
218161, 148sseldd 3967 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐𝐴)
219 fnfvof 7412 . . . . . . . . . . . . . . . . . . . . 21 (((𝑇 Fn 𝐴𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
220216, 217, 164, 218, 219syl22anc 834 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
221214, 215, 2203eqtrd 2860 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝑋𝑐)))
222140, 16, 142, 144, 148, 176, 204gsumpt 19013 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
223148fvresd 6684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇𝑐))
224222, 223eqtrd 2856 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇𝑐))
225221, 224oveq12d 7163 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)))
226209, 218ffvelrnd 6845 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ ℂ)
227175, 218ffvelrnd 6845 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ∈ ℂ)
228 simplrr 774 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
229228, 224breqtrd 5084 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (𝑇𝑐))
230229gt0ne0d 11193 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ≠ 0)
231226, 227, 230divcan3d 11410 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)) = (𝑋𝑐))
232225, 231eqtrd 2856 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋𝑐))
233167, 218ffvelrnd 6845 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ 𝐷)
234232, 233eqeltrd 2913 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
23591ad3antrrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐹:𝐷⟶ℝ)
236235, 233ffvelrnd 6845 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℝ)
237236leidd 11195 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ≤ (𝐹‘(𝑋𝑐)))
238232fveq2d 6668 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋𝑐)))
239 fco 6525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴𝐷) → (𝐹𝑋):𝐴⟶ℝ)
24091, 98, 239syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑋):𝐴⟶ℝ)
241150, 153, 240, 10, 10, 155off 7413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℝ)
242 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · (𝐹𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
243241, 157, 242sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
244243ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
245244, 161fssresd 6539 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
246240ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℝ)
247 fex 6981 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹𝑋) ∈ V)
248246, 164, 247syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) ∈ V)
249 offres 7675 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ (𝐹𝑋) ∈ V) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
250166, 248, 249syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
251250oveq1d 7160 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
252 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹𝑋):𝐴⟶ℂ)
253246, 157, 252sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℂ)
254253, 161fssresd 6539 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
255204, 206, 176, 254, 144, 211suppssof1 7854 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
256251, 255eqsstrd 4004 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
257140, 16, 142, 144, 148, 245, 256gsumpt 19013 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
258148fvresd 6684 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · (𝐹𝑋))‘𝑐))
25991ffnd 6509 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn 𝐷)
260 fnfco 6537 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝐷𝑋:𝐴𝐷) → (𝐹𝑋) Fn 𝐴)
261259, 98, 260syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹𝑋) Fn 𝐴)
262261ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) Fn 𝐴)
263 fnfvof 7412 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑇 Fn 𝐴 ∧ (𝐹𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
264216, 262, 164, 218, 263syl22anc 834 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
265 fvco3 6754 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋:𝐴𝐷𝑐𝐴) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
266167, 218, 265syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
267266oveq2d 7161 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
268264, 267eqtrd 2856 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
269257, 258, 2683eqtrd 2860 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
270269, 224oveq12d 7163 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)))
271236recnd 10658 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℂ)
272271, 227, 230divcan3d 11410 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)) = (𝐹‘(𝑋𝑐)))
273270, 272eqtrd 2856 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋𝑐)))
274237, 238, 2733brtr4d 5090 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
275135, 234, 274elrabd 3681 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
276275a1d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
277120simprbi 497 . . . . . . . . . . . . . . . 16 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
278119, 277syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
279 leloe 10716 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
28080, 122, 279sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
281278, 280mpbid 233 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘))))
282139, 276, 281mpjaodan 952 . . . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
28387, 282embantd 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
28485, 283syl5bi 243 . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
285284ex 413 . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
286285com23 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
287286expcom 414 . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
288287adantl 482 . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
289288a2d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
29031, 47, 63, 79, 84, 289findcard2s 8748 . . . . 5 (𝐴 ∈ Fin → (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})))
29110, 290mpcom 38 . . . 4 (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
2929, 291mpd 15 . . 3 (𝜑 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
293156ffnd 6509 . . . . . 6 (𝜑 → (𝑇f · 𝑋) Fn 𝐴)
294 fnresdm 6460 . . . . . 6 ((𝑇f · 𝑋) Fn 𝐴 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
295293, 294syl 17 . . . . 5 (𝜑 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
296295oveq2d 7161 . . . 4 (𝜑 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇f · 𝑋)))
297296, 6oveq12d 7163 . . 3 (𝜑 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)))
2983, 261, 10, 10, 155offn 7409 . . . . . . . 8 (𝜑 → (𝑇f · (𝐹𝑋)) Fn 𝐴)
299 fnresdm 6460 . . . . . . . 8 ((𝑇f · (𝐹𝑋)) Fn 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
300298, 299syl 17 . . . . . . 7 (𝜑 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
301300oveq2d 7161 . . . . . 6 (𝜑 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇f · (𝐹𝑋))))
302301, 6oveq12d 7163 . . . . 5 (𝜑 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)))
303302breq2d 5070 . . . 4 (𝜑 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
304303rabbidv 3481 . . 3 (𝜑 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
305292, 297, 3043eltr3d 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 𝑇))))
307306breq1d 5068 . . 3 (𝑤 = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
308307elrab 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 𝑇))))
309305, 308sylib 219 1 (𝜑 → (((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wcel 2105  wral 3138  {crab 3142  Vcvv 3495  cdif 3932  cun 3933  wss 3935  c0 4290  {csn 4559   class class class wbr 5058  cmpt 5138  cres 5551  ccom 5553   Fn wfn 6344  wf 6345  cfv 6349  (class class class)co 7145  f cof 7396   supp csupp 7821  Fincfn 8498  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  [,)cico 12730  [,]cicc 12731  Σcsu 15032   Σg cgsu 16704  Mndcmnd 17901  SubMndcsubmnd 17945  CMndccmn 18837  Ringcrg 19228  fldccnfld 20475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-inf2 9093  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 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  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 3497  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 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-iin 4915  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 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-tpos 7883  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-sup 8895  df-oi 8963  df-card 9357  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 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-rp 12380  df-ico 12734  df-icc 12735  df-fz 12883  df-fzo 13024  df-seq 13360  df-exp 13420  df-hash 13681  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-clim 14835  df-sum 15033  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-mulr 16569  df-starv 16570  df-tset 16574  df-ple 16575  df-ds 16577  df-unif 16578  df-0g 16705  df-gsum 16706  df-mre 16847  df-mrc 16848  df-acs 16850  df-mgm 17842  df-sgrp 17891  df-mnd 17902  df-submnd 17947  df-grp 18046  df-minusg 18047  df-mulg 18165  df-subg 18216  df-cntz 18387  df-cmn 18839  df-abl 18840  df-mgp 19171  df-ur 19183  df-ring 19230  df-cring 19231  df-oppr 19304  df-dvdsr 19322  df-unit 19323  df-invr 19353  df-dvr 19364  df-drng 19435  df-subrg 19464  df-cnfld 20476  df-refld 20679
This theorem is referenced by:  amgmlem  25495  amgmwlem  44801
  Copyright terms: Public domain W3C validator