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

Theorem sge0iunmpt 41107
Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
sge0iunmpt.a (𝜑𝐴𝑉)
sge0iunmpt.b ((𝜑𝑥𝐴) → 𝐵𝑊)
sge0iunmpt.dj (𝜑Disj 𝑥𝐴 𝐵)
sge0iunmpt.c ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
Assertion
Ref Expression
sge0iunmpt (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Distinct variable groups:   𝐴,𝑘,𝑥   𝐵,𝑘   𝑥,𝐶   𝑥,𝑊   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)   𝑉(𝑥,𝑘)   𝑊(𝑘)

Proof of Theorem sge0iunmpt
Dummy variables 𝑗 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1980 . . . 4 𝑥𝜑
2 nfcv 2890 . . . . . 6 𝑥Σ^
3 nfiu1 4690 . . . . . . 7 𝑥 𝑥𝐴 𝐵
4 nfcv 2890 . . . . . . 7 𝑥𝐶
53, 4nfmpt 4886 . . . . . 6 𝑥(𝑘 𝑥𝐴 𝐵𝐶)
62, 5nffv 6347 . . . . 5 𝑥^‘(𝑘 𝑥𝐴 𝐵𝐶))
7 nfmpt1 4887 . . . . . 6 𝑥(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
82, 7nffv 6347 . . . . 5 𝑥^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
96, 8nfeq 2902 . . . 4 𝑥^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
10 sge0iunmpt.a . . . . . . . . . 10 (𝜑𝐴𝑉)
11 sge0iunmpt.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵𝑊)
1211ralrimiva 3092 . . . . . . . . . 10 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
13 iunexg 7296 . . . . . . . . . 10 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
1410, 12, 13syl2anc 696 . . . . . . . . 9 (𝜑 𝑥𝐴 𝐵 ∈ V)
15 eliun 4664 . . . . . . . . . . . . 13 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
1615biimpi 206 . . . . . . . . . . . 12 (𝑘 𝑥𝐴 𝐵 → ∃𝑥𝐴 𝑘𝐵)
1716adantl 473 . . . . . . . . . . 11 ((𝜑𝑘 𝑥𝐴 𝐵) → ∃𝑥𝐴 𝑘𝐵)
18 nfcv 2890 . . . . . . . . . . . . . 14 𝑥𝑘
1918, 3nfel 2903 . . . . . . . . . . . . 13 𝑥 𝑘 𝑥𝐴 𝐵
201, 19nfan 1965 . . . . . . . . . . . 12 𝑥(𝜑𝑘 𝑥𝐴 𝐵)
214nfel1 2905 . . . . . . . . . . . 12 𝑥 𝐶 ∈ (0[,]+∞)
22 sge0iunmpt.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
23223exp 1112 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
2423adantr 472 . . . . . . . . . . . 12 ((𝜑𝑘 𝑥𝐴 𝐵) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
2520, 21, 24rexlimd 3152 . . . . . . . . . . 11 ((𝜑𝑘 𝑥𝐴 𝐵) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,]+∞)))
2617, 25mpd 15 . . . . . . . . . 10 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
27 eqid 2748 . . . . . . . . . 10 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶)
2826, 27fmptd 6536 . . . . . . . . 9 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
2914, 28sge0xrcl 41074 . . . . . . . 8 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
30293ad2ant1 1125 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
31 id 22 . . . . . . . . . . 11 ((Σ^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘𝐵𝐶)) = +∞)
3231eqcomd 2754 . . . . . . . . . 10 ((Σ^‘(𝑘𝐵𝐶)) = +∞ → +∞ = (Σ^‘(𝑘𝐵𝐶)))
3332adantl 473 . . . . . . . . 9 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ = (Σ^‘(𝑘𝐵𝐶)))
34333adant1 1122 . . . . . . . 8 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ = (Σ^‘(𝑘𝐵𝐶)))
3514adantr 472 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴 𝐵 ∈ V)
3626adantlr 753 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
37 ssiun2 4703 . . . . . . . . . . 11 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
3837adantl 473 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐵 𝑥𝐴 𝐵)
3935, 36, 38sge0lessmpt 41088 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
40393adant3 1124 . . . . . . . 8 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
4134, 40eqbrtrd 4814 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
4230, 41xrgepnfd 40014 . . . . . 6 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = +∞)
43103ad2ant1 1125 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → 𝐴𝑉)
44 nfv 1980 . . . . . . . . . . . . 13 𝑥(𝜑𝑦𝐴)
45 nfcsb1v 3678 . . . . . . . . . . . . . 14 𝑥𝑦 / 𝑥𝐵
46 nfcsb1v 3678 . . . . . . . . . . . . . 14 𝑥𝑦 / 𝑥𝑊
4745, 46nfel 2903 . . . . . . . . . . . . 13 𝑥𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊
4844, 47nfim 1962 . . . . . . . . . . . 12 𝑥((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
49 eleq1 2815 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5049anbi2d 742 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
51 csbeq1a 3671 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
52 csbeq1a 3671 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝑊 = 𝑦 / 𝑥𝑊)
5351, 52eleq12d 2821 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐵𝑊𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊))
5450, 53imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝐵𝑊) ↔ ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)))
5548, 54, 11chvar 2395 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
5655adantlr 753 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
5745, 4nfmpt 4886 . . . . . . . . . . . . . 14 𝑥(𝑘𝑦 / 𝑥𝐵𝐶)
58 nfcv 2890 . . . . . . . . . . . . . 14 𝑥(0[,]+∞)
5957, 45, 58nff 6190 . . . . . . . . . . . . 13 𝑥(𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞)
6044, 59nfim 1962 . . . . . . . . . . . 12 𝑥((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6151mpteq1d 4878 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑘𝐵𝐶) = (𝑘𝑦 / 𝑥𝐵𝐶))
6261, 51feq12d 6182 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑘𝐵𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞)))
6350, 62imbi12d 333 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))))
6423imp31 447 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
65 eqid 2748 . . . . . . . . . . . . 13 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
6664, 65fmptd 6536 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
6760, 63, 66chvar 2395 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6867adantlr 753 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6956, 68sge0cl 41070 . . . . . . . . 9 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)) ∈ (0[,]+∞))
70 nfcv 2890 . . . . . . . . . 10 𝑦^‘(𝑘𝐵𝐶))
712, 57nffv 6347 . . . . . . . . . 10 𝑥^‘(𝑘𝑦 / 𝑥𝐵𝐶))
7261fveq2d 6344 . . . . . . . . . 10 (𝑥 = 𝑦 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)))
7370, 71, 72cbvmpt 4889 . . . . . . . . 9 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑦𝐴 ↦ (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)))
7469, 73fmptd 6536 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
75743adant3 1124 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
76 id 22 . . . . . . . . . . 11 (𝑥𝐴𝑥𝐴)
77 fvexd 6352 . . . . . . . . . . 11 (𝑥𝐴 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
78 eqid 2748 . . . . . . . . . . . 12 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
7978elrnmpt1 5517 . . . . . . . . . . 11 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8076, 77, 79syl2anc 696 . . . . . . . . . 10 (𝑥𝐴 → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8180adantr 472 . . . . . . . . 9 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8233, 81eqeltrd 2827 . . . . . . . 8 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
83823adant1 1122 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8443, 75, 83sge0pnfval 41062 . . . . . 6 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = +∞)
8542, 84eqtr4d 2785 . . . . 5 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
86853exp 1112 . . . 4 (𝜑 → (𝑥𝐴 → ((Σ^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))))
871, 9, 86rexlimd 3152 . . 3 (𝜑 → (∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
8887imp 444 . 2 ((𝜑 ∧ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
89 simpl 474 . . 3 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → 𝜑)
90 ralnex 3118 . . . . 5 (∀𝑥𝐴 ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞)
91 df-ne 2921 . . . . . . 7 ((Σ^‘(𝑘𝐵𝐶)) ≠ +∞ ↔ ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞)
9291bicomi 214 . . . . . 6 (¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ (Σ^‘(𝑘𝐵𝐶)) ≠ +∞)
9392ralbii 3106 . . . . 5 (∀𝑥𝐴 ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9490, 93sylbb1 227 . . . 4 (¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞ → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9594adantl 473 . . 3 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9610adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝐴𝑉)
97 nfcv 2890 . . . . . . . . 9 𝑥𝑊
9845, 97nfel 2903 . . . . . . . 8 𝑥𝑦 / 𝑥𝐵𝑊
9944, 98nfim 1962 . . . . . . 7 𝑥((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
10051eleq1d 2812 . . . . . . . 8 (𝑥 = 𝑦 → (𝐵𝑊𝑦 / 𝑥𝐵𝑊))
10150, 100imbi12d 333 . . . . . . 7 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝐵𝑊) ↔ ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)))
10299, 101, 11chvar 2395 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
103102adantlr 753 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
104 sge0iunmpt.dj . . . . . . 7 (𝜑Disj 𝑥𝐴 𝐵)
105 nfcv 2890 . . . . . . . 8 𝑦𝐵
106105, 45, 51cbvdisj 4770 . . . . . . 7 (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
107104, 106sylib 208 . . . . . 6 (𝜑Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
108107adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
109 nfv 1980 . . . . . . . 8 𝑘(𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵)
110 nfcsb1v 3678 . . . . . . . . 9 𝑘𝑗 / 𝑘𝐶
111110nfel1 2905 . . . . . . . 8 𝑘𝑗 / 𝑘𝐶 ∈ (0[,]+∞)
112109, 111nfim 1962 . . . . . . 7 𝑘((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
113 eleq1 2815 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑘𝑦 / 𝑥𝐵𝑗𝑦 / 𝑥𝐵))
1141133anbi3d 1542 . . . . . . . 8 (𝑘 = 𝑗 → ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) ↔ (𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵)))
115 csbeq1a 3671 . . . . . . . . 9 (𝑘 = 𝑗𝐶 = 𝑗 / 𝑘𝐶)
116115eleq1d 2812 . . . . . . . 8 (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔ 𝑗 / 𝑘𝐶 ∈ (0[,]+∞)))
117114, 116imbi12d 333 . . . . . . 7 (𝑘 = 𝑗 → (((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
118 nfv 1980 . . . . . . . . . 10 𝑥 𝑦𝐴
11918, 45nfel 2903 . . . . . . . . . 10 𝑥 𝑘𝑦 / 𝑥𝐵
1201, 118, 119nf3an 1968 . . . . . . . . 9 𝑥(𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵)
121120, 21nfim 1962 . . . . . . . 8 𝑥((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
12251eleq2d 2813 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑘𝐵𝑘𝑦 / 𝑥𝐵))
12349, 1223anbi23d 1539 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵)))
124123imbi1d 330 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))))
125121, 124, 22chvar 2395 . . . . . . 7 ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
126112, 117, 125chvar 2395 . . . . . 6 ((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
1271263adant1r 1168 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
128 simpr 479 . . . . . . . . 9 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → 𝑦𝐴)
129 simpl 474 . . . . . . . . 9 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
130 simpl 474 . . . . . . . . . 10 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝑦𝐴)
131 simpr 479 . . . . . . . . . 10 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
132 nfcv 2890 . . . . . . . . . . . . . 14 𝑥𝑗 / 𝑘𝐶
13345, 132nfmpt 4886 . . . . . . . . . . . . 13 𝑥(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
1342, 133nffv 6347 . . . . . . . . . . . 12 𝑥^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
135 nfcv 2890 . . . . . . . . . . . 12 𝑥+∞
136134, 135nfne 3020 . . . . . . . . . . 11 𝑥^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞
137 nfcv 2890 . . . . . . . . . . . . . . . 16 𝑗𝐶
138137, 110, 115cbvmpt 4889 . . . . . . . . . . . . . . 15 (𝑘𝑦 / 𝑥𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
139138a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑘𝑦 / 𝑥𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
14061, 139eqtrd 2782 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑘𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
141140fveq2d 6344 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
142141neeq1d 2979 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((Σ^‘(𝑘𝐵𝐶)) ≠ +∞ ↔ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞))
143136, 142rspc 3431 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞))
144130, 131, 143sylc 65 . . . . . . . . 9 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞)
145128, 129, 144syl2anc 696 . . . . . . . 8 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞)
146145neneqd 2925 . . . . . . 7 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞)
147146adantll 752 . . . . . 6 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞)
1481263expa 1111 . . . . . . . . 9 (((𝜑𝑦𝐴) ∧ 𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
149 eqid 2748 . . . . . . . . 9 (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
150148, 149fmptd 6536 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
151150adantlr 753 . . . . . . 7 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
152103, 151sge0repnf 41075 . . . . . 6 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → ((Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ ↔ ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞))
153147, 152mpbird 247 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ)
154137, 110, 115cbvmpt 4889 . . . . . . . . 9 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑗 𝑥𝐴 𝐵𝑗 / 𝑘𝐶)
155105, 45, 51cbviun 4697 . . . . . . . . . 10 𝑥𝐴 𝐵 = 𝑦𝐴 𝑦 / 𝑥𝐵
156155mpteq1i 4879 . . . . . . . . 9 (𝑗 𝑥𝐴 𝐵𝑗 / 𝑘𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
157154, 156eqtri 2770 . . . . . . . 8 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
158157fveq2i 6343 . . . . . . 7 ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
159158, 29syl5eqelr 2832 . . . . . 6 (𝜑 → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ*)
160159adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ*)
16170, 134, 141cbvmpt 4889 . . . . . . . 8 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
162161fveq2i 6343 . . . . . . 7 ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))))
16311, 66sge0cl 41070 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
164163, 78fmptd 6536 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
16510, 164sge0xrcl 41074 . . . . . . 7 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
166162, 165syl5eqelr 2832 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))) ∈ ℝ*)
167166adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))) ∈ ℝ*)
168 eliun 4664 . . . . . . . . . 10 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵 ↔ ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
169168biimpi 206 . . . . . . . . 9 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵 → ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
170169adantl 473 . . . . . . . 8 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
171 nfv 1980 . . . . . . . . . 10 𝑦𝜑
172 nfcv 2890 . . . . . . . . . . 11 𝑦𝑗
173 nfiu1 4690 . . . . . . . . . . 11 𝑦 𝑦𝐴 𝑦 / 𝑥𝐵
174172, 173nfel 2903 . . . . . . . . . 10 𝑦 𝑗 𝑦𝐴 𝑦 / 𝑥𝐵
175171, 174nfan 1965 . . . . . . . . 9 𝑦(𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵)
176 nfv 1980 . . . . . . . . 9 𝑦𝑗 / 𝑘𝐶 ∈ (0[,]+∞)
177148exp31 631 . . . . . . . . . 10 (𝜑 → (𝑦𝐴 → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
178177adantr 472 . . . . . . . . 9 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → (𝑦𝐴 → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
179175, 176, 178rexlimd 3152 . . . . . . . 8 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → (∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞)))
180170, 179mpd 15 . . . . . . 7 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
181 eqid 2748 . . . . . . 7 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
182180, 181fmptd 6536 . . . . . 6 (𝜑 → (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶): 𝑦𝐴 𝑦 / 𝑥𝐵⟶(0[,]+∞))
183182adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶): 𝑦𝐴 𝑦 / 𝑥𝐵⟶(0[,]+∞))
184155, 14syl5eqelr 2832 . . . . . 6 (𝜑 𝑦𝐴 𝑦 / 𝑥𝐵 ∈ V)
185184adantr 472 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝑦𝐴 𝑦 / 𝑥𝐵 ∈ V)
18696, 103, 108, 127, 153, 160, 167, 183, 185sge0iunmptlemre 41104 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))))
187158a1i 11 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
188162a1i 11 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))))
189186, 187, 1883eqtr4d 2792 . . 3 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
19089, 95, 189syl2anc 696 . 2 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
19188, 190pm2.61dan 867 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  w3a 1072   = wceq 1620  wcel 2127  wne 2920  wral 3038  wrex 3039  Vcvv 3328  csb 3662  wss 3703   ciun 4660  Disj wdisj 4760   class class class wbr 4792  cmpt 4869  ran crn 5255  wf 6033  cfv 6037  (class class class)co 6801  cr 10098  0cc0 10099  +∞cpnf 10234  *cxr 10236  cle 10238  [,]cicc 12342  Σ^csumge0 41051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-inf2 8699  ax-ac2 9448  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-pre-sup 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-fal 1626  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-disj 4761  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-se 5214  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-isom 6046  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8501  df-oi 8568  df-card 8926  df-acn 8929  df-ac 9100  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-div 10848  df-nn 11184  df-2 11242  df-3 11243  df-n0 11456  df-z 11541  df-uz 11851  df-rp 11997  df-xadd 12111  df-ico 12345  df-icc 12346  df-fz 12491  df-fzo 12631  df-seq 12967  df-exp 13026  df-hash 13283  df-cj 14009  df-re 14010  df-im 14011  df-sqrt 14145  df-abs 14146  df-clim 14389  df-sum 14587  df-sumge0 41052
This theorem is referenced by:  sge0iun  41108  sge0xp  41118
  Copyright terms: Public domain W3C validator