Step | Hyp | Ref
| Expression |
1 | | carageniuncllem2.o |
. . . 4
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
2 | | carageniuncllem2.x |
. . . 4
⊢ 𝑋 = ∪
dom 𝑂 |
3 | | carageniuncllem2.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
4 | | carageniuncllem2.re |
. . . 4
⊢ (𝜑 → (𝑂‘𝐴) ∈ ℝ) |
5 | | inss1 3795 |
. . . . 5
⊢ (𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ 𝐴 |
6 | 5 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ 𝐴) |
7 | 1, 2, 3, 4, 6 | omessre 39400 |
. . 3
⊢ (𝜑 → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ) |
8 | | difssd 3700 |
. . . 4
⊢ (𝜑 → (𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ 𝐴) |
9 | 1, 2, 3, 4, 8 | omessre 39400 |
. . 3
⊢ (𝜑 → (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ) |
10 | | rexadd 11937 |
. . 3
⊢ (((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ ∧ (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) = ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
11 | 7, 9, 10 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) = ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))))) |
12 | | carageniuncllem2.z |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
13 | | ssinss1 3803 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑋 → (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝑋) |
14 | 3, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝑋) |
15 | 1, 2 | unidmex 38242 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ V) |
16 | | ssexg 4732 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ V) → 𝐴 ∈ V) |
17 | 3, 15, 16 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ V) |
18 | | inex1g 4729 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V → (𝐴 ∩ (𝐹‘𝑛)) ∈ V) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑛)) ∈ V) |
20 | | elpwg 4116 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∩ (𝐹‘𝑛)) ∈ V → ((𝐴 ∩ (𝐹‘𝑛)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝑋)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 ∩ (𝐹‘𝑛)) ∈ 𝒫 𝑋 ↔ (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝑋)) |
22 | 14, 21 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑛)) ∈ 𝒫 𝑋) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐴 ∩ (𝐹‘𝑛)) ∈ 𝒫 𝑋) |
24 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))) |
25 | 23, 24 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))):𝑍⟶𝒫 𝑋) |
26 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
27 | 26 | ineq2d 3776 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝐴 ∩ (𝐹‘𝑘)) = (𝐴 ∩ (𝐹‘𝑛))) |
28 | 27 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘))) = (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))) |
29 | 28 | feq1i 5949 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘))):𝑍⟶𝒫 𝑋 ↔ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))):𝑍⟶𝒫 𝑋) |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘))):𝑍⟶𝒫 𝑋 ↔ (𝑛 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑛))):𝑍⟶𝒫 𝑋)) |
31 | 25, 30 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘))):𝑍⟶𝒫 𝑋) |
32 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
33 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐴 ∩ (𝐹‘𝑛)) ∈ V) |
34 | 28 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ 𝑍 ∧ (𝐴 ∩ (𝐹‘𝑛)) ∈ V) → ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛) = (𝐴 ∩ (𝐹‘𝑛))) |
35 | 32, 33, 34 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛) = (𝐴 ∩ (𝐹‘𝑛))) |
36 | 35 | iuneq2dv 4478 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) |
37 | 36 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) = (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)))) |
38 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑛𝜑 |
39 | | carageniuncllem2.e |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
40 | | carageniuncllem2.f |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝑛) ∖ ∪
𝑖 ∈ (𝑀..^𝑛)(𝐸‘𝑖))) |
41 | 38, 12, 39, 40 | iundjiun 39353 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((∀𝑚 ∈ 𝑍 ∪ 𝑛 ∈ (𝑀...𝑚)(𝐹‘𝑛) = ∪ 𝑛 ∈ (𝑀...𝑚)(𝐸‘𝑛) ∧ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ∧ Disj 𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
42 | 41 | simplrd 789 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐸‘𝑛) = ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
44 | 43 | ineq2d 3776 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛))) |
45 | | iunin2 4520 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)) = (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) |
46 | 45 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ ∪ 𝑛 ∈ 𝑍 (𝐹‘𝑛)) = ∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)) |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐹‘𝑛)) = ∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) |
48 | 44, 47 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) |
49 | 48 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) = (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)))) |
50 | 49, 7 | eqeltrrd 2689 |
. . . . . . . . 9
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
51 | 37, 50 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → (𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) ∈ ℝ) |
52 | | carageniuncllem2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈
ℝ+) |
53 | 1, 2, 12, 31, 51, 52 | omeiunltfirp 39409 |
. . . . . . 7
⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) + 𝑌)) |
54 | 37 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) = (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)))) |
55 | | elpwinss 38241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧 ⊆ 𝑍) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) → 𝑧 ⊆ 𝑍) |
57 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) → 𝑛 ∈ 𝑧) |
58 | 56, 57 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛 ∈ 𝑧) → 𝑛 ∈ 𝑍) |
59 | 58 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) → 𝑛 ∈ 𝑍) |
60 | 19 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) → (𝐴 ∩ (𝐹‘𝑛)) ∈ V) |
61 | 59, 60, 34 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) → ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛) = (𝐴 ∩ (𝐹‘𝑛))) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛 ∈ 𝑧) → (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) = (𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
63 | 62 | sumeq2dv 14281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) = Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
64 | 63 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) + 𝑌) = (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
65 | 54, 64 | breq12d 4596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) + 𝑌) ↔ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
66 | 65 | biimpd 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) + 𝑌) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
67 | 66 | reximdva 3000 |
. . . . . . 7
⊢ (𝜑 → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪
𝑛 ∈ 𝑍 ((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) < (Σ𝑛 ∈ 𝑧 (𝑂‘((𝑘 ∈ 𝑍 ↦ (𝐴 ∩ (𝐹‘𝑘)))‘𝑛)) + 𝑌) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
68 | 53, 67 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
69 | | carageniuncllem2.m |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
70 | 69 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑀 ∈ ℤ) |
71 | 55 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ⊆ 𝑍) |
72 | | elinel2 3762 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧 ∈ Fin) |
73 | 72 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ Fin) |
74 | 70, 12, 71, 73 | uzfissfz 38483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ∃𝑘 ∈ 𝑍 𝑧 ⊆ (𝑀...𝑘)) |
75 | 74 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → ∃𝑘 ∈ 𝑍 𝑧 ⊆ (𝑀...𝑘)) |
76 | 50 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
77 | | fzfid 12634 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ⊆ (𝑀...𝑘) → (𝑀...𝑘) ∈ Fin) |
78 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ⊆ (𝑀...𝑘) → 𝑧 ⊆ (𝑀...𝑘)) |
79 | | ssfi 8065 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀...𝑘) ∈ Fin ∧ 𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ∈ Fin) |
80 | 77, 78, 79 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ⊆ (𝑀...𝑘) → 𝑧 ∈ Fin) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ∈ Fin) |
82 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ 𝑧) → 𝑂 ∈ OutMeas) |
83 | 3 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ 𝑧) → 𝐴 ⊆ 𝑋) |
84 | 4 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ 𝑧) → (𝑂‘𝐴) ∈ ℝ) |
85 | | inss1 3795 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝐴 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ 𝑧) → (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝐴) |
87 | 82, 2, 83, 84, 86 | omessre 39400 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ 𝑧) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
88 | 81, 87 | fsumrecl 14312 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
89 | 52 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑌 ∈ ℝ) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → 𝑌 ∈ ℝ) |
91 | 88, 90 | readdcld 9948 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ∈ ℝ) |
92 | 91 | ad4ant14 1285 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ∈ ℝ) |
93 | | fzfid 12634 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑀...𝑘) ∈ Fin) |
94 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∩ (𝐹‘𝑛)) ⊆ 𝐴) |
95 | 1, 2, 3, 4, 94 | omessre 39400 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
96 | 95 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
97 | 93, 96 | fsumrecl 14312 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
99 | 89 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑌 ∈ ℝ) |
100 | 98, 99 | readdcld 9948 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ∈ ℝ) |
101 | 100 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ∈ ℝ) |
102 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
103 | 97 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
104 | | fzfid 12634 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑀...𝑘) ∈ Fin) |
105 | 96 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ ℝ) |
106 | | 0xr 9965 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ* |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑘)) → 0 ∈
ℝ*) |
108 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑘)) → +∞ ∈
ℝ*) |
110 | 1, 2, 14 | omecl 39393 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ (0[,]+∞)) |
111 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑘)) → (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ (0[,]+∞)) |
112 | | iccgelb 12101 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧
(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ∈ (0[,]+∞)) → 0 ≤
(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
113 | 107, 109,
111, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝑘)) → 0 ≤ (𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
114 | 113 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) ∧ 𝑛 ∈ (𝑀...𝑘)) → 0 ≤ (𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
115 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → 𝑧 ⊆ (𝑀...𝑘)) |
116 | 104, 105,
114, 115 | fsumless 14369 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) ≤ Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛)))) |
117 | 88, 103, 90, 116 | leadd1dd 10520 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ≤ (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
118 | 117 | ad4ant14 1285 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) ≤ (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
119 | 76, 92, 101, 102, 118 | ltletrd 10076 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) ∧ 𝑧 ⊆ (𝑀...𝑘)) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
120 | 119 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑧 ⊆ (𝑀...𝑘) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
121 | 120 | reximdv 2999 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (∃𝑘 ∈ 𝑍 𝑧 ⊆ (𝑀...𝑘) → ∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
122 | 75, 121 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → ∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
123 | 122 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → ∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
124 | 123 | rexlimdva 3013 |
. . . . . 6
⊢ (𝜑 → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ 𝑧 (𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → ∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
125 | 68, 124 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
126 | 49 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) = (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛)))) |
127 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
128 | 126, 127 | eqbrtrd 4605 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
129 | 128 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
130 | 129 | reximdva 3000 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (𝑂‘∪
𝑛 ∈ 𝑍 (𝐴 ∩ (𝐹‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → ∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌))) |
131 | 125, 130 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
132 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) |
133 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑂 ∈ OutMeas) |
134 | | carageniuncllem2.s |
. . . . . . . . . 10
⊢ 𝑆 = (CaraGen‘𝑂) |
135 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐴 ⊆ 𝑋) |
136 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘𝐴) ∈ ℝ) |
137 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐸:𝑍⟶𝑆) |
138 | | carageniuncllem2.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) |
139 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
140 | 133, 134,
2, 135, 136, 12, 137, 138, 40, 139 | carageniuncllem1 39411 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) = (𝑂‘(𝐴 ∩ (𝐺‘𝑘)))) |
141 | 140 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
142 | 141 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
143 | 132, 142 | breqtrd 4609 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
144 | 143 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌))) |
145 | 144 | reximdva 3000 |
. . . 4
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < (Σ𝑛 ∈ (𝑀...𝑘)(𝑂‘(𝐴 ∩ (𝐹‘𝑛))) + 𝑌) → ∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌))) |
146 | 131, 145 | mpd 15 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
147 | 7 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ) |
148 | 9 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ∈ ℝ) |
149 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐺‘𝑘)) ⊆ 𝐴 |
150 | 149 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 ∩ (𝐺‘𝑘)) ⊆ 𝐴) |
151 | 133, 2, 135, 136, 150 | omessre 39400 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ∈ ℝ) |
152 | 89 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑌 ∈ ℝ) |
153 | 151, 152 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) ∈ ℝ) |
154 | 153 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) ∈ ℝ) |
155 | | difssd 3700 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 ∖ (𝐺‘𝑘)) ⊆ 𝐴) |
156 | 133, 2, 135, 136, 155 | omessre 39400 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘(𝐴 ∖ (𝐺‘𝑘))) ∈ ℝ) |
157 | 156 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∖ (𝐺‘𝑘))) ∈ ℝ) |
158 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
159 | 147, 154,
158 | ltled 10064 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ≤ ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) |
160 | 135 | ssdifssd 3710 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 ∖ (𝐺‘𝑘)) ⊆ 𝑋) |
161 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘)) |
162 | 161 | iuneq1d 4481 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑘 → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖)) |
163 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑀...𝑘) ∈ V |
164 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐸‘𝑖) ∈ V |
165 | 163, 164 | iunex 7039 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖) ∈ V |
166 | 162, 138,
165 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑍 → (𝐺‘𝑘) = ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖)) |
167 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (𝐸‘𝑖) = (𝐸‘𝑛)) |
168 | 167 | cbviunv 4495 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖) = ∪ 𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛) |
169 | 168 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑍 → ∪
𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖) = ∪ 𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛)) |
170 | 166, 169 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 → (𝐺‘𝑘) = ∪ 𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛)) |
171 | | elfzuz 12209 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ (ℤ≥‘𝑀)) |
172 | 12 | eqcomi 2619 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑀) = 𝑍 |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀...𝑘) → (ℤ≥‘𝑀) = 𝑍) |
174 | 171, 173 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀...𝑘) → 𝑖 ∈ 𝑍) |
175 | 174 | ssriv 3572 |
. . . . . . . . . . . . . 14
⊢ (𝑀...𝑘) ⊆ 𝑍 |
176 | | iunss1 4468 |
. . . . . . . . . . . . . 14
⊢ ((𝑀...𝑘) ⊆ 𝑍 → ∪
𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
177 | 175, 176 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛) |
178 | 177 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑍 → ∪
𝑛 ∈ (𝑀...𝑘)(𝐸‘𝑛) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
179 | 170, 178 | eqsstrd 3602 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑍 → (𝐺‘𝑘) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
180 | 179 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ⊆ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
181 | 180 | sscond 3709 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)) ⊆ (𝐴 ∖ (𝐺‘𝑘))) |
182 | 133, 2, 160, 181 | omessle 39388 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ≤ (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) |
183 | 182 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) ≤ (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) |
184 | 147, 148,
154, 157, 159, 183 | le2addd 10525 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘))))) |
185 | 151 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ∈ ℂ) |
186 | 89 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) |
187 | 186 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑌 ∈ ℂ) |
188 | 156 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑂‘(𝐴 ∖ (𝐺‘𝑘))) ∈ ℂ) |
189 | 185, 187,
188 | add32d 10142 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) + 𝑌)) |
190 | | rexadd 11937 |
. . . . . . . . . . . 12
⊢ (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) ∈ ℝ ∧ (𝑂‘(𝐴 ∖ (𝐺‘𝑘))) ∈ ℝ) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘))))) |
191 | 151, 156,
190 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘))))) |
192 | 191 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺‘𝑘))))) |
193 | 138 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))) |
194 | 162 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑛 = 𝑘) → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖)) |
195 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖𝜑 |
196 | 39 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝐸:𝑍⟶𝑆) |
197 | 174 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → 𝑖 ∈ 𝑍) |
198 | 196, 197 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀...𝑘)) → (𝐸‘𝑖) ∈ 𝑆) |
199 | 195, 1, 134, 93, 198 | caragenfiiuncl 39405 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖) ∈ 𝑆) |
200 | 199 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∪
𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖) ∈ 𝑆) |
201 | 193, 194,
139, 200 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = ∪ 𝑖 ∈ (𝑀...𝑘)(𝐸‘𝑖)) |
202 | 201, 200 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝑆) |
203 | 133, 134,
2, 202, 135 | caragensplit 39390 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) +𝑒 (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = (𝑂‘𝐴)) |
204 | 192, 203 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = (𝑂‘𝐴)) |
205 | 204 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) + 𝑌) = ((𝑂‘𝐴) + 𝑌)) |
206 | 189, 205 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = ((𝑂‘𝐴) + 𝑌)) |
207 | 206 | 3adant3 1074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → (((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) + (𝑂‘(𝐴 ∖ (𝐺‘𝑘)))) = ((𝑂‘𝐴) + 𝑌)) |
208 | 184, 207 | breqtrd 4609 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍 ∧ (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌)) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) |
209 | 208 | 3exp 1256 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)))) |
210 | 209 | rexlimdv 3012 |
. . 3
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) < ((𝑂‘(𝐴 ∩ (𝐺‘𝑘))) + 𝑌) → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌))) |
211 | 146, 210 | mpd 15 |
. 2
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) + (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) |
212 | 11, 211 | eqbrtrd 4605 |
1
⊢ (𝜑 → ((𝑂‘(𝐴 ∩ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛))) +𝑒 (𝑂‘(𝐴 ∖ ∪
𝑛 ∈ 𝑍 (𝐸‘𝑛)))) ≤ ((𝑂‘𝐴) + 𝑌)) |