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 46364
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 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐴𝑉)
3 sge0split.b . . . . 5 (𝜑𝐵𝑊)
43adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐵𝑊)
5 sge0split.u . . . 4 𝑈 = (𝐴𝐵)
6 sge0split.in0 . . . . 5 (𝜑 → (𝐴𝐵) = ∅)
76adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (𝐴𝐵) = ∅)
8 sge0split.f . . . . 5 (𝜑𝐹:𝑈⟶(0[,]+∞))
98adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝐹:𝑈⟶(0[,]+∞))
10 simpr 484 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) ∈ ℝ)
112, 4, 5, 7, 9, 10sge0resplit 46361 . . 3 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
12 unexg 7761 . . . . . . . . 9 ((𝐴𝑉𝐵𝑊) → (𝐴𝐵) ∈ V)
131, 3, 12syl2anc 584 . . . . . . . 8 (𝜑 → (𝐴𝐵) ∈ V)
145, 13eqeltrid 2842 . . . . . . 7 (𝜑𝑈 ∈ V)
1514adantr 480 . . . . . 6 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → 𝑈 ∈ V)
1615, 9, 10sge0ssre 46352 . . . . 5 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^‘(𝐹𝐴)) ∈ ℝ)
1715, 9, 10sge0ssre 46352 . . . . 5 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^‘(𝐹𝐵)) ∈ ℝ)
18 rexadd 13270 . . . . 5 (((Σ^‘(𝐹𝐴)) ∈ ℝ ∧ (Σ^‘(𝐹𝐵)) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
1916, 17, 18syl2anc 584 . . . 4 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))))
2019eqcomd 2740 . . 3 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → ((Σ^‘(𝐹𝐴)) + (Σ^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
2111, 20eqtrd 2774 . 2 ((𝜑 ∧ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
22 simpl 482 . . 3 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → 𝜑)
23 simpr 484 . . . . 5 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ¬ (Σ^𝐹) ∈ ℝ)
2414, 8sge0repnf 46341 . . . . . 6 (𝜑 → ((Σ^𝐹) ∈ ℝ ↔ ¬ (Σ^𝐹) = +∞))
2524adantr 480 . . . . 5 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ((Σ^𝐹) ∈ ℝ ↔ ¬ (Σ^𝐹) = +∞))
2623, 25mtbid 324 . . . 4 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → ¬ ¬ (Σ^𝐹) = +∞)
2726notnotrd 133 . . 3 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = +∞)
2814, 8sge0xrcl 46340 . . . . 5 (𝜑 → (Σ^𝐹) ∈ ℝ*)
2928adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) ∈ ℝ*)
30 ssun1 4187 . . . . . . . . . 10 𝐴 ⊆ (𝐴𝐵)
3130, 5sseqtrri 4032 . . . . . . . . 9 𝐴𝑈
3231a1i 11 . . . . . . . 8 (𝜑𝐴𝑈)
338, 32fssresd 6775 . . . . . . 7 (𝜑 → (𝐹𝐴):𝐴⟶(0[,]+∞))
341, 33sge0xrcl 46340 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ ℝ*)
35 iccssxr 13466 . . . . . . 7 (0[,]+∞) ⊆ ℝ*
36 ssun2 4188 . . . . . . . . . . 11 𝐵 ⊆ (𝐴𝐵)
3736, 5sseqtrri 4032 . . . . . . . . . 10 𝐵𝑈
3837a1i 11 . . . . . . . . 9 (𝜑𝐵𝑈)
398, 38fssresd 6775 . . . . . . . 8 (𝜑 → (𝐹𝐵):𝐵⟶(0[,]+∞))
403, 39sge0cl 46336 . . . . . . 7 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ (0[,]+∞))
4135, 40sselid 3992 . . . . . 6 (𝜑 → (Σ^‘(𝐹𝐵)) ∈ ℝ*)
4234, 41xaddcld 13339 . . . . 5 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ*)
4342adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ*)
44 pnfxr 11312 . . . . . . . . 9 +∞ ∈ ℝ*
45 eqid 2734 . . . . . . . . 9 +∞ = +∞
46 xreqle 45268 . . . . . . . . 9 ((+∞ ∈ ℝ* ∧ +∞ = +∞) → +∞ ≤ +∞)
4744, 45, 46mp2an 692 . . . . . . . 8 +∞ ≤ +∞
4847a1i 11 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ≤ +∞)
4914adantr 480 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝑈 ∈ V)
508adantr 480 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝐹:𝑈⟶(0[,]+∞))
51 rnresss 6036 . . . . . . . . . . 11 ran (𝐹𝐴) ⊆ ran 𝐹
5251sseli 3990 . . . . . . . . . 10 (+∞ ∈ ran (𝐹𝐴) → +∞ ∈ ran 𝐹)
5352adantl 481 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ∈ ran 𝐹)
5449, 50, 53sge0pnfval 46328 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) = +∞)
55 xrge0neqmnf 13488 . . . . . . . . . . . . . 14 ((Σ^‘(𝐹𝐵)) ∈ (0[,]+∞) → (Σ^‘(𝐹𝐵)) ≠ -∞)
5640, 55syl 17 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝐹𝐵)) ≠ -∞)
57 xaddpnf2 13265 . . . . . . . . . . . . 13 (((Σ^‘(𝐹𝐵)) ∈ ℝ* ∧ (Σ^‘(𝐹𝐵)) ≠ -∞) → (+∞ +𝑒^‘(𝐹𝐵))) = +∞)
5841, 56, 57syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (+∞ +𝑒^‘(𝐹𝐵))) = +∞)
5958eqcomd 2740 . . . . . . . . . . 11 (𝜑 → +∞ = (+∞ +𝑒^‘(𝐹𝐵))))
6059adantr 480 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ = (+∞ +𝑒^‘(𝐹𝐵))))
611adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → 𝐴𝑉)
6233adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
63 simpr 484 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → +∞ ∈ ran (𝐹𝐴))
6461, 62, 63sge0pnfval 46328 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) = +∞)
6564oveq1d 7445 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (+∞ +𝑒^‘(𝐹𝐵))))
6660, 54, 653eqtr4d 2784 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
6766, 54eqtr3d 2776 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = +∞)
6854, 67breq12d 5160 . . . . . . 7 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → ((Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ↔ +∞ ≤ +∞))
6948, 68mpbird 257 . . . . . 6 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
7047a1i 11 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ≤ +∞)
7114adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝑈 ∈ V)
728adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
73 rnresss 6036 . . . . . . . . . . . . 13 ran (𝐹𝐵) ⊆ ran 𝐹
7473sseli 3990 . . . . . . . . . . . 12 (+∞ ∈ ran (𝐹𝐵) → +∞ ∈ ran 𝐹)
7574adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ∈ ran 𝐹)
7671, 72, 75sge0pnfval 46328 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) = +∞)
773adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → 𝐵𝑊)
7839adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
79 simpr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → +∞ ∈ ran (𝐹𝐵))
8077, 78, 79sge0pnfval 46328 . . . . . . . . . . . 12 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = +∞)
8180oveq2d 7446 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = ((Σ^‘(𝐹𝐴)) +𝑒 +∞))
821, 33sge0cl 46336 . . . . . . . . . . . . . 14 (𝜑 → (Σ^‘(𝐹𝐴)) ∈ (0[,]+∞))
83 xrge0neqmnf 13488 . . . . . . . . . . . . . 14 ((Σ^‘(𝐹𝐴)) ∈ (0[,]+∞) → (Σ^‘(𝐹𝐴)) ≠ -∞)
8482, 83syl 17 . . . . . . . . . . . . 13 (𝜑 → (Σ^‘(𝐹𝐴)) ≠ -∞)
85 xaddpnf1 13264 . . . . . . . . . . . . 13 (((Σ^‘(𝐹𝐴)) ∈ ℝ* ∧ (Σ^‘(𝐹𝐴)) ≠ -∞) → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8634, 84, 85syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8786adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒 +∞) = +∞)
8881, 87eqtrd 2774 . . . . . . . . . 10 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = +∞)
8976, 88breq12d 5160 . . . . . . . . 9 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → ((Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ↔ +∞ ≤ +∞))
9070, 89mpbird 257 . . . . . . . 8 ((𝜑 ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
9190adantlr 715 . . . . . . 7 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
92 simpr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)))
93 vex 3481 . . . . . . . . . . . . 13 𝑧 ∈ V
94 eqid 2734 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))
9594elrnmpt 5971 . . . . . . . . . . . . 13 (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦)))
9693, 95ax-mp 5 . . . . . . . . . . . 12 (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦))
9792, 96sylib 218 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦))
98 simp3 1137 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑧 = Σ𝑦𝑥 (𝐹𝑦))
99 inss1 4244 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝑥𝐴)
100 inss2 4245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐴) ⊆ 𝐴
10199, 100sstri 4004 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ 𝐴
102 inss2 4245 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝑥𝐵)
103 inss2 4245 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐵) ⊆ 𝐵
104102, 103sstri 4004 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ 𝐵
105101, 104ssini 4247 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝐴𝐵)
106105a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ (𝐴𝐵))
107106, 6sseqtrd 4035 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ ∅)
108 ss0 4407 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥𝐴) ∩ (𝑥𝐵)) ⊆ ∅ → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
110109ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥𝐴) ∩ (𝑥𝐵)) = ∅)
111 indi 4289 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∩ (𝐴𝐵)) = ((𝑥𝐴) ∪ (𝑥𝐵))
112111eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵))
113112a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ((𝑥𝐴) ∪ (𝑥𝐵)) = (𝑥 ∩ (𝐴𝐵)))
1145eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐴𝐵) = 𝑈
115114ineq2i 4224 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∩ (𝐴𝐵)) = (𝑥𝑈)
116115a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ (𝐴𝐵)) = (𝑥𝑈))
117 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈)
118 elpwi 4611 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ 𝒫 𝑈𝑥𝑈)
119117, 118syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥𝑈)
120 dfss2 3980 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥𝑈 ↔ (𝑥𝑈) = 𝑥)
121120biimpi 216 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝑈 → (𝑥𝑈) = 𝑥)
122119, 121syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝑈) = 𝑥)
123113, 116, 1223eqtrrd 2779 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
124123adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥𝐴) ∪ (𝑥𝐵)))
125 elinel2 4211 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin)
126125adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin)
127 rge0ssre 13492 . . . . . . . . . . . . . . . . . . . . 21 (0[,)+∞) ⊆ ℝ
1288ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,]+∞))
129 pm4.56 990 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ↔ ¬ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
130129biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
131 elun 4162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (+∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) ↔ (+∞ ∈ ran (𝐹𝐴) ∨ +∞ ∈ ran (𝐹𝐵)))
132130, 131sylnibr 329 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((¬ +∞ ∈ ran (𝐹𝐴) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)))
133132adantll 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ (ran (𝐹𝐴) ∪ ran (𝐹𝐵)))
134 rnresun 45122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ran (𝐹 ↾ (𝐴𝐵)) = (ran (𝐹𝐴) ∪ ran (𝐹𝐵))
135134eqcomi 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran (𝐹 ↾ (𝐴𝐵))
136135a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran (𝐹 ↾ (𝐴𝐵)))
137114reseq2i 5996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 ↾ (𝐴𝐵)) = (𝐹𝑈)
138137rneqi 5950 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ran (𝐹 ↾ (𝐴𝐵)) = ran (𝐹𝑈)
139138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran (𝐹 ↾ (𝐴𝐵)) = ran (𝐹𝑈))
140 ffn 6736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹:𝑈⟶(0[,]+∞) → 𝐹 Fn 𝑈)
141 fnresdm 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹 Fn 𝑈 → (𝐹𝑈) = 𝐹)
1428, 140, 1413syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐹𝑈) = 𝐹)
143142rneqd 5951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ran (𝐹𝑈) = ran 𝐹)
144136, 139, 1433eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran 𝐹)
145144ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (ran (𝐹𝐴) ∪ ran (𝐹𝐵)) = ran 𝐹)
146133, 145neleqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ ran 𝐹)
147128, 146fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐹:𝑈⟶(0[,)+∞))
148147ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝐹:𝑈⟶(0[,)+∞))
149119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑥𝑈)
150 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑥)
151149, 150sseldd 3995 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦𝑥) → 𝑦𝑈)
152151adantll 714 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → 𝑦𝑈)
153148, 152ffvelcdmd 7104 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ (0[,)+∞))
154127, 153sselid 3992 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℝ)
155154recnd 11286 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦𝑥) → (𝐹𝑦) ∈ ℂ)
156110, 124, 126, 155fsumsplit 15773 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
157 infi 9299 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ Fin → (𝑥𝐴) ∈ Fin)
158125, 157syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐴) ∈ Fin)
159158adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ∈ Fin)
160 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
161 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝑥𝐴) → 𝑦𝑥)
162161adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → 𝑦𝑥)
163160, 162, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → (𝐹𝑦) ∈ ℝ)
164159, 163fsumrecl 15766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ)
165 infi 9299 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ Fin → (𝑥𝐵) ∈ Fin)
166125, 165syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥𝐵) ∈ Fin)
167166adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ∈ Fin)
168 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)))
169 elinel1 4210 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ (𝑥𝐵) → 𝑦𝑥)
170169adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → 𝑦𝑥)
171168, 170, 154syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → (𝐹𝑦) ∈ ℝ)
172167, 171fsumrecl 15766 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ)
173 rexadd 13270 . . . . . . . . . . . . . . . . . . . 20 ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
174164, 172, 173syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
175174eqcomd 2740 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) + Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
176156, 175eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) = (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) +𝑒 Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦)))
177 ressxr 11302 . . . . . . . . . . . . . . . . . . . 20 ℝ ⊆ ℝ*
178177, 164sselid 3992 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ*)
179177, 172sselid 3992 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ*)
1801adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → 𝐴𝑉)
18133adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
182 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → ¬ +∞ ∈ ran (𝐹𝐴))
183181, 182fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (𝐹𝐴):𝐴⟶(0[,)+∞))
184180, 183sge0reval 46327 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
185184eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) = (Σ^‘(𝐹𝐴)))
18634adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^‘(𝐹𝐴)) ∈ ℝ*)
187185, 186eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
188187adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ*)
1893adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝐵𝑊)
19039adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
191 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ¬ +∞ ∈ ran (𝐹𝐵))
192190, 191fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝐹𝐵):𝐵⟶(0[,)+∞))
193189, 192sge0reval 46327 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
194193eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) = (Σ^‘(𝐹𝐵)))
19541adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) ∈ ℝ*)
196194, 195eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
197196adantlr 715 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)
198188, 197jca 511 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
199198adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*))
200178, 179, 199jca31 514 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ∈ ℝ* ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ∈ ℝ*) ∧ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∈ ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ) ∈ ℝ*)))
201180adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐴𝑉)
202181adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐴):𝐴⟶(0[,]+∞))
203182adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹𝐴))
204202, 203fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐴):𝐴⟶(0[,)+∞))
205100a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ⊆ 𝐴)
206158adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐴) ∈ Fin)
207201, 204, 205, 206fsumlesge0 46332 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ≤ (Σ^‘(𝐹𝐴)))
208100sseli 3990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑥𝐴) → 𝑦𝐴)
209 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝑥𝐴) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
211210adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐴)) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
212211sumeq2dv 15734 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦))
213184adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
214212, 213breq12d 5160 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)((𝐹𝐴)‘𝑦) ≤ (Σ^‘(𝐹𝐴)) ↔ Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < )))
215207, 214mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
216215adantlr 715 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
217189adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐵𝑊)
218190adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐵):𝐵⟶(0[,]+∞))
219191adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈ ran (𝐹𝐵))
220218, 219fge0iccico 46325 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹𝐵):𝐵⟶(0[,)+∞))
221103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ⊆ 𝐵)
222166adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥𝐵) ∈ Fin)
223217, 220, 221, 222fsumlesge0 46332 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) ≤ (Σ^‘(𝐹𝐵)))
224103sseli 3990 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (𝑥𝐵) → 𝑦𝐵)
225 fvres 6925 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝑥𝐵) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
227226adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥𝐵)) → ((𝐹𝐵)‘𝑦) = (𝐹𝑦))
228227sumeq2dv 15734 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦))
229193adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
230228, 229breq12d 5160 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐵)((𝐹𝐵)‘𝑦) ≤ (Σ^‘(𝐹𝐵)) ↔ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
231223, 230mpbid 232 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
232231adantllr 719 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
233216, 232jca 511 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥𝐴)(𝐹𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) ∧ Σ𝑦 ∈ (𝑥𝐵)(𝐹𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
234 xle2add 13297 . . . . . . . . . . . . . . . . . 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 5169 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦𝑥 (𝐹𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
2372363adant3 1131 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → Σ𝑦𝑥 (𝐹𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
23898, 237eqbrtrd 5169 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦𝑥 (𝐹𝑦)) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
2392383exp 1118 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑧 = Σ𝑦𝑥 (𝐹𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))))
240239rexlimdv 3150 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦𝑥 (𝐹𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))))
241240adantr 480 . . . . . . . . . . 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 3143 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
244147sge0rnre 46319 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ)
245177a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ℝ ⊆ ℝ*)
246244, 245sstrd 4005 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)) ⊆ ℝ*)
247188, 197xaddcld 13339 . . . . . . . . . 10 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )) ∈ ℝ*)
248 supxrleub 13364 . . . . . . . . . 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 257 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
25114ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → 𝑈 ∈ V)
252251, 147sge0reval 46327 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦𝑥 (𝐹𝑦)), ℝ*, < ))
253184adantr 480 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ))
254193adantlr 715 . . . . . . . . 9 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^‘(𝐹𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < ))
255253, 254oveq12d 7448 . . . . . . . 8 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) = (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏𝑎 ((𝐹𝐴)‘𝑏)), ℝ*, < ) +𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑𝑐 ((𝐹𝐵)‘𝑑)), ℝ*, < )))
256250, 252, 2553brtr4d 5179 . . . . . . 7 (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) ∧ ¬ +∞ ∈ ran (𝐹𝐵)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
25791, 256pm2.61dan 813 . . . . . 6 ((𝜑 ∧ ¬ +∞ ∈ ran (𝐹𝐴)) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
25869, 257pm2.61dan 813 . . . . 5 (𝜑 → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
259258adantr 480 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) ≤ ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
260 pnfge 13169 . . . . . . 7 (((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ∈ ℝ* → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
26142, 260syl 17 . . . . . 6 (𝜑 → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
262261adantr 480 . . . . 5 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ +∞)
263 id 22 . . . . . . 7 ((Σ^𝐹) = +∞ → (Σ^𝐹) = +∞)
264263eqcomd 2740 . . . . . 6 ((Σ^𝐹) = +∞ → +∞ = (Σ^𝐹))
265264adantl 481 . . . . 5 ((𝜑 ∧ (Σ^𝐹) = +∞) → +∞ = (Σ^𝐹))
266262, 265breqtrd 5173 . . . 4 ((𝜑 ∧ (Σ^𝐹) = +∞) → ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))) ≤ (Σ^𝐹))
26729, 43, 259, 266xrletrid 13193 . . 3 ((𝜑 ∧ (Σ^𝐹) = +∞) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
26822, 27, 267syl2anc 584 . 2 ((𝜑 ∧ ¬ (Σ^𝐹) ∈ ℝ) → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
26921, 268pm2.61dan 813 1 (𝜑 → (Σ^𝐹) = ((Σ^‘(𝐹𝐴)) +𝑒^‘(𝐹𝐵))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cun 3960  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604   class class class wbr 5147  cmpt 5230  ran crn 5689  cres 5690   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  Fincfn 8983  supcsup 9477  cr 11151  0cc0 11152   + caddc 11155  +∞cpnf 11289  -∞cmnf 11290  *cxr 11291   < clt 11292  cle 11293   +𝑒 cxad 13149  [,)cico 13385  [,]cicc 13386  Σcsu 15718  Σ^csumge0 46317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-xadd 13152  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-sumge0 46318
This theorem is referenced by:  sge0splitmpt  46366
  Copyright terms: Public domain W3C validator