| Step | Hyp | Ref
| Expression |
| 1 | | iunin2 5071 |
. . . . 5
⊢ ∪ 𝑘 ∈ ℕ (𝐸 ∩ 𝐴) = (𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴) |
| 2 | 1 | fveq2i 6909 |
. . . 4
⊢ (𝑀‘∪ 𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) = (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) |
| 3 | | iccssxr 13470 |
. . . . 5
⊢
(0[,]+∞) ⊆ ℝ* |
| 4 | | carsgval.2 |
. . . . . 6
⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 5 | | nnex 12272 |
. . . . . . . 8
⊢ ℕ
∈ V |
| 6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ ∈
V) |
| 7 | | carsgclctunlem2.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑂) |
| 8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐸 ∈ 𝒫 𝑂) |
| 9 | 8 | elpwincl1 32544 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐸 ∩ 𝐴) ∈ 𝒫 𝑂) |
| 10 | 6, 9 | elpwiuncl 32546 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ (𝐸 ∩ 𝐴) ∈ 𝒫 𝑂) |
| 11 | 4, 10 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 12 | 3, 11 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) ∈
ℝ*) |
| 13 | 2, 12 | eqeltrrid 2846 |
. . 3
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) ∈
ℝ*) |
| 14 | 4, 7 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝑀‘𝐸) ∈ (0[,]+∞)) |
| 15 | 3, 14 | sselid 3981 |
. . . 4
⊢ (𝜑 → (𝑀‘𝐸) ∈
ℝ*) |
| 16 | 7 | elpwdifcl 32545 |
. . . . . . 7
⊢ (𝜑 → (𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴) ∈ 𝒫 𝑂) |
| 17 | 4, 16 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
(0[,]+∞)) |
| 18 | 3, 17 | sselid 3981 |
. . . . 5
⊢ (𝜑 → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
ℝ*) |
| 19 | 18 | xnegcld 13342 |
. . . 4
⊢ (𝜑 →
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
ℝ*) |
| 20 | 15, 19 | xaddcld 13343 |
. . 3
⊢ (𝜑 → ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ∈
ℝ*) |
| 21 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 22 | 21, 9 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 23 | 22 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 24 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑘ℕ |
| 25 | 24 | esumcl 34031 |
. . . . . . 7
⊢ ((ℕ
∈ V ∧ ∀𝑘
∈ ℕ (𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) →
Σ*𝑘 ∈
ℕ(𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 26 | 6, 23, 25 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 27 | 3, 26 | sselid 3981 |
. . . . 5
⊢ (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸 ∩ 𝐴)) ∈
ℝ*) |
| 28 | 9 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐸 ∩ 𝐴) ∈ 𝒫 𝑂) |
| 29 | | dfiun3g 5978 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ (𝐸 ∩ 𝐴) ∈ 𝒫 𝑂 → ∪ 𝑘 ∈ ℕ (𝐸 ∩ 𝐴) = ∪ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))) |
| 30 | 28, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑘 ∈ ℕ (𝐸 ∩ 𝐴) = ∪ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))) |
| 31 | 30 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) = (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴)))) |
| 32 | | nnct 14022 |
. . . . . . . . . 10
⊢ ℕ
≼ ω |
| 33 | | mptct 10578 |
. . . . . . . . . 10
⊢ (ℕ
≼ ω → (𝑘
∈ ℕ ↦ (𝐸
∩ 𝐴)) ≼
ω) |
| 34 | | rnct 10565 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω → ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω) |
| 35 | 32, 33, 34 | mp2b 10 |
. . . . . . . . 9
⊢ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴)) ≼ ω |
| 36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω) |
| 37 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) = (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) |
| 38 | 37 | rnmptss 7143 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ (𝐸 ∩ 𝐴) ∈ 𝒫 𝑂 → ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂) |
| 39 | 28, 38 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂) |
| 40 | | mptexg 7241 |
. . . . . . . . . 10
⊢ (ℕ
∈ V → (𝑘 ∈
ℕ ↦ (𝐸 ∩
𝐴)) ∈
V) |
| 41 | | rnexg 7924 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ∈ V → ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ∈ V) |
| 42 | 5, 40, 41 | mp2b 10 |
. . . . . . . . 9
⊢ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴)) ∈ V |
| 43 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → (𝑥 ≼ ω ↔ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω)) |
| 44 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → (𝑥 ⊆ 𝒫 𝑂 ↔ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂)) |
| 45 | 43, 44 | 3anbi23d 1441 |
. . . . . . . . . . 11
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) ↔ (𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂))) |
| 46 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → ∪ 𝑥 = ∪
ran (𝑘 ∈ ℕ
↦ (𝐸 ∩ 𝐴))) |
| 47 | 46 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → (𝑀‘∪ 𝑥) = (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴)))) |
| 48 | | esumeq1 34035 |
. . . . . . . . . . . 12
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → Σ*𝑦 ∈ 𝑥(𝑀‘𝑦) = Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦)) |
| 49 | 47, 48 | breq12d 5156 |
. . . . . . . . . . 11
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → ((𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦) ↔ (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦))) |
| 50 | 45, 49 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑥 = ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) → (((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) ↔ ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂) → (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦)))) |
| 51 | | carsgsiga.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 52 | 50, 51 | vtoclg 3554 |
. . . . . . . . 9
⊢ (ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴)) ∈ V → ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂) → (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦))) |
| 53 | 42, 52 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝜑 ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ≼ ω ∧ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴)) ⊆ 𝒫 𝑂) → (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦)) |
| 54 | 36, 39, 53 | mpd3an23 1465 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘∪ ran
(𝑘 ∈ ℕ ↦
(𝐸 ∩ 𝐴))) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦)) |
| 55 | 31, 54 | eqbrtrd 5165 |
. . . . . 6
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) ≤ Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦)) |
| 56 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑦 = (𝐸 ∩ 𝐴) → (𝑀‘𝑦) = (𝑀‘(𝐸 ∩ 𝐴))) |
| 57 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐸 ∩ 𝐴) = ∅) → (𝐸 ∩ 𝐴) = ∅) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐸 ∩ 𝐴) = ∅) → (𝑀‘(𝐸 ∩ 𝐴)) = (𝑀‘∅)) |
| 59 | | carsgsiga.1 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀‘∅) = 0) |
| 60 | 59 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐸 ∩ 𝐴) = ∅) → (𝑀‘∅) = 0) |
| 61 | 58, 60 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝐸 ∩ 𝐴) = ∅) → (𝑀‘(𝐸 ∩ 𝐴)) = 0) |
| 62 | | carsgclctunlem2.1 |
. . . . . . . . 9
⊢ (𝜑 → Disj 𝑘 ∈ ℕ 𝐴) |
| 63 | | disjin 32599 |
. . . . . . . . 9
⊢
(Disj 𝑘
∈ ℕ 𝐴 →
Disj 𝑘 ∈
ℕ (𝐴 ∩ 𝐸)) |
| 64 | 62, 63 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑘 ∈ ℕ (𝐴 ∩ 𝐸)) |
| 65 | | incom 4209 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝐸) = (𝐸 ∩ 𝐴) |
| 66 | 65 | rgenw 3065 |
. . . . . . . . 9
⊢
∀𝑘 ∈
ℕ (𝐴 ∩ 𝐸) = (𝐸 ∩ 𝐴) |
| 67 | | disjeq2 5114 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
ℕ (𝐴 ∩ 𝐸) = (𝐸 ∩ 𝐴) → (Disj 𝑘 ∈ ℕ (𝐴 ∩ 𝐸) ↔ Disj 𝑘 ∈ ℕ (𝐸 ∩ 𝐴))) |
| 68 | 66, 67 | ax-mp 5 |
. . . . . . . 8
⊢
(Disj 𝑘
∈ ℕ (𝐴 ∩
𝐸) ↔ Disj 𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) |
| 69 | 64, 68 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → Disj 𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) |
| 70 | 56, 6, 22, 9, 61, 69 | esumrnmpt2 34069 |
. . . . . 6
⊢ (𝜑 → Σ*𝑦 ∈ ran (𝑘 ∈ ℕ ↦ (𝐸 ∩ 𝐴))(𝑀‘𝑦) = Σ*𝑘 ∈ ℕ(𝑀‘(𝐸 ∩ 𝐴))) |
| 71 | 55, 70 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) ≤ Σ*𝑘 ∈ ℕ(𝑀‘(𝐸 ∩ 𝐴))) |
| 72 | | carsgval.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑂 ∈ 𝑉) |
| 73 | | difssd 4137 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴) ⊆ 𝐸) |
| 74 | | carsgsiga.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
| 75 | 72, 4, 73, 7, 74 | carsgmon 34316 |
. . . . . . 7
⊢ (𝜑 → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘𝐸)) |
| 76 | 14, 17, 75 | xrge0subcld 32767 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ∈
(0[,]+∞)) |
| 77 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑀:𝒫 𝑂⟶(0[,]+∞)) |
| 78 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐸 ∈ 𝒫 𝑂) |
| 79 | 78 | elpwincl1 32544 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴) ∈ 𝒫 𝑂) |
| 80 | 77, 79 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞)) |
| 81 | 3, 80 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈
ℝ*) |
| 82 | | xrge0neqmnf 13492 |
. . . . . . . . . . 11
⊢ ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) |
| 83 | 80, 82 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) |
| 84 | 78 | elpwdifcl 32545 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴) ∈ 𝒫 𝑂) |
| 85 | 77, 84 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞)) |
| 86 | 3, 85 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈
ℝ*) |
| 87 | | xrge0neqmnf 13492 |
. . . . . . . . . . 11
⊢ ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ (0[,]+∞) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) |
| 88 | 85, 87 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) |
| 89 | 86 | xnegcld 13342 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈
ℝ*) |
| 90 | | xnegneg 13256 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 91 | 86, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 92 | 91 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 93 | | xnegeq 13249 |
. . . . . . . . . . . . . . . . 17
⊢
(-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞ →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) =
-𝑒-∞) |
| 94 | 93 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) =
-𝑒-∞) |
| 95 | | xnegmnf 13252 |
. . . . . . . . . . . . . . . 16
⊢
-𝑒-∞ = +∞ |
| 96 | 94, 95 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) →
-𝑒-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = +∞) |
| 97 | 92, 96 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = +∞) |
| 98 | 97 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
+∞)) |
| 99 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝜑) |
| 100 | | fz1ssnn 13595 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(1...𝑛) ⊆
ℕ |
| 101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆
ℕ) |
| 102 | 101 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 103 | | carsgclctunlem2.2 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ (toCaraSiga‘𝑀)) |
| 104 | 99, 102, 103 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → 𝐴 ∈ (toCaraSiga‘𝑀)) |
| 105 | 104 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀)) |
| 106 | | dfiun3g 5978 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑘 ∈
(1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) → ∪
𝑘 ∈ (1...𝑛)𝐴 = ∪ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)) |
| 107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑘 ∈ (1...𝑛)𝐴 = ∪ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)) |
| 108 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑂 ∈ 𝑉) |
| 109 | 59 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘∅) = 0) |
| 110 | 51 | 3adant1r 1178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) |
| 111 | | fzfi 14013 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1...𝑛) ∈
Fin |
| 112 | | mptfi 9391 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1...𝑛) ∈ Fin
→ (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin) |
| 113 | | rnfi 9380 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin) |
| 114 | 111, 112,
113 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin |
| 115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ Fin) |
| 116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...𝑛) ↦ 𝐴) = (𝑘 ∈ (1...𝑛) ↦ 𝐴) |
| 117 | 116 | rnmptss 7143 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑘 ∈
(1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (toCaraSiga‘𝑀)) |
| 118 | 105, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (toCaraSiga‘𝑀)) |
| 119 | 108, 77, 109, 110, 115, 118 | fiunelcarsg 34318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ∈ (toCaraSiga‘𝑀)) |
| 120 | 107, 119 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀)) |
| 121 | 108, 77 | elcarsg 34307 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∪ 𝑘 ∈ (1...𝑛)𝐴 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝑘 ∈ (1...𝑛)𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝑒)))) |
| 122 | 120, 121 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∪ 𝑘 ∈ (1...𝑛)𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝑒))) |
| 123 | 122 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝑒)) |
| 124 | | ineq1 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝐸 → (𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴) = (𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) |
| 125 | 124 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝐸 → (𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 126 | | difeq1 4119 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝐸 → (𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴) = (𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) |
| 127 | 126 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝐸 → (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 128 | 125, 127 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝐸 → ((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)))) |
| 129 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝐸 → (𝑀‘𝑒) = (𝑀‘𝐸)) |
| 130 | 128, 129 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝐸 → (((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝑒) ↔ ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝐸))) |
| 131 | 130 | rspcv 3618 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∈ 𝒫 𝑂 → (∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝑒) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝐸))) |
| 132 | 78, 123, 131 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝐸)) |
| 133 | 132 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘𝐸)) |
| 134 | | xaddpnf1 13268 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) =
+∞) |
| 135 | 81, 83, 134 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) =
+∞) |
| 136 | 135 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 +∞) =
+∞) |
| 137 | 98, 133, 136 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀‘𝐸) = +∞) |
| 138 | | carsgclctunlem2.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘𝐸) ≠ +∞) |
| 139 | 138 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → (𝑀‘𝐸) ≠ +∞) |
| 140 | 139 | neneqd 2945 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) → ¬ (𝑀‘𝐸) = +∞) |
| 141 | 137, 140 | pm2.65da 817 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ¬
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) = -∞) |
| 142 | 141 | neqned 2947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) |
| 143 | | xaddass 13291 |
. . . . . . . . . 10
⊢ ((((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) ∧ ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞) ∧
(-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≠ -∞)) → (((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))))) |
| 144 | 81, 83, 86, 88, 89, 142, 143 | syl222anc 1388 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))))) |
| 145 | | xnegid 13280 |
. . . . . . . . . . 11
⊢ ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* → ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = 0) |
| 146 | 86, 145 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = 0) |
| 147 | 146 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 ((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)))) = ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒
0)) |
| 148 | | xaddrid 13283 |
. . . . . . . . . 10
⊢ ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 0) = (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 149 | 81, 148 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 0) = (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 150 | 144, 147,
149 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 151 | 132 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) = ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)))) |
| 152 | 107 | ineq2d 4220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴) = (𝐸 ∩ ∪ ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴))) |
| 153 | 152 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) = (𝑀‘(𝐸 ∩ ∪ ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴)))) |
| 154 | | mptss 6060 |
. . . . . . . . . . . . 13
⊢
((1...𝑛) ⊆
ℕ → (𝑘 ∈
(1...𝑛) ↦ 𝐴) ⊆ (𝑘 ∈ ℕ ↦ 𝐴)) |
| 155 | | rnss 5950 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ (𝑘 ∈ ℕ ↦ 𝐴) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴)) |
| 156 | 100, 154,
155 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴) |
| 157 | 156 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran (𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴)) |
| 158 | | disjrnmpt 32598 |
. . . . . . . . . . . . 13
⊢
(Disj 𝑘
∈ ℕ 𝐴 →
Disj 𝑦 ∈ ran
(𝑘 ∈ ℕ ↦
𝐴)𝑦) |
| 159 | 62, 158 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦) |
| 160 | 159 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦) |
| 161 | | disjss1 5116 |
. . . . . . . . . . 11
⊢ (ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴) ⊆ ran (𝑘 ∈ ℕ ↦ 𝐴) → (Disj 𝑦 ∈ ran (𝑘 ∈ ℕ ↦ 𝐴)𝑦 → Disj 𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)𝑦)) |
| 162 | 157, 160,
161 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)𝑦) |
| 163 | 108, 77, 109, 110, 115, 118, 162, 78 | carsgclctunlem1 34319 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪ ran
(𝑘 ∈ (1...𝑛) ↦ 𝐴))) = Σ*𝑦 ∈ ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)(𝑀‘(𝐸 ∩ 𝑦))) |
| 164 | | ineq2 4214 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (𝐸 ∩ 𝑦) = (𝐸 ∩ 𝐴)) |
| 165 | 164 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑀‘(𝐸 ∩ 𝑦)) = (𝑀‘(𝐸 ∩ 𝐴))) |
| 166 | 111 | elexi 3503 |
. . . . . . . . . . 11
⊢
(1...𝑛) ∈
V |
| 167 | 166 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1...𝑛) ∈ V) |
| 168 | 99, 102, 22 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) → (𝑀‘(𝐸 ∩ 𝐴)) ∈ (0[,]+∞)) |
| 169 | | inss2 4238 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 ∩ 𝐴) ⊆ 𝐴 |
| 170 | | sseq2 4010 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = ∅ → ((𝐸 ∩ 𝐴) ⊆ 𝐴 ↔ (𝐸 ∩ 𝐴) ⊆ ∅)) |
| 171 | 169, 170 | mpbii 233 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝐸 ∩ 𝐴) ⊆ ∅) |
| 172 | | ss0 4402 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ∩ 𝐴) ⊆ ∅ → (𝐸 ∩ 𝐴) = ∅) |
| 173 | 171, 172 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (𝐸 ∩ 𝐴) = ∅) |
| 174 | 173 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝐸 ∩ 𝐴) = ∅) |
| 175 | 174 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘(𝐸 ∩ 𝐴)) = (𝑀‘∅)) |
| 176 | 109 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘∅) = 0) |
| 177 | 175, 176 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (1...𝑛)) ∧ 𝐴 = ∅) → (𝑀‘(𝐸 ∩ 𝐴)) = 0) |
| 178 | 62 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑘 ∈ ℕ 𝐴) |
| 179 | | disjss1 5116 |
. . . . . . . . . . 11
⊢
((1...𝑛) ⊆
ℕ → (Disj 𝑘 ∈ ℕ 𝐴 → Disj 𝑘 ∈ (1...𝑛)𝐴)) |
| 180 | 101, 178,
179 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Disj 𝑘 ∈ (1...𝑛)𝐴) |
| 181 | 165, 167,
168, 104, 177, 180 | esumrnmpt2 34069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑦 ∈
ran (𝑘 ∈ (1...𝑛) ↦ 𝐴)(𝑀‘(𝐸 ∩ 𝑦)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸 ∩ 𝐴))) |
| 182 | 153, 163,
181 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ (1...𝑛)𝐴)) = Σ*𝑘 ∈ (1...𝑛)(𝑀‘(𝐸 ∩ 𝐴))) |
| 183 | 150, 151,
182 | 3eqtr3rd 2786 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝑀‘(𝐸 ∩ 𝐴)) = ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)))) |
| 184 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
(0[,]+∞)) |
| 185 | 3, 184 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
ℝ*) |
| 186 | 185 | xnegcld 13342 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈
ℝ*) |
| 187 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘𝐸) ∈
ℝ*) |
| 188 | | iunss1 5006 |
. . . . . . . . . . . 12
⊢
((1...𝑛) ⊆
ℕ → ∪ 𝑘 ∈ (1...𝑛)𝐴 ⊆ ∪
𝑘 ∈ ℕ 𝐴) |
| 189 | 100, 188 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑘 ∈ (1...𝑛)𝐴 ⊆ ∪
𝑘 ∈ ℕ 𝐴) |
| 190 | 189 | sscond 4146 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴) ⊆ (𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) |
| 191 | 74 | 3adant1r 1178 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦)) |
| 192 | 108, 77, 190, 84, 191 | carsgmon 34316 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) |
| 193 | | xleneg 13260 |
. . . . . . . . . 10
⊢ (((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈ ℝ*
∧ (𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*) →
((𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ↔ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 194 | 193 | biimpa 476 |
. . . . . . . . 9
⊢ ((((𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈ ℝ*
∧ (𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ*) ∧ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) → -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) |
| 195 | 185, 86, 192, 194 | syl21anc 838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) |
| 196 | | xleadd2a 13296 |
. . . . . . . 8
⊢
(((-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ∈ ℝ* ∧
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈ ℝ*
∧ (𝑀‘𝐸) ∈ ℝ*)
∧ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴)) ≤ -𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) → ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 197 | 89, 186, 187, 195, 196 | syl31anc 1375 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ (1...𝑛)𝐴))) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 198 | 183, 197 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
Σ*𝑘 ∈
(1...𝑛)(𝑀‘(𝐸 ∩ 𝐴)) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 199 | 76, 22, 198 | esumgect 34091 |
. . . . 5
⊢ (𝜑 → Σ*𝑘 ∈ ℕ(𝑀‘(𝐸 ∩ 𝐴)) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 200 | 12, 27, 20, 71, 199 | xrletrd 13204 |
. . . 4
⊢ (𝜑 → (𝑀‘∪
𝑘 ∈ ℕ (𝐸 ∩ 𝐴)) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 201 | 2, 200 | eqbrtrrid 5179 |
. . 3
⊢ (𝜑 → (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 202 | | xleadd1a 13295 |
. . 3
⊢ ((((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) ∈ ℝ*
∧ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ∈ ℝ*
∧ (𝑀‘(𝐸 ∖ ∪ 𝑘 ∈ ℕ 𝐴)) ∈ ℝ*) ∧ (𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) ≤ ((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ≤ (((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 203 | 13, 20, 18, 201, 202 | syl31anc 1375 |
. 2
⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ≤ (((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)))) |
| 204 | | xrge0npcan 33025 |
. . 3
⊢ (((𝑀‘𝐸) ∈ (0[,]+∞) ∧ (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ∈ (0[,]+∞) ∧
(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴)) ≤ (𝑀‘𝐸)) → (((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) = (𝑀‘𝐸)) |
| 205 | 14, 17, 75, 204 | syl3anc 1373 |
. 2
⊢ (𝜑 → (((𝑀‘𝐸) +𝑒
-𝑒(𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) = (𝑀‘𝐸)) |
| 206 | 203, 205 | breqtrd 5169 |
1
⊢ (𝜑 → ((𝑀‘(𝐸 ∩ ∪
𝑘 ∈ ℕ 𝐴)) +𝑒 (𝑀‘(𝐸 ∖ ∪
𝑘 ∈ ℕ 𝐴))) ≤ (𝑀‘𝐸)) |