Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sge0split Structured version   Visualization version   GIF version

Theorem sge0split 45204
Description: Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0split.a (𝜑𝐴𝑉)
sge0split.b (𝜑𝐵𝑊)
sge0split.u 𝑈 = (𝐴𝐵)
sge0split.in0 (𝜑 → (𝐴𝐵) = ∅)
sge0split.f (𝜑𝐹:𝑈⟶(0[,]+∞))
Assertion
Ref Expression
sge0split (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))

Proof of Theorem sge0split
Dummy variables 𝑎 𝑏 𝑥 𝑧 𝑦 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sge0split.a . . . . 5 (𝜑𝐴𝑉)
21adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐴𝑉)
3 sge0split.b . . . . 5 (𝜑𝐵𝑊)
43adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐵𝑊)
5 sge0split.u . . . 4 𝑈 = (𝐴𝐵)
6 sge0split.in0 . . . . 5 (𝜑 → (𝐴𝐵) = ∅)
76adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (𝐴𝐵) = ∅)
8 sge0split.f . . . . 5 (𝜑𝐹:𝑈⟶(0[,]+∞))
98adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐹:𝑈⟶(0[,]+∞))
10 simpr 485 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) ∈ ℝ)
112, 4, 5, 7, 9, 10sge0resplit 45201 . . 3 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
12 unexg 7738 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
131, 3, 12syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴𝐵) ∈ V)
145, 13eqeltrid 2837 . . . . . . 7 (𝜑𝑈 ∈ V)
1514adantr 481 . . . . . 6 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝑈 ∈ V)
1615, 9, 10sge0ssre 45192 . . . . 5 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^‘(𝐹𝐴)) ∈ ℝ)
1715, 9, 10sge0ssre 45192 . . . . 5 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^‘(𝐹𝐵)) ∈ ℝ)
18 rexadd 13213 . . . . 5 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
1916, 17, 18syl2anc 584 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
2019eqcomd 2738 . . 3 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
2111, 20eqtrd 2772 . 2 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
22 simpl 483 . . 3 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → 𝜑)
23 simpr 485 . . . . 5 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ¬ (Σ^𝐹) ∈ ℝ)
2414, 8sge0repnf 45181 . . . . . 6 (𝜑 → ((Σ^𝐹) ∈ ℝ ↔ ¬ (Σ^𝐹) = +∞))
2524adantr 481 . . . . 5 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ((Σ^𝐹) ∈ ℝ ↔ ¬ (Σ^𝐹) = +∞))
2623, 25mtbid 323 . . . 4 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ¬ ¬ (Σ^𝐹) = +∞)
2726notnotrd 133 . . 3 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = +∞)
2814, 8sge0xrcl 45180 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ*)
2928adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) ∈ ℝ*)
30 ssun1 4172 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
3130, 5sseqtrri 4019 . . . . . . . . 9 𝐴𝑈
3231a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
338, 32fssresd 6758 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
341, 33sge0xrcl 45180 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ*)
35 iccssxr 13409 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
36 ssun2 4173 . . . . . . . . . . 11 𝐵 ⊆ (𝐴𝐵)
3736, 5sseqtrri 4019 . . . . . . . . . 10 𝐵𝑈
3837a1i 11 . . . . . . . . 9 (𝜑𝐵𝑈)
398, 38fssresd 6758 . . . . . . . 8 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
403, 39sge0cl 45176 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ (0[,]+∞))
4135, 40sselid 3980 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ*)
4234, 41xaddcld 13282 . . . . 5 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ*)
4342adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ*)
44 pnfxr 11270 . . . . . . . . 9 +∞ ∈ ℝ*
45 eqid 2732 . . . . . . . . 9 +∞ = +∞
46 xreqle 44107 . . . . . . . . 9 ((+∞ ∈ ℝ* ∧ +∞ = +∞) → +∞ ≤ +∞)
4744, 45, 46mp2an 690 . . . . . . . 8 +∞ ≤ +∞
4847a1i 11 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ≤ +∞)
4914adantr 481 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝑈 ∈ V)
508adantr 481 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝐹:𝑈⟶(0[,]+∞))
51 rnresss 6017 . . . . . . . . . . 11 ran (𝐹𝐴) ⊆ ran 𝐹
5251sseli 3978 . . . . . . . . . 10 (+∞ ∈ ran (𝐹𝐴) → +∞ ∈ ran 𝐹)
5352adantl 482 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ∈ ran 𝐹)
5449, 50, 53sge0pnfval 45168 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) = +∞)
55 xrge0neqmnf 13431 . . . . . . . . . . . . . 14 ((Σ^‘(𝐹𝐵)) ∈ (0[,]+∞) → (Σ^‘(𝐹𝐵)) ≠ -∞)
5640, 55syl 17 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝐹𝐵)) ≠ -∞)
57 xaddpnf2 13208 . . . . . . . . . . . . 13 (((Σ^‘(𝐹𝐵)) ∈ ℝ* ∧ (Σ^‘(𝐹𝐵)) ≠ -∞) → (+∞ +𝑒^‘(𝐹𝐵))) = +∞)
5841, 56, 57syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (+∞ +𝑒^‘(𝐹𝐵))) = +∞)
5958eqcomd 2738 . . . . . . . . . . 11 (𝜑 → +∞ = (+∞ +𝑒^‘(𝐹𝐵))))
6059adantr 481 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ = (+∞ +𝑒^‘(𝐹𝐵))))
611adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝐴𝑉)
6233adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
63 simpr 485 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ∈ ran (𝐹𝐴))
6461, 62, 63sge0pnfval 45168 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) = +∞)
6564oveq1d 7426 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (+∞ +𝑒^‘(𝐹𝐵))))
6660, 54, 653eqtr4d 2782 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
6766, 54eqtr3d 2774 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = +∞)
6854, 67breq12d 5161 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ↔ +∞ ≤ +∞))
6948, 68mpbird 256 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
7047a1i 11 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ≤ +∞)
7114adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝑈 ∈ V)
728adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
73 rnresss 6017 . . . . . . . . . . . . 13 ran (𝐹𝐵) ⊆ ran 𝐹
7473sseli 3978 . . . . . . . . . . . 12 (+∞ ∈ ran (𝐹𝐵) → +∞ ∈ ran 𝐹)
7574adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ∈ ran 𝐹)
7671, 72, 75sge0pnfval 45168 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) = +∞)
773adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝐵𝑊)
7839adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
79 simpr 485 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ∈ ran (𝐹𝐵))
8077, 78, 79sge0pnfval 45168 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = +∞)
8180oveq2d 7427 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) +𝑒 +∞))
821, 33sge0cl 45176 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ (0[,]+∞))
83 xrge0neqmnf 13431 . . . . . . . . . . . . . 14 ((Σ^‘(𝐹𝐴)) ∈ (0[,]+∞) → (Σ^‘(𝐹𝐴)) ≠ -∞)
8482, 83syl 17 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝐹𝐴)) ≠ -∞)
85 xaddpnf1 13207 . . . . . . . . . . . . 13 (((Σ^‘(𝐹𝐴)) ∈ ℝ* ∧ (Σ^‘(𝐹𝐴)) ≠ -∞) → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8634, 84, 85syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8786adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8881, 87eqtrd 2772 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = +∞)
8976, 88breq12d 5161 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ↔ +∞ ≤ +∞))
9070, 89mpbird 256 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
9190adantlr 713 . . . . . . 7 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
92 simpr 485 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
93 vex 3478 . . . . . . . . . . . . 13 𝑧 ∈ V
94 eqid 2732 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
9594elrnmpt 5955 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦)))
9693, 95ax-mp 5 . . . . . . . . . . . 12 (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦))
9792, 96sylib 217 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦))
98 simp3 1138 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑧 = Σ𝑦𝑥 (𝐹𝑦))
99 inss1 4228 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝑥𝐴)
100 inss2 4229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐴) ⊆ 𝐴
10199, 100sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ 𝐴
102 inss2 4229 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝑥𝐵)
103 inss2 4229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐵) ⊆ 𝐵
104102, 103sstri 3991 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ 𝐵
105101, 104ssini 4231 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝐴𝐵)
106105a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝐴𝐵))
107106, 6sseqtrd 4022 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ ∅)
108 ss0 4398 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ ∅ → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
110109ad3antrrr 728 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
111 indi 4273 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
112111eqcomi 2741 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
113112a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
1145eqcomi 2741 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴𝐵) = 𝑈
115114ineq2i 4209 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∩ (𝐴𝐵)) = (𝑥𝑈)
116115a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ (𝐴𝐵)) = (𝑥𝑈))
117 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
118 elpwi 4609 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
119117, 118syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
120 df-ss 3965 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
121120biimpi 215 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = 𝑥)
122119, 121syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝑈) = 𝑥)
123113, 116, 1223eqtrrd 2777 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
124123adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
125 elinel2 4196 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
126125adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
127 rge0ssre 13435 . . . . . . . . . . . . . . . . . . . . 21 (0[,)+∞) ⊆ ℝ
1288ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
129 pm4.56 987 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ↔ ¬ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
130129biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
131 elun 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (+∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) ↔ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
132130, 131sylnibr 328 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)))
133132adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)))
134 rnresun 43958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran (𝐹 ↾ (𝐴𝐵)) = (ran (𝐹𝐴) ∪ ran (𝐹𝐵))
135134eqcomi 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran (𝐹 ↾ (𝐴𝐵))
136135a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran (𝐹 ↾ (𝐴𝐵)))
137114reseq2i 5978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 ↾ (𝐴𝐵)) = (𝐹𝑈)
138137rneqi 5936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran (𝐹 ↾ (𝐴𝐵)) = ran (𝐹𝑈)
139138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran (𝐹 ↾ (𝐴𝐵)) = ran (𝐹𝑈))
140 ffn 6717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹:𝑈⟶(0[,]+∞) → 𝐹 Fn 𝑈)
141 fnresdm 6669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 Fn 𝑈 → (𝐹𝑈) = 𝐹)
1428, 140, 1413syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑈) = 𝐹)
143142rneqd 5937 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran (𝐹𝑈) = ran 𝐹)
144136, 139, 1433eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran 𝐹)
145144ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran 𝐹)
146133, 145neleqtrd 2855 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ ran 𝐹)
147128, 146fge0iccico 45165 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,)+∞))
148147ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
149119adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑥𝑈)
150 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑥)
151149, 150sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
152151adantll 712 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
153148, 152ffvelcdmd 7087 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
154127, 153sselid 3980 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℝ)
155154recnd 11244 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
156110, 124, 126, 155fsumsplit 15689 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
157 infi 9270 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ Fin → (𝑥𝐴) ∈ Fin)
158125, 157syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
159158adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ∈ Fin)
160 simpl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
161 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝑥𝐴) → 𝑦𝑥)
162161adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝑥)
163160, 162, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) ∈ ℝ)
164159, 163fsumrecl 15682 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ)
165 infi 9270 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ Fin → (𝑥𝐵) ∈ Fin)
166125, 165syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
167166adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ∈ Fin)
168 simpl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
169 elinel1 4195 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝑥𝐵) → 𝑦𝑥)
170169adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → 𝑦𝑥)
171168, 170, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → (𝐹𝑦) ∈ ℝ)
172167, 171fsumrecl 15682 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ)
173 rexadd 13213 . . . . . . . . . . . . . . . . . . . 20 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
174164, 172, 173syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
175174eqcomd 2738 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
176156, 175eqtrd 2772 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
177 ressxr 11260 . . . . . . . . . . . . . . . . . . . 20 ℝ ⊆ ℝ*
178177, 164sselid 3980 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ*)
179177, 172sselid 3980 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ*)
1801adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → 𝐴𝑉)
18133adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
182 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → ¬ +∞ ∈ ran (𝐹𝐴))
183181, 182fge0iccico 45165 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,)+∞))
184180, 183sge0reval 45167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
185184eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
18634adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) ∈ ℝ*)
187185, 186eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
188187adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
1893adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐵𝑊)
19039adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
191 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ ran (𝐹𝐵))
192190, 191fge0iccico 45165 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,)+∞))
193189, 192sge0reval 45167 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
194193eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
19541adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) ∈ ℝ*)
196194, 195eqeltrd 2833 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
197196adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
198188, 197jca 512 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
199198adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
200178, 179, 199jca31 515 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ* ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ*) ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)))
201180adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐴𝑉)
202181adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
203182adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹𝐴))
204202, 203fge0iccico 45165 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐴):𝐴⟶(0[,)+∞))
205100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ⊆ 𝐴)
206158adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ∈ Fin)
207201, 204, 205, 206fsumlesge0 45172 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ≤ (Σ^‘(𝐹𝐴)))
208100sseli 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
209 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝑥𝐴) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
211210adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
212211sumeq2dv 15651 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦))
213184adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
214212, 213breq12d 5161 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ≤ (Σ^‘(𝐹𝐴)) ↔ Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < )))
215207, 214mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
216215adantlr 713 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
217189adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐵𝑊)
218190adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
219191adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹𝐵))
220218, 219fge0iccico 45165 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐵):𝐵⟶(0[,)+∞))
221103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ⊆ 𝐵)
222166adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ∈ Fin)
223217, 220, 221, 222fsumlesge0 45172 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) ≤ (Σ^‘(𝐹𝐵)))
224103sseli 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
225 fvres 6910 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝑥𝐵) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
227226adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
228227sumeq2dv 15651 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))
229193adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
230228, 229breq12d 5161 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) ≤ (Σ^‘(𝐹𝐵)) ↔ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
231223, 230mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
232231adantllr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
233216, 232jca 512 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
234 xle2add 13240 . . . . . . . . . . . . . . . . . 18 (((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ* ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ*) ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)) → ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
235200, 233, 234sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
236176, 235eqbrtrd 5170 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
2372363adant3 1132 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
23898, 237eqbrtrd 5170 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
2392383exp 1119 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑧 = Σ𝑦𝑥 (𝐹𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))))
240239rexlimdv 3153 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
241240adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
24297, 241mpd 15 . . . . . . . . . 10 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
243242ralrimiva 3146 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
244147sge0rnre 45159 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ)
245177a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ℝ ⊆ ℝ*)
246244, 245sstrd 3992 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ*)
247188, 197xaddcld 13282 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) ∈ ℝ*)
248 supxrleub 13307 . . . . . . . . . 10 ((ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ* ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) ∈ ℝ*) → (sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
249246, 247, 248syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
250243, 249mpbird 256 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
25114ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝑈 ∈ V)
252251, 147sge0reval 45167 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
253184adantr 481 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
254193adantlr 713 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
255253, 254oveq12d 7429 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
256250, 252, 2553brtr4d 5180 . . . . . . 7 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
25791, 256pm2.61dan 811 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
25869, 257pm2.61dan 811 . . . . 5 (𝜑 → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
259258adantr 481 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
260 pnfge 13112 . . . . . . 7 (((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ* → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
26142, 260syl 17 . . . . . 6 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
262261adantr 481 . . . . 5 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
263 id 22 . . . . . . 7 ((Σ^𝐹) = +∞ → (Σ^𝐹) = +∞)
264263eqcomd 2738 . . . . . 6 ((Σ^𝐹) = +∞ → +∞ = (Σ^𝐹))
265264adantl 482 . . . . 5 ((𝜑 ∧ (Σ^𝐹) = +∞) → +∞ = (Σ^𝐹))
266262, 265breqtrd 5174 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ (Σ^𝐹))
26729, 43, 259, 266xrletrid 13136 . . 3 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
26822, 27, 267syl2anc 584 . 2 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
26921, 268pm2.61dan 811 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2940  wral 3061  wrex 3070  Vcvv 3474  cun 3946  cin 3947  wss 3948  c0 4322  𝒫 cpw 4602   class class class wbr 5148  cmpt 5231  ran crn 5677  cres 5678   Fn wfn 6538  wf 6539  cfv 6543  (class class class)co 7411  Fincfn 8941  supcsup 9437  cr 11111  0cc0 11112   + caddc 11115  +∞cpnf 11247  -∞cmnf 11248  *cxr 11249   < clt 11250  cle 11251   +𝑒 cxad 13092  [,)cico 13328  [,]cicc 13329  Σcsu 15634  Σ^csumge0 45157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-xadd 13095  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-sum 15635  df-sumge0 45158
This theorem is referenced by:  sge0splitmpt  45206
  Copyright terms: Public domain W3C validator