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

Theorem jensen 26138
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 6601 . . . . . . . 8 (𝜑𝑇 Fn 𝐴)
4 fnresdm 6551 . . . . . . . 8 (𝑇 Fn 𝐴 → (𝑇𝐴) = 𝑇)
53, 4syl 17 . . . . . . 7 (𝜑 → (𝑇𝐴) = 𝑇)
65oveq2d 7291 . . . . . 6 (𝜑 → (ℂfld Σg (𝑇𝐴)) = (ℂfld Σg 𝑇))
71, 6breqtrrd 5102 . . . . 5 (𝜑 → 0 < (ℂfld Σg (𝑇𝐴)))
8 ssid 3943 . . . . 5 𝐴𝐴
97, 8jctil 520 . . . 4 (𝜑 → (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))))
10 jensen.4 . . . . 5 (𝜑𝐴 ∈ Fin)
11 sseq1 3946 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
12 reseq2 5886 . . . . . . . . . . . . 13 (𝑎 = ∅ → (𝑇𝑎) = (𝑇 ↾ ∅))
13 res0 5895 . . . . . . . . . . . . 13 (𝑇 ↾ ∅) = ∅
1412, 13eqtrdi 2794 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑇𝑎) = ∅)
1514oveq2d 7291 . . . . . . . . . . 11 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg ∅))
16 cnfld0 20622 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
1716gsum0 18368 . . . . . . . . . . 11 (ℂfld Σg ∅) = 0
1815, 17eqtrdi 2794 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = 0)
1918breq2d 5086 . . . . . . . . 9 (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < 0))
2011, 19anbi12d 631 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21 reseq2 5886 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ ∅))
2221oveq2d 7291 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)))
2322, 18oveq12d 7293 . . . . . . . . 9 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0))
24 reseq2 5886 . . . . . . . . . . . . 13 (𝑎 = ∅ → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ ∅))
2524oveq2d 7291 . . . . . . . . . . . 12 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)))
2625, 18oveq12d 7293 . . . . . . . . . . 11 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0))
2726breq2d 5086 . . . . . . . . . 10 (𝑎 = ∅ → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)))
2827rabbidv 3414 . . . . . . . . 9 (𝑎 = ∅ → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
2923, 28eleq12d 2833 . . . . . . . 8 (𝑎 = ∅ → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)}))
3020, 29imbi12d 345 . . . . . . 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 341 . . . . . 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 3946 . . . . . . . . 9 (𝑎 = 𝑘 → (𝑎𝐴𝑘𝐴))
33 reseq2 5886 . . . . . . . . . . 11 (𝑎 = 𝑘 → (𝑇𝑎) = (𝑇𝑘))
3433oveq2d 7291 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝑘)))
3534breq2d 5086 . . . . . . . . 9 (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝑘))))
3632, 35anbi12d 631 . . . . . . . 8 (𝑎 = 𝑘 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘)))))
37 reseq2 5886 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝑘))
3837oveq2d 7291 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)))
3938, 34oveq12d 7293 . . . . . . . . 9 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
40 reseq2 5886 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝑘))
4140oveq2d 7291 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)))
4241, 34oveq12d 7293 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
4342breq2d 5086 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
4443rabbidv 3414 . . . . . . . . 9 (𝑎 = 𝑘 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})
4539, 44eleq12d 2833 . . . . . . . 8 (𝑎 = 𝑘 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))
4636, 45imbi12d 345 . . . . . . 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 341 . . . . . 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 3946 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49 reseq2 5886 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
5049oveq2d 7291 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
5150breq2d 5086 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5248, 51anbi12d 631 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53 reseq2 5886 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})))
5453oveq2d 7291 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
5554, 50oveq12d 7293 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56 reseq2 5886 . . . . . . . . . . . . 13 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})))
5756oveq2d 7291 . . . . . . . . . . . 12 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))))
5857, 50oveq12d 7293 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5958breq2d 5086 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
6059rabbidv 3414 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
6155, 60eleq12d 2833 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
6252, 61imbi12d 345 . . . . . . 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 341 . . . . . 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 3946 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
65 reseq2 5886 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑇𝑎) = (𝑇𝐴))
6665oveq2d 7291 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝐴)))
6766breq2d 5086 . . . . . . . . 9 (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝐴))))
6864, 67anbi12d 631 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴)))))
69 reseq2 5886 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝐴))
7069oveq2d 7291 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)))
7170, 66oveq12d 7293 . . . . . . . . 9 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
72 reseq2 5886 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝐴))
7372oveq2d 7291 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)))
7473, 66oveq12d 7293 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
7574breq2d 5086 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))))
7675rabbidv 3414 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
7771, 76eleq12d 2833 . . . . . . . 8 (𝑎 = 𝐴 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
7868, 77imbi12d 345 . . . . . . 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 341 . . . . . 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 10977 . . . . . . . . . 10 0 ∈ ℝ
8180ltnri 11084 . . . . . . . . 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 768 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
8786unssad 4121 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘𝐴)
88 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇𝑘)))
89 jensen.1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ⊆ ℝ)
9089ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐷 ⊆ ℝ)
91 jensen.2 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐷⟶ℝ)
9291ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐹:𝐷⟶ℝ)
93 simplll 772 . . . . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . . . . 18 (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑇𝑘))
106 eqid 2738 . . . . . . . . . . . . . . . . . 18 (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))
107 cnring 20620 . . . . . . . . . . . . . . . . . . . . . . 23 fld ∈ Ring
108 ringcmn 19820 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109107, 108mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
11010ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111110, 87ssfid 9042 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
112 rege0subm 20654 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,)+∞) ∈ (SubMnd‘ℂfld)
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
1142ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
115114, 87fssresd 6641 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘):𝑘⟶(0[,)+∞))
116 c0ex 10969 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
118115, 111, 117fdmfifsupp 9138 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘) finSupp 0)
11916, 109, 111, 113, 115, 118gsumsubmcl 19520 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞))
120 elrege0 13186 . . . . . . . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 0 < (ℂfld Σg (𝑇𝑘)))
125123, 124elrpd 12769 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ+)
126 simprr 770 . . . . . . . . . . . . . . . . . . . 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 6774 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
128127breq1d 5084 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
129128elrab 3624 . . . . . . . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . . . . . . . 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 26137 . . . . . . . . . . . . . . . . 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 6774 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135134breq1d 5084 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136135elrab 3624 . . . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . . . . 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 20601 . . . . . . . . . . . . . . . . . . . . 21 ℂ = (Base‘ℂfld)
141 ringmnd 19793 . . . . . . . . . . . . . . . . . . . . . 22 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
142107, 141mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ℂfld ∈ Mnd)
143110, 86ssfid 9042 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
144143adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
145 ssun2 4107 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐} ⊆ (𝑘 ∪ {𝑐})
146 vsnid 4598 . . . . . . . . . . . . . . . . . . . . . . 23 𝑐 ∈ {𝑐}
147145, 146sselii 3918 . . . . . . . . . . . . . . . . . . . . . 22 𝑐 ∈ (𝑘 ∪ {𝑐})
148147a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
149 remulcl 10956 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
150149adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
151 rge0ssre 13188 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
152 fss 6617 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
1532, 151, 152sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇:𝐴⟶ℝ)
15498, 89fssd 6618 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋:𝐴⟶ℝ)
155 inidm 4152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝐴) = 𝐴
156150, 153, 154, 10, 10, 155off 7551 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℝ)
157 ax-resscn 10928 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ ⊆ ℂ
158 fss 6617 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · 𝑋):𝐴⟶ℂ)
159156, 157, 158sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℂ)
160159ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · 𝑋):𝐴⟶ℂ)
16186adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
162160, 161fssresd 6641 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
1632ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
164110adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐴 ∈ Fin)
165163, 164fexd 7103 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 ∈ V)
16698ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴𝐷)
167166, 164fexd 7103 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 ∈ V)
168 offres 7826 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
169165, 167, 168syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
170169oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
171151, 157sstri 3930 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℂ
172 fss 6617 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
173163, 171, 172sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶ℂ)
174173, 161fssresd 6641 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
175 eldifi 4061 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
176175adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
177176fvresd 6794 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇𝑥))
178 difun2 4414 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
179 difss 4066 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∖ {𝑐}) ⊆ 𝑘
180178, 179eqsstri 3955 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
181180sseli 3917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥𝑘)
182 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 = (ℂfld Σg (𝑇𝑘)))
18387adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘𝐴)
184163, 183feqresmpt 6838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑘) = (𝑥𝑘 ↦ (𝑇𝑥)))
185184oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))))
186111adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘 ∈ Fin)
187183sselda 3921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 𝑥𝐴)
188163ffvelrnda 6961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝐴) → (𝑇𝑥) ∈ (0[,)+∞))
189187, 188syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ (0[,)+∞))
190171, 189sselid 3919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℂ)
191186, 190gsumfsum 20665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))) = Σ𝑥𝑘 (𝑇𝑥))
192182, 185, 1913eqtrrd 2783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → Σ𝑥𝑘 (𝑇𝑥) = 0)
193 elrege0 13186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑇𝑥) ∈ (0[,)+∞) ↔ ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
194189, 193sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
195194simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℝ)
196194simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 0 ≤ (𝑇𝑥))
197186, 195, 196fsum00 15510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (Σ𝑥𝑘 (𝑇𝑥) = 0 ↔ ∀𝑥𝑘 (𝑇𝑥) = 0))
198192, 197mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ∀𝑥𝑘 (𝑇𝑥) = 0)
199198r19.21bi 3134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) = 0)
200181, 199sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇𝑥) = 0)
201177, 200eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
202174, 201suppss 8010 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
203 mul02 11153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
204203adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
20589ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℝ)
206205, 157sstrdi 3933 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℂ)
207166, 206fssd 6618 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴⟶ℂ)
208207, 161fssresd 6641 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
209116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 ∈ V)
210202, 204, 174, 208, 144, 209suppssof1 8015 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
211170, 210eqsstrd 3959 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
212140, 16, 142, 144, 148, 162, 211gsumpt 19563 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
213148fvresd 6794 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · 𝑋)‘𝑐))
214163ffnd 6601 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 Fn 𝐴)
215166ffnd 6601 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 Fn 𝐴)
216161, 148sseldd 3922 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐𝐴)
217 fnfvof 7550 . . . . . . . . . . . . . . . . . . . . 21 (((𝑇 Fn 𝐴𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
218214, 215, 164, 216, 217syl22anc 836 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
219212, 213, 2183eqtrd 2782 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝑋𝑐)))
220140, 16, 142, 144, 148, 174, 202gsumpt 19563 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
221148fvresd 6794 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇𝑐))
222220, 221eqtrd 2778 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇𝑐))
223219, 222oveq12d 7293 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)))
224207, 216ffvelrnd 6962 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ ℂ)
225173, 216ffvelrnd 6962 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ∈ ℂ)
226 simplrr 775 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
227226, 222breqtrd 5100 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (𝑇𝑐))
228227gt0ne0d 11539 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ≠ 0)
229224, 225, 228divcan3d 11756 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)) = (𝑋𝑐))
230223, 229eqtrd 2778 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋𝑐))
231166, 216ffvelrnd 6962 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ 𝐷)
232230, 231eqeltrd 2839 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
23391ad3antrrr 727 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐹:𝐷⟶ℝ)
234233, 231ffvelrnd 6962 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℝ)
235234leidd 11541 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ≤ (𝐹‘(𝑋𝑐)))
236230fveq2d 6778 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋𝑐)))
237 fco 6624 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴𝐷) → (𝐹𝑋):𝐴⟶ℝ)
23891, 98, 237syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑋):𝐴⟶ℝ)
239150, 153, 238, 10, 10, 155off 7551 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℝ)
240 fss 6617 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · (𝐹𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
241239, 157, 240sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
242241ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
243242, 161fssresd 6641 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
244238ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℝ)
245244, 164fexd 7103 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) ∈ V)
246 offres 7826 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ (𝐹𝑋) ∈ V) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
247165, 245, 246syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
248247oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
249 fss 6617 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹𝑋):𝐴⟶ℂ)
250244, 157, 249sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℂ)
251250, 161fssresd 6641 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
252202, 204, 174, 251, 144, 209suppssof1 8015 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
253248, 252eqsstrd 3959 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
254140, 16, 142, 144, 148, 243, 253gsumpt 19563 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
255148fvresd 6794 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · (𝐹𝑋))‘𝑐))
25691ffnd 6601 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn 𝐷)
257 fnfco 6639 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝐷𝑋:𝐴𝐷) → (𝐹𝑋) Fn 𝐴)
258256, 98, 257syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹𝑋) Fn 𝐴)
259258ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) Fn 𝐴)
260 fnfvof 7550 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑇 Fn 𝐴 ∧ (𝐹𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
261214, 259, 164, 216, 260syl22anc 836 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
262 fvco3 6867 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋:𝐴𝐷𝑐𝐴) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
263166, 216, 262syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
264263oveq2d 7291 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
265261, 264eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
266254, 255, 2653eqtrd 2782 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
267266, 222oveq12d 7293 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)))
268234recnd 11003 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℂ)
269268, 225, 228divcan3d 11756 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)) = (𝐹‘(𝑋𝑐)))
270267, 269eqtrd 2778 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋𝑐)))
271235, 236, 2703brtr4d 5106 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
272135, 232, 271elrabd 3626 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
273272a1d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
274120simprbi 497 . . . . . . . . . . . . . . . 16 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
275119, 274syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
276 leloe 11061 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
27780, 122, 276sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
278275, 277mpbid 231 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘))))
279139, 273, 278mpjaodan 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
28087, 279embantd 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
28185, 280syl5bi 241 . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
282281ex 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
283282com23 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
284283expcom 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
285284adantl 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
286285a2d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
28731, 47, 63, 79, 84, 286findcard2s 8948 . . . . 5 (𝐴 ∈ Fin → (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})))
28810, 287mpcom 38 . . . 4 (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
2899, 288mpd 15 . . 3 (𝜑 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
290156ffnd 6601 . . . . . 6 (𝜑 → (𝑇f · 𝑋) Fn 𝐴)
291 fnresdm 6551 . . . . . 6 ((𝑇f · 𝑋) Fn 𝐴 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
292290, 291syl 17 . . . . 5 (𝜑 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
293292oveq2d 7291 . . . 4 (𝜑 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇f · 𝑋)))
294293, 6oveq12d 7293 . . 3 (𝜑 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)))
2953, 258, 10, 10, 155offn 7546 . . . . . . . 8 (𝜑 → (𝑇f · (𝐹𝑋)) Fn 𝐴)
296 fnresdm 6551 . . . . . . . 8 ((𝑇f · (𝐹𝑋)) Fn 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
297295, 296syl 17 . . . . . . 7 (𝜑 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
298297oveq2d 7291 . . . . . 6 (𝜑 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇f · (𝐹𝑋))))
299298, 6oveq12d 7293 . . . . 5 (𝜑 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)))
300299breq2d 5086 . . . 4 (𝜑 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
301300rabbidv 3414 . . 3 (𝜑 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
302289, 294, 3013eltr3d 2853 . 2 (𝜑 → ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
303 fveq2 6774 . . . 4 (𝑤 = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) → (𝐹𝑤) = (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))))
304303breq1d 5084 . . 3 (𝑤 = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
305304elrab 3624 . 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 𝑇))))
306302, 305sylib 217 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 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106  wral 3064  {crab 3068  Vcvv 3432  cdif 3884  cun 3885  wss 3887  c0 4256  {csn 4561   class class class wbr 5074  cmpt 5157  cres 5591  ccom 5593   Fn wfn 6428  wf 6429  cfv 6433  (class class class)co 7275  f cof 7531   supp csupp 7977  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876  +∞cpnf 11006   < clt 11009  cle 11010  cmin 11205   / cdiv 11632  [,)cico 13081  [,]cicc 13082  Σcsu 15397   Σg cgsu 17151  Mndcmnd 18385  SubMndcsubmnd 18429  CMndccmn 19386  Ringcrg 19783  fldccnfld 20597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-tpos 8042  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-sup 9201  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-rp 12731  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-0g 17152  df-gsum 17153  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-grp 18580  df-minusg 18581  df-mulg 18701  df-subg 18752  df-cntz 18923  df-cmn 19388  df-abl 19389  df-mgp 19721  df-ur 19738  df-ring 19785  df-cring 19786  df-oppr 19862  df-dvdsr 19883  df-unit 19884  df-invr 19914  df-dvr 19925  df-drng 19993  df-subrg 20022  df-cnfld 20598  df-refld 20810
This theorem is referenced by:  amgmlem  26139  amgmwlem  46506
  Copyright terms: Public domain W3C validator