Step | Hyp | Ref
| Expression |
1 | | caratheodorylem1.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
2 | | eluzfz2 12765 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁)) |
4 | | id 22 |
. 2
⊢ (𝜑 → 𝜑) |
5 | | 2fveq3 6543 |
. . . . 5
⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀))) |
6 | | oveq2 7024 |
. . . . . . 7
⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀)) |
7 | 6 | mpteq1d 5049 |
. . . . . 6
⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) |
8 | 7 | fveq2d 6542 |
. . . . 5
⊢ (𝑗 = 𝑀 →
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) =
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))) |
9 | 5, 8 | eqeq12d 2810 |
. . . 4
⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))) |
10 | 9 | imbi2d 342 |
. . 3
⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))) |
11 | | 2fveq3 6543 |
. . . . 5
⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖))) |
12 | | oveq2 7024 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖)) |
13 | 12 | mpteq1d 5049 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) |
14 | 13 | fveq2d 6542 |
. . . . 5
⊢ (𝑗 = 𝑖 →
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) |
15 | 11, 14 | eqeq12d 2810 |
. . . 4
⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))) |
16 | 15 | imbi2d 342 |
. . 3
⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))) |
17 | | 2fveq3 6543 |
. . . . 5
⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1)))) |
18 | | oveq2 7024 |
. . . . . . 7
⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1))) |
19 | 18 | mpteq1d 5049 |
. . . . . 6
⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) |
20 | 19 | fveq2d 6542 |
. . . . 5
⊢ (𝑗 = (𝑖 + 1) →
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))) |
21 | 17, 20 | eqeq12d 2810 |
. . . 4
⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))) |
22 | 21 | imbi2d 342 |
. . 3
⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))) |
23 | | 2fveq3 6543 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁))) |
24 | | oveq2 7024 |
. . . . . . 7
⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁)) |
25 | 24 | mpteq1d 5049 |
. . . . . 6
⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))) |
26 | 25 | fveq2d 6542 |
. . . . 5
⊢ (𝑗 = 𝑁 →
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) =
(Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))) |
27 | 23, 26 | eqeq12d 2810 |
. . . 4
⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))) |
28 | 27 | imbi2d 342 |
. . 3
⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))) |
29 | | eluzel2 12098 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
30 | 1, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
31 | | fzsn 12799 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
33 | 32 | mpteq1d 5049 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) |
34 | 33 | fveq2d 6542 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) =
(Σ^‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))) |
35 | | caratheodorylem1.o |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 ∈ OutMeas) |
36 | 35 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas) |
37 | | eqid 2795 |
. . . . . . . 8
⊢ ∪ dom 𝑂 = ∪ dom 𝑂 |
38 | | caratheodorylem1.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (CaraGen‘𝑂) |
39 | 38 | caragenss 42328 |
. . . . . . . . . . 11
⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂) |
40 | 36, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂) |
41 | | caratheodorylem1.e |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:𝑍⟶𝑆) |
42 | 41 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆) |
43 | | elsni 4489 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀) |
44 | 43 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀) |
45 | | uzid 12108 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
46 | 30, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
47 | | caratheodorylem1.z |
. . . . . . . . . . . . . 14
⊢ 𝑍 =
(ℤ≥‘𝑀) |
48 | 46, 47 | syl6eleqr 2894 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ 𝑍) |
49 | 48 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍) |
50 | 44, 49 | eqeltrd 2883 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍) |
51 | 42, 50 | ffvelrnd 6717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆) |
52 | 40, 51 | sseldd 3890 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂) |
53 | | elssuni 4774 |
. . . . . . . . 9
⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
54 | 52, 53 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
55 | 36, 37, 54 | omecl 42327 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
56 | | eqid 2795 |
. . . . . . 7
⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) |
57 | 55, 56 | fmptd 6741 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞)) |
58 | 30, 57 | sge0sn 42203 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀)) |
59 | | eqidd 2796 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) |
60 | 32 | iuneq1d 4851 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖)) |
61 | | fveq2 6538 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀)) |
62 | 61 | iunxsng 4911 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ 𝑍 → ∪
𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀)) |
63 | 48, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀)) |
64 | | eqidd 2796 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀)) |
65 | 60, 63, 64 | 3eqtrrd 2836 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸‘𝑀) = ∪
𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
66 | 65 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪
𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
67 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀)) |
68 | 67 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀)) |
69 | | caratheodorylem1.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) |
70 | | oveq2 7024 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀)) |
71 | 70 | iuneq1d 4851 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑀 → ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
72 | | ovex 7048 |
. . . . . . . . . . . 12
⊢ (𝑀...𝑀) ∈ V |
73 | | fvex 6551 |
. . . . . . . . . . . 12
⊢ (𝐸‘𝑖) ∈ V |
74 | 72, 73 | iunex 7525 |
. . . . . . . . . . 11
⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V |
75 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V) |
76 | 69, 71, 48, 75 | fvmptd3 6657 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑀) = ∪
𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
77 | 76 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪
𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖)) |
78 | 66, 68, 77 | 3eqtr4d 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀)) |
79 | 78 | fveq2d 6542 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀))) |
80 | | snidg 4504 |
. . . . . . 7
⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀}) |
81 | 48, 80 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ {𝑀}) |
82 | | fvexd 6553 |
. . . . . 6
⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V) |
83 | 59, 79, 81, 82 | fvmptd 6641 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀))) |
84 | 34, 58, 83 | 3eqtrrd 2836 |
. . . 4
⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))) |
85 | 84 | a1i 11 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))) |
86 | | simp3 1131 |
. . . . 5
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑) |
87 | | simp1 1129 |
. . . . 5
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁)) |
88 | | id 22 |
. . . . . . 7
⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))) |
89 | 88 | imp 407 |
. . . . . 6
⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) |
90 | 89 | 3adant1 1123 |
. . . . 5
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) |
91 | | elfzoel1 12886 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ) |
92 | | elfzoelz 12888 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ) |
93 | 92 | peano2zd 11939 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ) |
94 | 91, 93, 93 | 3jca 1121 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈
ℤ)) |
95 | 91 | zred 11936 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ) |
96 | 93 | zred 11936 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ) |
97 | 92 | zred 11936 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ) |
98 | | elfzole1 12896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖) |
99 | 97 | ltp1d 11418 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1)) |
100 | 95, 97, 96, 98, 99 | lelttrd 10645 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1)) |
101 | 95, 96, 100 | ltled 10635 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1)) |
102 | | leid 10583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 + 1) ∈ ℝ →
(𝑖 + 1) ≤ (𝑖 + 1)) |
103 | 96, 102 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1)) |
104 | 94, 101, 103 | jca32 516 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧
(𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1)))) |
105 | | elfz2 12749 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) ↔ ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧
(𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1)))) |
106 | 104, 105 | sylibr 235 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1))) |
107 | 106 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1))) |
108 | | fveq2 6538 |
. . . . . . . . . . . . 13
⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1))) |
109 | 108 | ssiun2s 4871 |
. . . . . . . . . . . 12
⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗)) |
110 | 107, 109 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗)) |
111 | | fveq2 6538 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗)) |
112 | 111 | cbviunv 4866 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) |
113 | 112 | mpteq2i 5052 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 ↦ ∪
𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪
𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)) |
114 | 69, 113 | eqtri 2819 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)) |
115 | | oveq2 7024 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1))) |
116 | 115 | iuneq1d 4851 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗)) |
117 | 30 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ) |
118 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ) |
119 | 118 | peano2zd 11939 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ) |
120 | 117 | zred 11936 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ) |
121 | 119 | zred 11936 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ) |
122 | 118 | zred 11936 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ) |
123 | 98 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖) |
124 | 122 | ltp1d 11418 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1)) |
125 | 120, 122,
121, 123, 124 | lelttrd 10645 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1)) |
126 | 120, 121,
125 | ltled 10635 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1)) |
127 | 117, 119,
126 | 3jca 1121 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1))) |
128 | | eluz2 12099 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 + 1) ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1))) |
129 | 127, 128 | sylibr 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈
(ℤ≥‘𝑀)) |
130 | 47 | eqcomi 2804 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑀) = 𝑍 |
131 | 129, 130 | syl6eleq 2893 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍) |
132 | | ovex 7048 |
. . . . . . . . . . . . . . 15
⊢ (𝑀...(𝑖 + 1)) ∈ V |
133 | | fvex 6551 |
. . . . . . . . . . . . . . 15
⊢ (𝐸‘𝑗) ∈ V |
134 | 132, 133 | iunex 7525 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V) |
136 | 114, 116,
131, 135 | fvmptd3 6657 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪
𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗)) |
137 | 136 | eqcomd 2801 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1))) |
138 | 110, 137 | sseqtrd 3928 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1))) |
139 | | sseqin2 4112 |
. . . . . . . . . . 11
⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1))) |
140 | 139 | biimpi 217 |
. . . . . . . . . 10
⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1))) |
141 | 138, 140 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1))) |
142 | 141 | fveq2d 6542 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1)))) |
143 | | nfcv 2949 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝐸‘(𝑖 + 1)) |
144 | | elfzouz 12892 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ≥‘𝑀)) |
145 | 144 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ≥‘𝑀)) |
146 | 143, 145,
108 | iunp1 40867 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪
𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1)))) |
147 | 136, 146 | eqtrd 2831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪
𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1)))) |
148 | 147 | difeq1d 4019 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1)))) |
149 | | caratheodorylem1.dj |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛)) |
150 | | fveq2 6538 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗)) |
151 | 150 | cbvdisjv 4941 |
. . . . . . . . . . . . . . 15
⊢
(Disj 𝑛
∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗)) |
152 | 149, 151 | sylib 219 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗)) |
153 | 152 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗)) |
154 | | fzssuz 12798 |
. . . . . . . . . . . . . . 15
⊢ (𝑀...𝑖) ⊆ (ℤ≥‘𝑀) |
155 | 154, 130 | sseqtri 3924 |
. . . . . . . . . . . . . 14
⊢ (𝑀...𝑖) ⊆ 𝑍 |
156 | 155 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍) |
157 | | fzp1nel 12841 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(𝑖 + 1) ∈ (𝑀...𝑖) |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖)) |
159 | 158 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖)) |
160 | 131, 159 | eldifd 3870 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖))) |
161 | 153, 156,
160, 108 | disjiun2 40859 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅) |
162 | | undif4 4330 |
. . . . . . . . . . . 12
⊢
((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1)))) |
163 | 161, 162 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1)))) |
164 | 163 | eqcomd 2801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) |
165 | | simpl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑) |
166 | 145, 130 | syl6eleq 2893 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍) |
167 | 114 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪
𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))) |
168 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖) |
169 | 168 | oveq2d 7032 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖)) |
170 | 169 | iuneq1d 4851 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪
𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗)) |
171 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍) |
172 | | ovex 7048 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀...𝑖) ∈ V |
173 | 172, 133 | iunex 7525 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V |
174 | 173 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪
𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V) |
175 | 167, 170,
171, 174 | fvmptd 6641 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗)) |
176 | 165, 166,
175 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗)) |
177 | 176 | eqcomd 2801 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖)) |
178 | | difid 4250 |
. . . . . . . . . . . . 13
⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅ |
179 | 178 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅) |
180 | 177, 179 | uneq12d 4061 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅)) |
181 | | un0 4264 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖) |
182 | 181 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)) |
183 | 180, 182 | eqtrd 2831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖)) |
184 | 148, 164,
183 | 3eqtrd 2835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖)) |
185 | 184 | fveq2d 6542 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖))) |
186 | 142, 185 | oveq12d 7034 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺‘𝑖)))) |
187 | 186 | 3adant3 1125 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺‘𝑖)))) |
188 | 35 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas) |
189 | 41 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆) |
190 | 189, 131 | ffvelrnd 6717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆) |
191 | | simpll 763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑) |
192 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ) |
193 | | elfzelz 12758 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ) |
194 | 193 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ) |
195 | | elfzle1 12760 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗) |
196 | 195 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗) |
197 | 192, 194,
196 | 3jca 1121 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗)) |
198 | | eluz2 12099 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗)) |
199 | 197, 198 | sylibr 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ≥‘𝑀)) |
200 | 199, 130 | syl6eleq 2893 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍) |
201 | 200 | adantll 710 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍) |
202 | 35, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆 ⊆ dom 𝑂) |
203 | 202 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂) |
204 | 41 | ffvelrnda 6716 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆) |
205 | 203, 204 | sseldd 3890 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂) |
206 | | elssuni 4774 |
. . . . . . . . . . . . . 14
⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
207 | 205, 206 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
208 | 191, 201,
207 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
209 | 208 | ralrimiva 3149 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
210 | | iunss 4868 |
. . . . . . . . . . 11
⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom
𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
211 | 209, 210 | sylibr 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
212 | 136, 211 | eqsstrd 3926 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪
dom 𝑂) |
213 | 188, 38, 37, 190, 212 | caragensplit 42324 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1)))) |
214 | 213 | eqcomd 2801 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))) |
215 | 214 | 3adant3 1125 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))) |
216 | 188 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas) |
217 | 165 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑) |
218 | | elfzuz 12754 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ≥‘𝑀)) |
219 | 218, 130 | syl6eleq 2893 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍) |
220 | 219 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍) |
221 | 41, 202 | fssd 6396 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂) |
222 | 221 | ffvelrnda 6716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂) |
223 | 222, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
224 | 217, 220,
223 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom
𝑂) |
225 | 216, 37, 224 | omecl 42327 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞)) |
226 | | 2fveq3 6543 |
. . . . . . . . 9
⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1)))) |
227 | 145, 225,
226 | sge0p1 42238 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) →
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) =
((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1))))) |
228 | 227 | 3adant3 1125 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) →
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) =
((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1))))) |
229 | | id 22 |
. . . . . . . . . 10
⊢ ((𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) |
230 | 229 | eqcomd 2801 |
. . . . . . . . 9
⊢ ((𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) →
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖))) |
231 | 230 | oveq1d 7031 |
. . . . . . . 8
⊢ ((𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) →
((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1))))) |
232 | 231 | 3ad2ant3 1128 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) →
((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1))))) |
233 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑) |
234 | 155 | sseli 3885 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍) |
235 | 234 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍) |
236 | 233, 235,
207 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
237 | 236 | adantlr 711 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
238 | 237 | ralrimiva 3149 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
239 | | iunss 4868 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom
𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
240 | 238, 239 | sylibr 235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪
𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom
𝑂) |
241 | 175, 240 | eqsstrd 3926 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom
𝑂) |
242 | 165, 166,
241 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom
𝑂) |
243 | 188, 37, 242 | omexrcl 42331 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈
ℝ*) |
244 | 110, 211 | sstrd 3899 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪
dom 𝑂) |
245 | 188, 37, 244 | omexrcl 42331 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈
ℝ*) |
246 | 243, 245 | xaddcomd 41133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺‘𝑖)))) |
247 | 246 | 3adant3 1125 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺‘𝑖)))) |
248 | 228, 232,
247 | 3eqtrd 2835 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) →
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺‘𝑖)))) |
249 | 187, 215,
248 | 3eqtr4d 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))) |
250 | 86, 87, 90, 249 | syl3anc 1364 |
. . . 4
⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))) |
251 | 250 | 3exp 1112 |
. . 3
⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) =
(Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))) |
252 | 10, 16, 22, 28, 85, 251 | fzind2 13005 |
. 2
⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))) |
253 | 3, 4, 252 | sylc 65 |
1
⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) =
(Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))) |