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 44005
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 1915 . . . 4 𝑥𝜑
2 nfcv 2905 . . . . . 6 𝑥Σ^
3 nfiu1 4965 . . . . . . 7 𝑥 𝑥𝐴 𝐵
4 nfcv 2905 . . . . . . 7 𝑥𝐶
53, 4nfmpt 5188 . . . . . 6 𝑥(𝑘 𝑥𝐴 𝐵𝐶)
62, 5nffv 6810 . . . . 5 𝑥^‘(𝑘 𝑥𝐴 𝐵𝐶))
7 nfmpt1 5189 . . . . . 6 𝑥(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
82, 7nffv 6810 . . . . 5 𝑥^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
96, 8nfeq 2918 . . . 4 𝑥^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
10 sge0iunmpt.a . . . . . . . . . 10 (𝜑𝐴𝑉)
11 sge0iunmpt.b . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝐵𝑊)
1211ralrimiva 3140 . . . . . . . . . 10 (𝜑 → ∀𝑥𝐴 𝐵𝑊)
13 iunexg 7834 . . . . . . . . . 10 ((𝐴𝑉 ∧ ∀𝑥𝐴 𝐵𝑊) → 𝑥𝐴 𝐵 ∈ V)
1410, 12, 13syl2anc 585 . . . . . . . . 9 (𝜑 𝑥𝐴 𝐵 ∈ V)
15 eliun 4935 . . . . . . . . . . . . 13 (𝑘 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑘𝐵)
1615biimpi 215 . . . . . . . . . . . 12 (𝑘 𝑥𝐴 𝐵 → ∃𝑥𝐴 𝑘𝐵)
1716adantl 483 . . . . . . . . . . 11 ((𝜑𝑘 𝑥𝐴 𝐵) → ∃𝑥𝐴 𝑘𝐵)
18 nfcv 2905 . . . . . . . . . . . . . 14 𝑥𝑘
1918, 3nfel 2919 . . . . . . . . . . . . 13 𝑥 𝑘 𝑥𝐴 𝐵
201, 19nfan 1900 . . . . . . . . . . . 12 𝑥(𝜑𝑘 𝑥𝐴 𝐵)
214nfel1 2921 . . . . . . . . . . . 12 𝑥 𝐶 ∈ (0[,]+∞)
22 sge0iunmpt.c . . . . . . . . . . . . . 14 ((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
23223exp 1119 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
2423adantr 482 . . . . . . . . . . . 12 ((𝜑𝑘 𝑥𝐴 𝐵) → (𝑥𝐴 → (𝑘𝐵𝐶 ∈ (0[,]+∞))))
2520, 21, 24rexlimd 3246 . . . . . . . . . . 11 ((𝜑𝑘 𝑥𝐴 𝐵) → (∃𝑥𝐴 𝑘𝐵𝐶 ∈ (0[,]+∞)))
2617, 25mpd 15 . . . . . . . . . 10 ((𝜑𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
27 eqid 2736 . . . . . . . . . 10 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑘 𝑥𝐴 𝐵𝐶)
2826, 27fmptd 7016 . . . . . . . . 9 (𝜑 → (𝑘 𝑥𝐴 𝐵𝐶): 𝑥𝐴 𝐵⟶(0[,]+∞))
2914, 28sge0xrcl 43972 . . . . . . . 8 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
30293ad2ant1 1133 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) ∈ ℝ*)
31 id 22 . . . . . . . . . . 11 ((Σ^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘𝐵𝐶)) = +∞)
3231eqcomd 2742 . . . . . . . . . 10 ((Σ^‘(𝑘𝐵𝐶)) = +∞ → +∞ = (Σ^‘(𝑘𝐵𝐶)))
3332adantl 483 . . . . . . . . 9 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ = (Σ^‘(𝑘𝐵𝐶)))
34333adant1 1130 . . . . . . . 8 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ = (Σ^‘(𝑘𝐵𝐶)))
3514adantr 482 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝑥𝐴 𝐵 ∈ V)
3626adantlr 713 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑘 𝑥𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
37 ssiun2 4984 . . . . . . . . . . 11 (𝑥𝐴𝐵 𝑥𝐴 𝐵)
3837adantl 483 . . . . . . . . . 10 ((𝜑𝑥𝐴) → 𝐵 𝑥𝐴 𝐵)
3935, 36, 38sge0lessmpt 43986 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
40393adant3 1132 . . . . . . . 8 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘𝐵𝐶)) ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
4134, 40eqbrtrd 5103 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ≤ (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)))
4230, 41xrgepnfd 42917 . . . . . 6 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = +∞)
43103ad2ant1 1133 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → 𝐴𝑉)
44 nfv 1915 . . . . . . . . . . . . 13 𝑥(𝜑𝑦𝐴)
45 nfcsb1v 3862 . . . . . . . . . . . . . 14 𝑥𝑦 / 𝑥𝐵
46 nfcsb1v 3862 . . . . . . . . . . . . . 14 𝑥𝑦 / 𝑥𝑊
4745, 46nfel 2919 . . . . . . . . . . . . 13 𝑥𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊
4844, 47nfim 1897 . . . . . . . . . . . 12 𝑥((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
49 eleq1w 2819 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
5049anbi2d 630 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝜑𝑥𝐴) ↔ (𝜑𝑦𝐴)))
51 csbeq1a 3851 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
52 csbeq1a 3851 . . . . . . . . . . . . . 14 (𝑥 = 𝑦𝑊 = 𝑦 / 𝑥𝑊)
5351, 52eleq12d 2831 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐵𝑊𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊))
5450, 53imbi12d 346 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝐵𝑊) ↔ ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)))
5548, 54, 11chvarfv 2231 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
5655adantlr 713 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝐵𝑦 / 𝑥𝑊)
5745, 4nfmpt 5188 . . . . . . . . . . . . . 14 𝑥(𝑘𝑦 / 𝑥𝐵𝐶)
58 nfcv 2905 . . . . . . . . . . . . . 14 𝑥(0[,]+∞)
5957, 45, 58nff 6622 . . . . . . . . . . . . 13 𝑥(𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞)
6044, 59nfim 1897 . . . . . . . . . . . 12 𝑥((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6151mpteq1d 5176 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑘𝐵𝐶) = (𝑘𝑦 / 𝑥𝐵𝐶))
6261, 51feq12d 6614 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → ((𝑘𝐵𝐶):𝐵⟶(0[,]+∞) ↔ (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞)))
6350, 62imbi12d 346 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞)) ↔ ((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))))
6423imp31 419 . . . . . . . . . . . . 13 (((𝜑𝑥𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
65 eqid 2736 . . . . . . . . . . . . 13 (𝑘𝐵𝐶) = (𝑘𝐵𝐶)
6664, 65fmptd 7016 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝑘𝐵𝐶):𝐵⟶(0[,]+∞))
6760, 63, 66chvarfv 2231 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6867adantlr 713 . . . . . . . . . 10 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → (𝑘𝑦 / 𝑥𝐵𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
6956, 68sge0cl 43968 . . . . . . . . 9 (((𝜑𝑥𝐴) ∧ 𝑦𝐴) → (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)) ∈ (0[,]+∞))
70 nfcv 2905 . . . . . . . . . 10 𝑦^‘(𝑘𝐵𝐶))
712, 57nffv 6810 . . . . . . . . . 10 𝑥^‘(𝑘𝑦 / 𝑥𝐵𝐶))
7261fveq2d 6804 . . . . . . . . . 10 (𝑥 = 𝑦 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)))
7370, 71, 72cbvmpt 5192 . . . . . . . . 9 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑦𝐴 ↦ (Σ^‘(𝑘𝑦 / 𝑥𝐵𝐶)))
7469, 73fmptd 7016 . . . . . . . 8 ((𝜑𝑥𝐴) → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
75743adant3 1132 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
76 id 22 . . . . . . . . . . 11 (𝑥𝐴𝑥𝐴)
77 fvexd 6815 . . . . . . . . . . 11 (𝑥𝐴 → (Σ^‘(𝑘𝐵𝐶)) ∈ V)
78 eqid 2736 . . . . . . . . . . . 12 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))
7978elrnmpt1 5875 . . . . . . . . . . 11 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) ∈ V) → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8076, 77, 79syl2anc 585 . . . . . . . . . 10 (𝑥𝐴 → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8180adantr 482 . . . . . . . . 9 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘𝐵𝐶)) ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8233, 81eqeltrd 2837 . . . . . . . 8 ((𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
83823adant1 1130 . . . . . . 7 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → +∞ ∈ ran (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))
8443, 75, 83sge0pnfval 43960 . . . . . 6 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = +∞)
8542, 84eqtr4d 2779 . . . . 5 ((𝜑𝑥𝐴 ∧ (Σ^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
86853exp 1119 . . . 4 (𝜑 → (𝑥𝐴 → ((Σ^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))))
871, 9, 86rexlimd 3246 . . 3 (𝜑 → (∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞ → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))))))
8887imp 408 . 2 ((𝜑 ∧ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
89 simpl 484 . . 3 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → 𝜑)
90 ralnex 3073 . . . . 5 (∀𝑥𝐴 ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞)
91 df-ne 2942 . . . . . . 7 ((Σ^‘(𝑘𝐵𝐶)) ≠ +∞ ↔ ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞)
9291bicomi 223 . . . . . 6 (¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ (Σ^‘(𝑘𝐵𝐶)) ≠ +∞)
9392ralbii 3093 . . . . 5 (∀𝑥𝐴 ¬ (Σ^‘(𝑘𝐵𝐶)) = +∞ ↔ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9490, 93sylbb1 237 . . . 4 (¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞ → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9594adantl 483 . . 3 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
9610adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝐴𝑉)
97 nfcv 2905 . . . . . . . . 9 𝑥𝑊
9845, 97nfel 2919 . . . . . . . 8 𝑥𝑦 / 𝑥𝐵𝑊
9944, 98nfim 1897 . . . . . . 7 𝑥((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
10051eleq1d 2821 . . . . . . . 8 (𝑥 = 𝑦 → (𝐵𝑊𝑦 / 𝑥𝐵𝑊))
10150, 100imbi12d 346 . . . . . . 7 (𝑥 = 𝑦 → (((𝜑𝑥𝐴) → 𝐵𝑊) ↔ ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)))
10299, 101, 11chvarfv 2231 . . . . . 6 ((𝜑𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
103102adantlr 713 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → 𝑦 / 𝑥𝐵𝑊)
104 sge0iunmpt.dj . . . . . . 7 (𝜑Disj 𝑥𝐴 𝐵)
105 nfcv 2905 . . . . . . . 8 𝑦𝐵
106105, 45, 51cbvdisj 5056 . . . . . . 7 (Disj 𝑥𝐴 𝐵Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
107104, 106sylib 217 . . . . . 6 (𝜑Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
108107adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → Disj 𝑦𝐴 𝑦 / 𝑥𝐵)
109 nfv 1915 . . . . . . . 8 𝑘(𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵)
110 nfcsb1v 3862 . . . . . . . . 9 𝑘𝑗 / 𝑘𝐶
111110nfel1 2921 . . . . . . . 8 𝑘𝑗 / 𝑘𝐶 ∈ (0[,]+∞)
112109, 111nfim 1897 . . . . . . 7 𝑘((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
113 eleq1w 2819 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑘𝑦 / 𝑥𝐵𝑗𝑦 / 𝑥𝐵))
1141133anbi3d 1442 . . . . . . . 8 (𝑘 = 𝑗 → ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) ↔ (𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵)))
115 csbeq1a 3851 . . . . . . . . 9 (𝑘 = 𝑗𝐶 = 𝑗 / 𝑘𝐶)
116115eleq1d 2821 . . . . . . . 8 (𝑘 = 𝑗 → (𝐶 ∈ (0[,]+∞) ↔ 𝑗 / 𝑘𝐶 ∈ (0[,]+∞)))
117114, 116imbi12d 346 . . . . . . 7 (𝑘 = 𝑗 → (((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
118 nfv 1915 . . . . . . . . . 10 𝑥 𝑦𝐴
11918, 45nfel 2919 . . . . . . . . . 10 𝑥 𝑘𝑦 / 𝑥𝐵
1201, 118, 119nf3an 1902 . . . . . . . . 9 𝑥(𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵)
121120, 21nfim 1897 . . . . . . . 8 𝑥((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
12251eleq2d 2822 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑘𝐵𝑘𝑦 / 𝑥𝐵))
12349, 1223anbi23d 1439 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝜑𝑥𝐴𝑘𝐵) ↔ (𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵)))
124123imbi1d 343 . . . . . . . 8 (𝑥 = 𝑦 → (((𝜑𝑥𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞)) ↔ ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))))
125121, 124, 22chvarfv 2231 . . . . . . 7 ((𝜑𝑦𝐴𝑘𝑦 / 𝑥𝐵) → 𝐶 ∈ (0[,]+∞))
126112, 117, 125chvarfv 2231 . . . . . 6 ((𝜑𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
1271263adant1r 1177 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
128 simpr 486 . . . . . . . . 9 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → 𝑦𝐴)
129 simpl 484 . . . . . . . . 9 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
130 simpl 484 . . . . . . . . . 10 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝑦𝐴)
131 simpr 486 . . . . . . . . . 10 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞)
132 nfcv 2905 . . . . . . . . . . . . . 14 𝑥𝑗 / 𝑘𝐶
13345, 132nfmpt 5188 . . . . . . . . . . . . 13 𝑥(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
1342, 133nffv 6810 . . . . . . . . . . . 12 𝑥^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
135 nfcv 2905 . . . . . . . . . . . 12 𝑥+∞
136134, 135nfne 3043 . . . . . . . . . . 11 𝑥^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞
137 nfcv 2905 . . . . . . . . . . . . . . . 16 𝑗𝐶
138137, 110, 115cbvmpt 5192 . . . . . . . . . . . . . . 15 (𝑘𝑦 / 𝑥𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
139138a1i 11 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑘𝑦 / 𝑥𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
14061, 139eqtrd 2776 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑘𝐵𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
141140fveq2d 6804 . . . . . . . . . . . 12 (𝑥 = 𝑦 → (Σ^‘(𝑘𝐵𝐶)) = (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
142141neeq1d 3001 . . . . . . . . . . 11 (𝑥 = 𝑦 → ((Σ^‘(𝑘𝐵𝐶)) ≠ +∞ ↔ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞))
143136, 142rspc 3554 . . . . . . . . . 10 (𝑦𝐴 → (∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞))
144130, 131, 143sylc 65 . . . . . . . . 9 ((𝑦𝐴 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞)
145128, 129, 144syl2anc 585 . . . . . . . 8 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ≠ +∞)
146145neneqd 2946 . . . . . . 7 ((∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞ ∧ 𝑦𝐴) → ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞)
147146adantll 712 . . . . . 6 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞)
1481263expa 1118 . . . . . . . . 9 (((𝜑𝑦𝐴) ∧ 𝑗𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
149 eqid 2736 . . . . . . . . 9 (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶) = (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
150148, 149fmptd 7016 . . . . . . . 8 ((𝜑𝑦𝐴) → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
151150adantlr 713 . . . . . . 7 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶):𝑦 / 𝑥𝐵⟶(0[,]+∞))
152103, 151sge0repnf 43973 . . . . . 6 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → ((Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ ↔ ¬ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = +∞))
153147, 152mpbird 258 . . . . 5 (((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) ∧ 𝑦𝐴) → (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ)
154137, 110, 115cbvmpt 5192 . . . . . . . . 9 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑗 𝑥𝐴 𝐵𝑗 / 𝑘𝐶)
155105, 45, 51cbviun 4973 . . . . . . . . . 10 𝑥𝐴 𝐵 = 𝑦𝐴 𝑦 / 𝑥𝐵
156155mpteq1i 5177 . . . . . . . . 9 (𝑗 𝑥𝐴 𝐵𝑗 / 𝑘𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
157154, 156eqtri 2764 . . . . . . . 8 (𝑘 𝑥𝐴 𝐵𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
158157fveq2i 6803 . . . . . . 7 ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))
159158, 29eqeltrrid 2842 . . . . . 6 (𝜑 → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ*)
160159adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) ∈ ℝ*)
16170, 134, 141cbvmpt 5192 . . . . . . . 8 (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))) = (𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
162161fveq2i 6803 . . . . . . 7 ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶))))
16311, 66sge0cl 43968 . . . . . . . . 9 ((𝜑𝑥𝐴) → (Σ^‘(𝑘𝐵𝐶)) ∈ (0[,]+∞))
164163, 78fmptd 7016 . . . . . . . 8 (𝜑 → (𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶))):𝐴⟶(0[,]+∞))
16510, 164sge0xrcl 43972 . . . . . . 7 (𝜑 → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) ∈ ℝ*)
166162, 165eqeltrrid 2842 . . . . . 6 (𝜑 → (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))) ∈ ℝ*)
167166adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))) ∈ ℝ*)
168 eliun 4935 . . . . . . . . . 10 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵 ↔ ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
169168biimpi 215 . . . . . . . . 9 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵 → ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
170169adantl 483 . . . . . . . 8 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → ∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵)
171 nfv 1915 . . . . . . . . . 10 𝑦𝜑
172 nfcv 2905 . . . . . . . . . . 11 𝑦𝑗
173 nfiu1 4965 . . . . . . . . . . 11 𝑦 𝑦𝐴 𝑦 / 𝑥𝐵
174172, 173nfel 2919 . . . . . . . . . 10 𝑦 𝑗 𝑦𝐴 𝑦 / 𝑥𝐵
175171, 174nfan 1900 . . . . . . . . 9 𝑦(𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵)
176 nfv 1915 . . . . . . . . 9 𝑦𝑗 / 𝑘𝐶 ∈ (0[,]+∞)
177148exp31 421 . . . . . . . . . 10 (𝜑 → (𝑦𝐴 → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
178177adantr 482 . . . . . . . . 9 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → (𝑦𝐴 → (𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞))))
179175, 176, 178rexlimd 3246 . . . . . . . 8 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → (∃𝑦𝐴 𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶 ∈ (0[,]+∞)))
180170, 179mpd 15 . . . . . . 7 ((𝜑𝑗 𝑦𝐴 𝑦 / 𝑥𝐵) → 𝑗 / 𝑘𝐶 ∈ (0[,]+∞))
181 eqid 2736 . . . . . . 7 (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶) = (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)
182180, 181fmptd 7016 . . . . . 6 (𝜑 → (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶): 𝑦𝐴 𝑦 / 𝑥𝐵⟶(0[,]+∞))
183182adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶): 𝑦𝐴 𝑦 / 𝑥𝐵⟶(0[,]+∞))
184155, 14eqeltrrid 2842 . . . . . 6 (𝜑 𝑦𝐴 𝑦 / 𝑥𝐵 ∈ V)
185184adantr 482 . . . . 5 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → 𝑦𝐴 𝑦 / 𝑥𝐵 ∈ V)
18696, 103, 108, 127, 153, 160, 167, 183, 185sge0iunmptlemre 44002 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))))
187158a1i 11 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑗 𝑦𝐴 𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))
188162a1i 11 . . . 4 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))) = (Σ^‘(𝑦𝐴 ↦ (Σ^‘(𝑗𝑦 / 𝑥𝐵𝑗 / 𝑘𝐶)))))
189186, 187, 1883eqtr4d 2786 . . 3 ((𝜑 ∧ ∀𝑥𝐴^‘(𝑘𝐵𝐶)) ≠ +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
19089, 95, 189syl2anc 585 . 2 ((𝜑 ∧ ¬ ∃𝑥𝐴^‘(𝑘𝐵𝐶)) = +∞) → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
19188, 190pm2.61dan 811 1 (𝜑 → (Σ^‘(𝑘 𝑥𝐴 𝐵𝐶)) = (Σ^‘(𝑥𝐴 ↦ (Σ^‘(𝑘𝐵𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1087   = wceq 1539  wcel 2104  wne 2941  wral 3062  wrex 3071  Vcvv 3437  csb 3837  wss 3892   ciun 4931  Disj wdisj 5046   class class class wbr 5081  cmpt 5164  ran crn 5597  wf 6450  cfv 6454  (class class class)co 7303  cr 10912  0cc0 10913  +∞cpnf 11048  *cxr 11050  cle 11052  [,]cicc 13124  Σ^csumge0 43949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-inf2 9439  ax-ac2 10261  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990  ax-pre-sup 10991
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-disj 5047  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-se 5552  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-isom 6463  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-om 7741  df-1st 7859  df-2nd 7860  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-er 8525  df-map 8644  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-sup 9241  df-oi 9309  df-card 9737  df-acn 9740  df-ac 9914  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-div 11675  df-nn 12016  df-2 12078  df-3 12079  df-n0 12276  df-z 12362  df-uz 12625  df-rp 12773  df-xadd 12891  df-ico 13127  df-icc 13128  df-fz 13282  df-fzo 13425  df-seq 13764  df-exp 13825  df-hash 14087  df-cj 14851  df-re 14852  df-im 14853  df-sqrt 14987  df-abs 14988  df-clim 15238  df-sum 15439  df-sumge0 43950
This theorem is referenced by:  sge0iun  44006  sge0xp  44016
  Copyright terms: Public domain W3C validator