Step | Hyp | Ref
| Expression |
1 | | sge0split.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | 1 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝐴 ∈ 𝑉) |
3 | | sge0split.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
4 | 3 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝐵 ∈ 𝑊) |
5 | | sge0split.u |
. . . 4
⊢ 𝑈 = (𝐴 ∪ 𝐵) |
6 | | sge0split.in0 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → (𝐴 ∩ 𝐵) = ∅) |
8 | | sge0split.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑈⟶(0[,]+∞)) |
9 | 8 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝐹:𝑈⟶(0[,]+∞)) |
10 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) ∈ ℝ) |
11 | 2, 4, 5, 7, 9, 10 | sge0resplit 43619 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +
(Σ^‘(𝐹 ↾ 𝐵)))) |
12 | | unexg 7534 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∪ 𝐵) ∈ V) |
13 | 1, 3, 12 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) |
14 | 5, 13 | eqeltrid 2842 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ V) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) → 𝑈 ∈ V) |
16 | 15, 9, 10 | sge0ssre 43610 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ) |
17 | 15, 9, 10 | sge0ssre 43610 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ) |
18 | | rexadd 12822 |
. . . . 5
⊢
(((Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ ∧
(Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) =
((Σ^‘(𝐹 ↾ 𝐴)) +
(Σ^‘(𝐹 ↾ 𝐵)))) |
19 | 16, 17, 18 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) =
((Σ^‘(𝐹 ↾ 𝐴)) +
(Σ^‘(𝐹 ↾ 𝐵)))) |
20 | 19 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
((Σ^‘(𝐹 ↾ 𝐴)) +
(Σ^‘(𝐹 ↾ 𝐵))) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
21 | 11, 20 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
22 | | simpl 486 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) → 𝜑) |
23 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) → ¬
(Σ^‘𝐹) ∈ ℝ) |
24 | 14, 8 | sge0repnf 43599 |
. . . . . 6
⊢ (𝜑 →
((Σ^‘𝐹) ∈ ℝ ↔ ¬
(Σ^‘𝐹) = +∞)) |
25 | 24 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) →
((Σ^‘𝐹) ∈ ℝ ↔ ¬
(Σ^‘𝐹) = +∞)) |
26 | 23, 25 | mtbid 327 |
. . . 4
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) → ¬ ¬
(Σ^‘𝐹) = +∞) |
27 | 26 | notnotrd 135 |
. . 3
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) = +∞) |
28 | 14, 8 | sge0xrcl 43598 |
. . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) ∈
ℝ*) |
29 | 28 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
(Σ^‘𝐹) ∈
ℝ*) |
30 | | ssun1 4086 |
. . . . . . . . . 10
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
31 | 30, 5 | sseqtrri 3938 |
. . . . . . . . 9
⊢ 𝐴 ⊆ 𝑈 |
32 | 31 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
33 | 8, 32 | fssresd 6586 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞)) |
34 | 1, 33 | sge0xrcl 43598 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐴)) ∈
ℝ*) |
35 | | iccssxr 13018 |
. . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* |
36 | | ssun2 4087 |
. . . . . . . . . . 11
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
37 | 36, 5 | sseqtrri 3938 |
. . . . . . . . . 10
⊢ 𝐵 ⊆ 𝑈 |
38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
39 | 8, 38 | fssresd 6586 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
40 | 3, 39 | sge0cl 43594 |
. . . . . . 7
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐵)) ∈ (0[,]+∞)) |
41 | 35, 40 | sseldi 3899 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐵)) ∈
ℝ*) |
42 | 34, 41 | xaddcld 12891 |
. . . . 5
⊢ (𝜑 →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ∈
ℝ*) |
43 | 42 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ∈
ℝ*) |
44 | | pnfxr 10887 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
45 | | eqid 2737 |
. . . . . . . . 9
⊢ +∞
= +∞ |
46 | | xreqle 42530 |
. . . . . . . . 9
⊢
((+∞ ∈ ℝ* ∧ +∞ = +∞) →
+∞ ≤ +∞) |
47 | 44, 45, 46 | mp2an 692 |
. . . . . . . 8
⊢ +∞
≤ +∞ |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ≤
+∞) |
49 | 14 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝑈 ∈ V) |
50 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝐹:𝑈⟶(0[,]+∞)) |
51 | | rnresss 5887 |
. . . . . . . . . . 11
⊢ ran
(𝐹 ↾ 𝐴) ⊆ ran 𝐹 |
52 | 51 | sseli 3896 |
. . . . . . . . . 10
⊢ (+∞
∈ ran (𝐹 ↾ 𝐴) → +∞ ∈ ran
𝐹) |
53 | 52 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ∈ ran 𝐹) |
54 | 49, 50, 53 | sge0pnfval 43586 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
(Σ^‘𝐹) = +∞) |
55 | | xrge0neqmnf 13040 |
. . . . . . . . . . . . . 14
⊢
((Σ^‘(𝐹 ↾ 𝐵)) ∈ (0[,]+∞) →
(Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞) |
56 | 40, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞) |
57 | | xaddpnf2 12817 |
. . . . . . . . . . . . 13
⊢
(((Σ^‘(𝐹 ↾ 𝐵)) ∈ ℝ* ∧
(Σ^‘(𝐹 ↾ 𝐵)) ≠ -∞) → (+∞
+𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞) |
58 | 41, 56, 57 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (+∞
+𝑒 (Σ^‘(𝐹 ↾ 𝐵))) = +∞) |
59 | 58 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (𝜑 → +∞ = (+∞
+𝑒 (Σ^‘(𝐹 ↾ 𝐵)))) |
60 | 59 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ = (+∞
+𝑒 (Σ^‘(𝐹 ↾ 𝐵)))) |
61 | 1 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → 𝐴 ∈ 𝑉) |
62 | 33 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞)) |
63 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) → +∞ ∈ ran (𝐹 ↾ 𝐴)) |
64 | 61, 62, 63 | sge0pnfval 43586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
(Σ^‘(𝐹 ↾ 𝐴)) = +∞) |
65 | 64 | oveq1d 7228 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) = (+∞ +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
66 | 60, 54, 65 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
67 | 66, 54 | eqtr3d 2779 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) = +∞) |
68 | 54, 67 | breq12d 5066 |
. . . . . . 7
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
((Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ↔ +∞ ≤
+∞)) |
69 | 48, 68 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐴)) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
70 | 47 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ≤
+∞) |
71 | 14 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝑈 ∈ V) |
72 | 8 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,]+∞)) |
73 | | rnresss 5887 |
. . . . . . . . . . . . 13
⊢ ran
(𝐹 ↾ 𝐵) ⊆ ran 𝐹 |
74 | 73 | sseli 3896 |
. . . . . . . . . . . 12
⊢ (+∞
∈ ran (𝐹 ↾ 𝐵) → +∞ ∈ ran
𝐹) |
75 | 74 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ∈ ran 𝐹) |
76 | 71, 72, 75 | sge0pnfval 43586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
(Σ^‘𝐹) = +∞) |
77 | 3 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → 𝐵 ∈ 𝑊) |
78 | 39 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
79 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) → +∞ ∈ ran (𝐹 ↾ 𝐵)) |
80 | 77, 78, 79 | sge0pnfval 43586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
(Σ^‘(𝐹 ↾ 𝐵)) = +∞) |
81 | 80 | oveq2d 7229 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
+∞)) |
82 | 1, 33 | sge0cl 43594 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐴)) ∈ (0[,]+∞)) |
83 | | xrge0neqmnf 13040 |
. . . . . . . . . . . . . 14
⊢
((Σ^‘(𝐹 ↾ 𝐴)) ∈ (0[,]+∞) →
(Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞) |
85 | | xaddpnf1 12816 |
. . . . . . . . . . . . 13
⊢
(((Σ^‘(𝐹 ↾ 𝐴)) ∈ ℝ* ∧
(Σ^‘(𝐹 ↾ 𝐴)) ≠ -∞) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) =
+∞) |
86 | 34, 84, 85 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) =
+∞) |
87 | 86 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒 +∞) =
+∞) |
88 | 81, 87 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) = +∞) |
89 | 76, 88 | breq12d 5066 |
. . . . . . . . 9
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
((Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ↔ +∞ ≤
+∞)) |
90 | 70, 89 | mpbird 260 |
. . . . . . . 8
⊢ ((𝜑 ∧ +∞ ∈ ran (𝐹 ↾ 𝐵)) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
91 | 90 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ +∞ ∈ ran
(𝐹 ↾ 𝐵)) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
92 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
93 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
94 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) = (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
95 | 94 | elrnmpt 5825 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) |
96 | 93, 95 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ↔ ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
97 | 92, 96 | sylib 221 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → ∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
98 | | simp3 1140 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) |
99 | | inss1 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝑥 ∩ 𝐴) |
100 | | inss2 4144 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 |
101 | 99, 100 | sstri 3910 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ 𝐴 |
102 | | inss2 4144 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝑥 ∩ 𝐵) |
103 | | inss2 4144 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵 |
104 | 102, 103 | sstri 3910 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ 𝐵 |
105 | 101, 104 | ssini 4146 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝐴 ∩ 𝐵) |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ (𝐴 ∩ 𝐵)) |
107 | 106, 6 | sseqtrd 3941 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ ∅) |
108 | | ss0 4313 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) ⊆ ∅ → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅) |
110 | 109 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((𝑥 ∩ 𝐴) ∩ (𝑥 ∩ 𝐵)) = ∅) |
111 | | indi 4188 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) |
112 | 111 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵)) |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵)) = (𝑥 ∩ (𝐴 ∪ 𝐵))) |
114 | 5 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∪ 𝐵) = 𝑈 |
115 | 114 | ineq2i 4124 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = (𝑥 ∩ 𝑈) |
116 | 115 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ (𝐴 ∪ 𝐵)) = (𝑥 ∩ 𝑈)) |
117 | | elinel1 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ 𝒫 𝑈) |
118 | | elpwi 4522 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝒫 𝑈 → 𝑥 ⊆ 𝑈) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ⊆ 𝑈) |
120 | | df-ss 3883 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ⊆ 𝑈 ↔ (𝑥 ∩ 𝑈) = 𝑥) |
121 | 120 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ⊆ 𝑈 → (𝑥 ∩ 𝑈) = 𝑥) |
122 | 119, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝑈) = 𝑥) |
123 | 113, 116,
122 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵))) |
124 | 123 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ 𝐵))) |
125 | | elinel2 4110 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → 𝑥 ∈ Fin) |
126 | 125 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝑥 ∈ Fin) |
127 | | rge0ssre 13044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0[,)+∞) ⊆ ℝ |
128 | 8 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,]+∞)) |
129 | | pm4.56 989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((¬
+∞ ∈ ran (𝐹
↾ 𝐴) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ↔ ¬
(+∞ ∈ ran (𝐹
↾ 𝐴) ∨ +∞
∈ ran (𝐹 ↾ 𝐵))) |
130 | 129 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((¬
+∞ ∈ ran (𝐹
↾ 𝐴) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) → ¬
(+∞ ∈ ran (𝐹
↾ 𝐴) ∨ +∞
∈ ran (𝐹 ↾ 𝐵))) |
131 | | elun 4063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (+∞
∈ (ran (𝐹 ↾
𝐴) ∪ ran (𝐹 ↾ 𝐵)) ↔ (+∞ ∈ ran (𝐹 ↾ 𝐴) ∨ +∞ ∈ ran (𝐹 ↾ 𝐵))) |
132 | 130, 131 | sylnibr 332 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((¬
+∞ ∈ ran (𝐹
↾ 𝐴) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) → ¬
+∞ ∈ (ran (𝐹
↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵))) |
133 | 132 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈
(ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵))) |
134 | | rnresun 42389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ran
(𝐹 ↾ (𝐴 ∪ 𝐵)) = (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) |
135 | 134 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ran
(𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran (𝐹 ↾ (𝐴 ∪ 𝐵)) |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran (𝐹 ↾ (𝐴 ∪ 𝐵))) |
137 | 114 | reseq2i 5848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 ↾ (𝐴 ∪ 𝐵)) = (𝐹 ↾ 𝑈) |
138 | 137 | rneqi 5806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ran
(𝐹 ↾ (𝐴 ∪ 𝐵)) = ran (𝐹 ↾ 𝑈) |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ran (𝐹 ↾ (𝐴 ∪ 𝐵)) = ran (𝐹 ↾ 𝑈)) |
140 | | ffn 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹:𝑈⟶(0[,]+∞) → 𝐹 Fn 𝑈) |
141 | | fnresdm 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 Fn 𝑈 → (𝐹 ↾ 𝑈) = 𝐹) |
142 | 8, 140, 141 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐹 ↾ 𝑈) = 𝐹) |
143 | 142 | rneqd 5807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ran (𝐹 ↾ 𝑈) = ran 𝐹) |
144 | 136, 139,
143 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran 𝐹) |
145 | 144 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (ran (𝐹 ↾ 𝐴) ∪ ran (𝐹 ↾ 𝐵)) = ran 𝐹) |
146 | 133, 145 | neleqtrd 2859 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ¬ +∞ ∈
ran 𝐹) |
147 | 128, 146 | fge0iccico 43583 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → 𝐹:𝑈⟶(0[,)+∞)) |
148 | 147 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝐹:𝑈⟶(0[,)+∞)) |
149 | 119 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑥 ⊆ 𝑈) |
150 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑥) |
151 | 149, 150 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈) |
152 | 151 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑈) |
153 | 148, 152 | ffvelrnd 6905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ (0[,)+∞)) |
154 | 127, 153 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℝ) |
155 | 154 | recnd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ 𝑥) → (𝐹‘𝑦) ∈ ℂ) |
156 | 110, 124,
126, 155 | fsumsplit 15305 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) |
157 | | infi 8899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ Fin → (𝑥 ∩ 𝐴) ∈ Fin) |
158 | 125, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐴) ∈ Fin) |
159 | 158 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ∈ Fin) |
160 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin))) |
161 | | elinel1 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → 𝑦 ∈ 𝑥) |
162 | 161 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → 𝑦 ∈ 𝑥) |
163 | 160, 162,
154 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → (𝐹‘𝑦) ∈ ℝ) |
164 | 159, 163 | fsumrecl 15298 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ) |
165 | | infi 8899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ Fin → (𝑥 ∩ 𝐵) ∈ Fin) |
166 | 125, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑥 ∩ 𝐵) ∈ Fin) |
167 | 166 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin) |
168 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → (((𝜑 ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈ ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin))) |
169 | | elinel1 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → 𝑦 ∈ 𝑥) |
170 | 169 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → 𝑦 ∈ 𝑥) |
171 | 168, 170,
154 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐴)) ∧ ¬
+∞ ∈ ran (𝐹
↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → (𝐹‘𝑦) ∈ ℝ) |
172 | 167, 171 | fsumrecl 15298 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ) |
173 | | rexadd 12822 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((Σ𝑦 ∈
(𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ ∧ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) |
174 | 164, 172,
173 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) |
175 | 174 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) + Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) |
176 | 156, 175 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) = (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦))) |
177 | | ressxr 10877 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ℝ
⊆ ℝ* |
178 | 177, 164 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈
ℝ*) |
179 | 177, 172 | sseldi 3899 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈
ℝ*) |
180 | 1 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → 𝐴 ∈ 𝑉) |
181 | 33 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞)) |
182 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝐴)) |
183 | 181, 182 | fge0iccico 43583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,)+∞)) |
184 | 180, 183 | sge0reval 43585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) →
(Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
)) |
185 | 184 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) =
(Σ^‘(𝐹 ↾ 𝐴))) |
186 | 34 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) →
(Σ^‘(𝐹 ↾ 𝐴)) ∈
ℝ*) |
187 | 185, 186 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ*) |
188 | 187 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ*) |
189 | 3 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → 𝐵 ∈ 𝑊) |
190 | 39 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
191 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) |
192 | 190, 191 | fge0iccico 43583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,)+∞)) |
193 | 189, 192 | sge0reval 43585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) →
(Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)) |
194 | 193 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) =
(Σ^‘(𝐹 ↾ 𝐵))) |
195 | 41 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) →
(Σ^‘(𝐹 ↾ 𝐵)) ∈
ℝ*) |
196 | 194, 195 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*) |
197 | 196 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*) |
198 | 188, 197 | jca 515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*)) |
199 | 198 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*)) |
200 | 178, 179,
199 | jca31 518 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ* ∧
Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ*) ∧ (sup(ran
(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*))) |
201 | 180 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐴 ∈ 𝑉) |
202 | 181 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,]+∞)) |
203 | 182 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝐴)) |
204 | 202, 203 | fge0iccico 43583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐴):𝐴⟶(0[,)+∞)) |
205 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ⊆ 𝐴) |
206 | 158 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐴) ∈ Fin) |
207 | 201, 204,
205, 206 | fsumlesge0 43590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ≤
(Σ^‘(𝐹 ↾ 𝐴))) |
208 | 100 | sseli 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → 𝑦 ∈ 𝐴) |
209 | | fvres 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
210 | 208, 209 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (𝑥 ∩ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
211 | 210 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐴)) → ((𝐹 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
212 | 211 | sumeq2dv 15267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦)) |
213 | 184 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
)) |
214 | 212, 213 | breq12d 5066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)((𝐹 ↾ 𝐴)‘𝑦) ≤
(Σ^‘(𝐹 ↾ 𝐴)) ↔ Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
))) |
215 | 207, 214 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
)) |
216 | 215 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
)) |
217 | 189 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → 𝐵 ∈ 𝑊) |
218 | 190 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,]+∞)) |
219 | 191 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) |
220 | 218, 219 | fge0iccico 43583 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝐹 ↾ 𝐵):𝐵⟶(0[,)+∞)) |
221 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ⊆ 𝐵) |
222 | 166 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (𝑥 ∩ 𝐵) ∈ Fin) |
223 | 217, 220,
221, 222 | fsumlesge0 43590 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) ≤
(Σ^‘(𝐹 ↾ 𝐵))) |
224 | 103 | sseli 3896 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → 𝑦 ∈ 𝐵) |
225 | | fvres 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦)) |
226 | 224, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ (𝑥 ∩ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦)) |
227 | 226 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) ∧ 𝑦 ∈ (𝑥 ∩ 𝐵)) → ((𝐹 ↾ 𝐵)‘𝑦) = (𝐹‘𝑦)) |
228 | 227 | sumeq2dv 15267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) = Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) |
229 | 193 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) →
(Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)) |
230 | 228, 229 | breq12d 5066 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐵)((𝐹 ↾ 𝐵)‘𝑦) ≤
(Σ^‘(𝐹 ↾ 𝐵)) ↔ Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
231 | 223, 230 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)) |
232 | 231 | adantllr 719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)) |
233 | 216, 232 | jca 515 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∧
Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
234 | | xle2add 12849 |
. . . . . . . . . . . . . . . . . 18
⊢
(((Σ𝑦 ∈
(𝑥 ∩ 𝐴)(𝐹‘𝑦) ∈ ℝ* ∧
Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ∈ ℝ*) ∧ (sup(ran
(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∈
ℝ* ∧ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < ) ∈
ℝ*)) → ((Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) ≤ sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < ) ∧
Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦) ≤ sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) →
(Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)))) |
235 | 200, 233,
234 | sylc 65 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → (Σ𝑦 ∈ (𝑥 ∩ 𝐴)(𝐹‘𝑦) +𝑒 Σ𝑦 ∈ (𝑥 ∩ 𝐵)(𝐹‘𝑦)) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
236 | 176, 235 | eqbrtrd 5075 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
237 | 236 | 3adant3 1134 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
238 | 98, 237 | eqbrtrd 5075 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑥 ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
239 | 238 | 3exp 1121 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (𝑥 ∈ (𝒫 𝑈 ∩ Fin) → (𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))))) |
240 | 239 | rexlimdv 3202 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)))) |
241 | 240 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → (∃𝑥 ∈ (𝒫 𝑈 ∩ Fin)𝑧 = Σ𝑦 ∈ 𝑥 (𝐹‘𝑦) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)))) |
242 | 97, 241 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) ∧ 𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))) → 𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
243 | 242 | ralrimiva 3105 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
244 | 147 | sge0rnre 43577 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆ ℝ) |
245 | 177 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ℝ ⊆
ℝ*) |
246 | 244, 245 | sstrd 3911 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)) ⊆
ℝ*) |
247 | 188, 197 | xaddcld 12891 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ∈
ℝ*) |
248 | | supxrleub 12916 |
. . . . . . . . . 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) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)))) |
249 | 246, 247,
248 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → (sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ≤ (sup(ran
(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, < )) ↔
∀𝑧 ∈ ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦))𝑧 ≤ (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)))) |
250 | 243, 249 | mpbird 260 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, < ) ≤ (sup(ran
(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
251 | 14 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) → 𝑈 ∈ V) |
252 | 251, 147 | sge0reval 43585 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) →
(Σ^‘𝐹) = sup(ran (𝑥 ∈ (𝒫 𝑈 ∩ Fin) ↦ Σ𝑦 ∈ 𝑥 (𝐹‘𝑦)), ℝ*, <
)) |
253 | 184 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) →
(Σ^‘(𝐹 ↾ 𝐴)) = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, <
)) |
254 | 193 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) →
(Σ^‘(𝐹 ↾ 𝐵)) = sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
)) |
255 | 253, 254 | oveq12d 7231 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) = (sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ Σ𝑏 ∈ 𝑎 ((𝐹 ↾ 𝐴)‘𝑏)), ℝ*, < )
+𝑒 sup(ran (𝑐 ∈ (𝒫 𝐵 ∩ Fin) ↦ Σ𝑑 ∈ 𝑐 ((𝐹 ↾ 𝐵)‘𝑑)), ℝ*, <
))) |
256 | 250, 252,
255 | 3brtr4d 5085 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) ∧ ¬ +∞ ∈
ran (𝐹 ↾ 𝐵)) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
257 | 91, 256 | pm2.61dan 813 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ +∞ ∈ ran
(𝐹 ↾ 𝐴)) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
258 | 69, 257 | pm2.61dan 813 |
. . . . 5
⊢ (𝜑 →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
259 | 258 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
(Σ^‘𝐹) ≤
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
260 | | pnfge 12722 |
. . . . . . 7
⊢
(((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ∈ ℝ* →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞) |
261 | 42, 260 | syl 17 |
. . . . . 6
⊢ (𝜑 →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞) |
262 | 261 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ≤ +∞) |
263 | | id 22 |
. . . . . . 7
⊢
((Σ^‘𝐹) = +∞ →
(Σ^‘𝐹) = +∞) |
264 | 263 | eqcomd 2743 |
. . . . . 6
⊢
((Σ^‘𝐹) = +∞ → +∞ =
(Σ^‘𝐹)) |
265 | 264 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) → +∞ =
(Σ^‘𝐹)) |
266 | 262, 265 | breqtrd 5079 |
. . . 4
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵))) ≤
(Σ^‘𝐹)) |
267 | 29, 43, 259, 266 | xrletrid 12745 |
. . 3
⊢ ((𝜑 ∧
(Σ^‘𝐹) = +∞) →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
268 | 22, 27, 267 | syl2anc 587 |
. 2
⊢ ((𝜑 ∧ ¬
(Σ^‘𝐹) ∈ ℝ) →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |
269 | 21, 268 | pm2.61dan 813 |
1
⊢ (𝜑 →
(Σ^‘𝐹) =
((Σ^‘(𝐹 ↾ 𝐴)) +𝑒
(Σ^‘(𝐹 ↾ 𝐵)))) |