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

Theorem jensen 25726
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 6505 . . . . . . . 8 (𝜑𝑇 Fn 𝐴)
4 fnresdm 6455 . . . . . . . 8 (𝑇 Fn 𝐴 → (𝑇𝐴) = 𝑇)
53, 4syl 17 . . . . . . 7 (𝜑 → (𝑇𝐴) = 𝑇)
65oveq2d 7186 . . . . . 6 (𝜑 → (ℂfld Σg (𝑇𝐴)) = (ℂfld Σg 𝑇))
71, 6breqtrrd 5058 . . . . 5 (𝜑 → 0 < (ℂfld Σg (𝑇𝐴)))
8 ssid 3899 . . . . 5 𝐴𝐴
97, 8jctil 523 . . . 4 (𝜑 → (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))))
10 jensen.4 . . . . 5 (𝜑𝐴 ∈ Fin)
11 sseq1 3902 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
12 reseq2 5820 . . . . . . . . . . . . 13 (𝑎 = ∅ → (𝑇𝑎) = (𝑇 ↾ ∅))
13 res0 5829 . . . . . . . . . . . . 13 (𝑇 ↾ ∅) = ∅
1412, 13eqtrdi 2789 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑇𝑎) = ∅)
1514oveq2d 7186 . . . . . . . . . . 11 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg ∅))
16 cnfld0 20241 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
1716gsum0 18010 . . . . . . . . . . 11 (ℂfld Σg ∅) = 0
1815, 17eqtrdi 2789 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = 0)
1918breq2d 5042 . . . . . . . . 9 (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < 0))
2011, 19anbi12d 634 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21 reseq2 5820 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ ∅))
2221oveq2d 7186 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)))
2322, 18oveq12d 7188 . . . . . . . . 9 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0))
24 reseq2 5820 . . . . . . . . . . . . 13 (𝑎 = ∅ → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ ∅))
2524oveq2d 7186 . . . . . . . . . . . 12 (𝑎 = ∅ → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)))
2625, 18oveq12d 7188 . . . . . . . . . . 11 (𝑎 = ∅ → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0))
2726breq2d 5042 . . . . . . . . . 10 (𝑎 = ∅ → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)))
2827rabbidv 3381 . . . . . . . . 9 (𝑎 = ∅ → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
2923, 28eleq12d 2827 . . . . . . . 8 (𝑎 = ∅ → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)}))
3020, 29imbi12d 348 . . . . . . 7 (𝑎 = ∅ → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})))
3130imbi2d 344 . . . . . 6 (𝑎 = ∅ → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)}))))
32 sseq1 3902 . . . . . . . . 9 (𝑎 = 𝑘 → (𝑎𝐴𝑘𝐴))
33 reseq2 5820 . . . . . . . . . . 11 (𝑎 = 𝑘 → (𝑇𝑎) = (𝑇𝑘))
3433oveq2d 7186 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝑘)))
3534breq2d 5042 . . . . . . . . 9 (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝑘))))
3632, 35anbi12d 634 . . . . . . . 8 (𝑎 = 𝑘 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘)))))
37 reseq2 5820 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝑘))
3837oveq2d 7186 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)))
3938, 34oveq12d 7188 . . . . . . . . 9 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
40 reseq2 5820 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝑘))
4140oveq2d 7186 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)))
4241, 34oveq12d 7188 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
4342breq2d 5042 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
4443rabbidv 3381 . . . . . . . . 9 (𝑎 = 𝑘 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})
4539, 44eleq12d 2827 . . . . . . . 8 (𝑎 = 𝑘 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))
4636, 45imbi12d 348 . . . . . . 7 (𝑎 = 𝑘 → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})))
4746imbi2d 344 . . . . . 6 (𝑎 = 𝑘 → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))))
48 sseq1 3902 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49 reseq2 5820 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
5049oveq2d 7186 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
5150breq2d 5042 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5248, 51anbi12d 634 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53 reseq2 5820 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})))
5453oveq2d 7186 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
5554, 50oveq12d 7188 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56 reseq2 5820 . . . . . . . . . . . . 13 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})))
5756oveq2d 7186 . . . . . . . . . . . 12 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))))
5857, 50oveq12d 7188 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5958breq2d 5042 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
6059rabbidv 3381 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
6155, 60eleq12d 2827 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
6252, 61imbi12d 348 . . . . . . 7 (𝑎 = (𝑘 ∪ {𝑐}) → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
6362imbi2d 344 . . . . . 6 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
64 sseq1 3902 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
65 reseq2 5820 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑇𝑎) = (𝑇𝐴))
6665oveq2d 7186 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝐴)))
6766breq2d 5042 . . . . . . . . 9 (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝐴))))
6864, 67anbi12d 634 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴)))))
69 reseq2 5820 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑇f · 𝑋) ↾ 𝑎) = ((𝑇f · 𝑋) ↾ 𝐴))
7069oveq2d 7186 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)))
7170, 66oveq12d 7188 . . . . . . . . 9 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
72 reseq2 5820 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝑎) = ((𝑇f · (𝐹𝑋)) ↾ 𝐴))
7372oveq2d 7186 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)))
7473, 66oveq12d 7188 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
7574breq2d 5042 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))))
7675rabbidv 3381 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
7771, 76eleq12d 2827 . . . . . . . 8 (𝑎 = 𝐴 → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
7868, 77imbi12d 348 . . . . . . 7 (𝑎 = 𝐴 → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})))
7978imbi2d 344 . . . . . 6 (𝑎 = 𝐴 → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))))
80 0re 10721 . . . . . . . . . 10 0 ∈ ℝ
8180ltnri 10827 . . . . . . . . 9 ¬ 0 < 0
8281pm2.21i 119 . . . . . . . 8 (0 < 0 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ ∅)) / 0)})
8382adantl 485 . . . . . . 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 454 . . . . . . . . . . . 12 (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) ↔ (𝑘𝐴 → (0 < (ℂfld Σg (𝑇𝑘)) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})))
86 simprl 771 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
8786unssad 4077 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘𝐴)
88 simpr 488 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇𝑘)))
89 jensen.1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ⊆ ℝ)
9089ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐷 ⊆ ℝ)
91 jensen.2 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐷⟶ℝ)
9291ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐹:𝐷⟶ℝ)
93 simplll 775 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝜑)
94 jensen.3 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
9593, 94sylan 583 . . . . . . . . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) ∧ (𝑥𝐷𝑦𝐷𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
103 simpllr 776 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ¬ 𝑐𝑘)
10486adantr 484 . . . . . . . . . . . . . . . . . 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 20239 . . . . . . . . . . . . . . . . . . . . . . 23 fld ∈ Ring
108 ringcmn 19453 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109107, 108mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
11010ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111110, 87ssfid 8819 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
112 rege0subm 20273 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,)+∞) ∈ (SubMnd‘ℂfld)
113112a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
1142ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
115114, 87fssresd 6545 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘):𝑘⟶(0[,)+∞))
116 c0ex 10713 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
117116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
118115, 111, 117fdmfifsupp 8916 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘) finSupp 0)
11916, 109, 111, 113, 115, 118gsumsubmcl 19158 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞))
120 elrege0 12928 . . . . . . . . . . . . . . . . . . . . . 22 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) ↔ ((ℂfld Σg (𝑇𝑘)) ∈ ℝ ∧ 0 ≤ (ℂfld Σg (𝑇𝑘))))
121120simplbi 501 . . . . . . . . . . . . . . . . . . . . 21 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
122119, 121syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
123122adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
124 simprl 771 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 0 < (ℂfld Σg (𝑇𝑘)))
125123, 124elrpd 12511 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ+)
126 simprr 773 . . . . . . . . . . . . . . . . . . . 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 6674 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
128127breq1d 5040 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
129128elrab 3588 . . . . . . . . . . . . . . . . . . . 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 221 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
131130simpld 498 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ 𝐷)
132130simprd 499 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
13390, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 125, 131, 132jensenlem2 25725 . . . . . . . . . . . . . . . . 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 6674 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135134breq1d 5040 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136135elrab 3588 . . . . . . . . . . . . . . . . 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 237 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
138137expr 460 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → (((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))} → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
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 20221 . . . . . . . . . . . . . . . . . . . . 21 ℂ = (Base‘ℂfld)
141 ringmnd 19426 . . . . . . . . . . . . . . . . . . . . . 22 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
142107, 141mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ℂfld ∈ Mnd)
143110, 86ssfid 8819 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
144143adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
145 ssun2 4063 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐} ⊆ (𝑘 ∪ {𝑐})
146 vsnid 4553 . . . . . . . . . . . . . . . . . . . . . . 23 𝑐 ∈ {𝑐}
147145, 146sselii 3874 . . . . . . . . . . . . . . . . . . . . . 22 𝑐 ∈ (𝑘 ∪ {𝑐})
148147a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
149 remulcl 10700 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
150149adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
151 rge0ssre 12930 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
152 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
1532, 151, 152sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇:𝐴⟶ℝ)
15498, 89fssd 6522 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋:𝐴⟶ℝ)
155 inidm 4109 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝐴) = 𝐴
156150, 153, 154, 10, 10, 155off 7442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℝ)
157 ax-resscn 10672 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ ⊆ ℂ
158 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · 𝑋):𝐴⟶ℂ)
159156, 157, 158sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · 𝑋):𝐴⟶ℂ)
160159ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · 𝑋):𝐴⟶ℂ)
16186adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
162160, 161fssresd 6545 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
1632ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
164110adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐴 ∈ Fin)
165163, 164fexd 7000 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 ∈ V)
16698ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴𝐷)
167166, 164fexd 7000 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 ∈ V)
168 offres 7709 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
169165, 167, 168syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
170169oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
171151, 157sstri 3886 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℂ
172 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
173163, 171, 172sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶ℂ)
174173, 161fssresd 6545 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
175 eldifi 4017 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
176175adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
177176fvresd 6694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇𝑥))
178 difun2 4370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
179 difss 4022 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∖ {𝑐}) ⊆ 𝑘
180178, 179eqsstri 3911 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
181180sseli 3873 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥𝑘)
182 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 = (ℂfld Σg (𝑇𝑘)))
18387adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘𝐴)
184163, 183feqresmpt 6738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑘) = (𝑥𝑘 ↦ (𝑇𝑥)))
185184oveq2d 7186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))))
186111adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘 ∈ Fin)
187183sselda 3877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 𝑥𝐴)
188163ffvelrnda 6861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝐴) → (𝑇𝑥) ∈ (0[,)+∞))
189187, 188syldan 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ (0[,)+∞))
190171, 189sseldi 3875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℂ)
191186, 190gsumfsum 20284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))) = Σ𝑥𝑘 (𝑇𝑥))
192182, 185, 1913eqtrrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → Σ𝑥𝑘 (𝑇𝑥) = 0)
193 elrege0 12928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑇𝑥) ∈ (0[,)+∞) ↔ ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
194189, 193sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
195194simpld 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℝ)
196194simprd 499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 0 ≤ (𝑇𝑥))
197186, 195, 196fsum00 15246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (Σ𝑥𝑘 (𝑇𝑥) = 0 ↔ ∀𝑥𝑘 (𝑇𝑥) = 0))
198192, 197mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ∀𝑥𝑘 (𝑇𝑥) = 0)
199198r19.21bi 3121 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) = 0)
200181, 199sylan2 596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇𝑥) = 0)
201177, 200eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
202174, 201suppss 7889 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
203 mul02 10896 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
204203adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
20589ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℝ)
206205, 157sstrdi 3889 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℂ)
207166, 206fssd 6522 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴⟶ℂ)
208207, 161fssresd 6545 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
209116a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 ∈ V)
210202, 204, 174, 208, 144, 209suppssof1 7894 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
211170, 210eqsstrd 3915 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
212140, 16, 142, 144, 148, 162, 211gsumpt 19201 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
213148fvresd 6694 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · 𝑋)‘𝑐))
214163ffnd 6505 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 Fn 𝐴)
215166ffnd 6505 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 Fn 𝐴)
216161, 148sseldd 3878 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐𝐴)
217 fnfvof 7441 . . . . . . . . . . . . . . . . . . . . 21 (((𝑇 Fn 𝐴𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
218214, 215, 164, 216, 217syl22anc 838 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
219212, 213, 2183eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝑋𝑐)))
220140, 16, 142, 144, 148, 174, 202gsumpt 19201 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
221148fvresd 6694 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇𝑐))
222220, 221eqtrd 2773 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇𝑐))
223219, 222oveq12d 7188 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)))
224207, 216ffvelrnd 6862 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ ℂ)
225173, 216ffvelrnd 6862 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ∈ ℂ)
226 simplrr 778 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
227226, 222breqtrd 5056 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (𝑇𝑐))
228227gt0ne0d 11282 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ≠ 0)
229224, 225, 228divcan3d 11499 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)) = (𝑋𝑐))
230223, 229eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋𝑐))
231166, 216ffvelrnd 6862 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ 𝐷)
232230, 231eqeltrd 2833 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
23391ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐹:𝐷⟶ℝ)
234233, 231ffvelrnd 6862 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℝ)
235234leidd 11284 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ≤ (𝐹‘(𝑋𝑐)))
236230fveq2d 6678 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋𝑐)))
237 fco 6528 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴𝐷) → (𝐹𝑋):𝐴⟶ℝ)
23891, 98, 237syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑋):𝐴⟶ℝ)
239150, 153, 238, 10, 10, 155off 7442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℝ)
240 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇f · (𝐹𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
241239, 157, 240sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
242241ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇f · (𝐹𝑋)):𝐴⟶ℂ)
243242, 161fssresd 6545 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
244238ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℝ)
245244, 164fexd 7000 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) ∈ V)
246 offres 7709 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ (𝐹𝑋) ∈ V) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
247165, 245, 246syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
248247oveq1d 7185 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
249 fss 6521 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹𝑋):𝐴⟶ℂ)
250244, 157, 249sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℂ)
251250, 161fssresd 6545 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
252202, 204, 174, 251, 144, 209suppssof1 7894 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘f · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
253248, 252eqsstrd 3915 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
254140, 16, 142, 144, 148, 243, 253gsumpt 19201 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
255148fvresd 6694 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇f · (𝐹𝑋))‘𝑐))
25691ffnd 6505 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn 𝐷)
257 fnfco 6543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝐷𝑋:𝐴𝐷) → (𝐹𝑋) Fn 𝐴)
258256, 98, 257syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹𝑋) Fn 𝐴)
259258ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) Fn 𝐴)
260 fnfvof 7441 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑇 Fn 𝐴 ∧ (𝐹𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
261214, 259, 164, 216, 260syl22anc 838 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
262 fvco3 6767 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋:𝐴𝐷𝑐𝐴) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
263166, 216, 262syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
264263oveq2d 7186 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
265261, 264eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇f · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
266254, 255, 2653eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
267266, 222oveq12d 7188 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)))
268234recnd 10747 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℂ)
269268, 225, 228divcan3d 11499 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)) = (𝐹‘(𝑋𝑐)))
270267, 269eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋𝑐)))
271235, 236, 2703brtr4d 5062 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
272135, 232, 271elrabd 3590 . . . . . . . . . . . . . . 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 500 . . . . . . . . . . . . . . . 16 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
275119, 274syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
276 leloe 10805 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
27780, 122, 276sylancr 590 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
278275, 277mpbid 235 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘))))
279139, 273, 278mpjaodan 958 . . . . . . . . . . . . 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 245 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
282281ex 416 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑐𝑘) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
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 417 . . . . . . . 8 𝑐𝑘 → (𝜑 → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
285284adantl 485 . . . . . . 7 ((𝑘 ∈ Fin ∧ ¬ 𝑐𝑘) → (𝜑 → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇f · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
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 8764 . . . . 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 6505 . . . . . 6 (𝜑 → (𝑇f · 𝑋) Fn 𝐴)
291 fnresdm 6455 . . . . . 6 ((𝑇f · 𝑋) Fn 𝐴 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
292290, 291syl 17 . . . . 5 (𝜑 → ((𝑇f · 𝑋) ↾ 𝐴) = (𝑇f · 𝑋))
293292oveq2d 7186 . . . 4 (𝜑 → (ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇f · 𝑋)))
294293, 6oveq12d 7188 . . 3 (𝜑 → ((ℂfld Σg ((𝑇f · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)))
2953, 258, 10, 10, 155offn 7437 . . . . . . . 8 (𝜑 → (𝑇f · (𝐹𝑋)) Fn 𝐴)
296 fnresdm 6455 . . . . . . . 8 ((𝑇f · (𝐹𝑋)) Fn 𝐴 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
297295, 296syl 17 . . . . . . 7 (𝜑 → ((𝑇f · (𝐹𝑋)) ↾ 𝐴) = (𝑇f · (𝐹𝑋)))
298297oveq2d 7186 . . . . . 6 (𝜑 → (ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇f · (𝐹𝑋))))
299298, 6oveq12d 7188 . . . . 5 (𝜑 → ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)))
300299breq2d 5042 . . . 4 (𝜑 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
301300rabbidv 3381 . . 3 (𝜑 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇f · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
302289, 294, 3013eltr3d 2847 . 2 (𝜑 → ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
303 fveq2 6674 . . . 4 (𝑤 = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) → (𝐹𝑤) = (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))))
304303breq1d 5040 . . 3 (𝑤 = ((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹𝑤) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇f · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
305304elrab 3588 . 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 221 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 209  wa 399  wo 846  w3a 1088   = wceq 1542  wcel 2114  wral 3053  {crab 3057  Vcvv 3398  cdif 3840  cun 3841  wss 3843  c0 4211  {csn 4516   class class class wbr 5030  cmpt 5110  cres 5527  ccom 5529   Fn wfn 6334  wf 6335  cfv 6339  (class class class)co 7170  f cof 7423   supp csupp 7856  Fincfn 8555  cc 10613  cr 10614  0cc0 10615  1c1 10616   + caddc 10618   · cmul 10620  +∞cpnf 10750   < clt 10753  cle 10754  cmin 10948   / cdiv 11375  [,)cico 12823  [,]cicc 12824  Σcsu 15135   Σg cgsu 16817  Mndcmnd 18027  SubMndcsubmnd 18071  CMndccmn 19024  Ringcrg 19416  fldccnfld 20217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-inf2 9177  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693  ax-addf 10694  ax-mulf 10695
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-of 7425  df-om 7600  df-1st 7714  df-2nd 7715  df-supp 7857  df-tpos 7921  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-er 8320  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-fsupp 8907  df-sup 8979  df-oi 9047  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-rp 12473  df-ico 12827  df-icc 12828  df-fz 12982  df-fzo 13125  df-seq 13461  df-exp 13522  df-hash 13783  df-cj 14548  df-re 14549  df-im 14550  df-sqrt 14684  df-abs 14685  df-clim 14935  df-sum 15136  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-sets 16593  df-ress 16594  df-plusg 16681  df-mulr 16682  df-starv 16683  df-tset 16687  df-ple 16688  df-ds 16690  df-unif 16691  df-0g 16818  df-gsum 16819  df-mre 16960  df-mrc 16961  df-acs 16963  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-submnd 18073  df-grp 18222  df-minusg 18223  df-mulg 18343  df-subg 18394  df-cntz 18565  df-cmn 19026  df-abl 19027  df-mgp 19359  df-ur 19371  df-ring 19418  df-cring 19419  df-oppr 19495  df-dvdsr 19513  df-unit 19514  df-invr 19544  df-dvr 19555  df-drng 19623  df-subrg 19652  df-cnfld 20218  df-refld 20421
This theorem is referenced by:  amgmlem  25727  amgmwlem  45959
  Copyright terms: Public domain W3C validator