Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  caratheodorylem1 Structured version   Visualization version   GIF version

Theorem caratheodorylem1 42350
Description: Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
caratheodorylem1.o (𝜑𝑂 ∈ OutMeas)
caratheodorylem1.s 𝑆 = (CaraGen‘𝑂)
caratheodorylem1.z 𝑍 = (ℤ𝑀)
caratheodorylem1.e (𝜑𝐸:𝑍𝑆)
caratheodorylem1.dj (𝜑Disj 𝑛𝑍 (𝐸𝑛))
caratheodorylem1.g 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
caratheodorylem1.n (𝜑𝑁 ∈ (ℤ𝑀))
Assertion
Ref Expression
caratheodorylem1 (𝜑 → (𝑂‘(𝐺𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛)))))
Distinct variable groups:   𝑖,𝐸,𝑛   𝑖,𝐺,𝑛   𝑖,𝑀,𝑛   𝑖,𝑁,𝑛   𝑖,𝑂,𝑛   𝑛,𝑍   𝜑,𝑖,𝑛
Allowed substitution hints:   𝑆(𝑖,𝑛)   𝑍(𝑖)

Proof of Theorem caratheodorylem1
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 caratheodorylem1.n . . 3 (𝜑𝑁 ∈ (ℤ𝑀))
2 eluzfz2 12765 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
31, 2syl 17 . 2 (𝜑𝑁 ∈ (𝑀...𝑁))
4 id 22 . 2 (𝜑𝜑)
5 2fveq3 6543 . . . . 5 (𝑗 = 𝑀 → (𝑂‘(𝐺𝑗)) = (𝑂‘(𝐺𝑀)))
6 oveq2 7024 . . . . . . 7 (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
76mpteq1d 5049 . . . . . 6 (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛))))
87fveq2d 6542 . . . . 5 (𝑗 = 𝑀 → (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛)))))
95, 8eqeq12d 2810 . . . 4 (𝑗 = 𝑀 → ((𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) ↔ (𝑂‘(𝐺𝑀)) = (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛))))))
109imbi2d 342 . . 3 (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺𝑀)) = (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛)))))))
11 2fveq3 6543 . . . . 5 (𝑗 = 𝑖 → (𝑂‘(𝐺𝑗)) = (𝑂‘(𝐺𝑖)))
12 oveq2 7024 . . . . . . 7 (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
1312mpteq1d 5049 . . . . . 6 (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))
1413fveq2d 6542 . . . . 5 (𝑗 = 𝑖 → (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))))
1511, 14eqeq12d 2810 . . . 4 (𝑗 = 𝑖 → ((𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) ↔ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))))
1615imbi2d 342 . . 3 (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))))))
17 2fveq3 6543 . . . . 5 (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
18 oveq2 7024 . . . . . . 7 (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
1918mpteq1d 5049 . . . . . 6 (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛))))
2019fveq2d 6542 . . . . 5 (𝑗 = (𝑖 + 1) → (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))))
2117, 20eqeq12d 2810 . . . 4 (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛))))))
2221imbi2d 342 . . 3 (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))))))
23 2fveq3 6543 . . . . 5 (𝑗 = 𝑁 → (𝑂‘(𝐺𝑗)) = (𝑂‘(𝐺𝑁)))
24 oveq2 7024 . . . . . . 7 (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
2524mpteq1d 5049 . . . . . 6 (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛))))
2625fveq2d 6542 . . . . 5 (𝑗 = 𝑁 → (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛)))))
2723, 26eqeq12d 2810 . . . 4 (𝑗 = 𝑁 → ((𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛)))) ↔ (𝑂‘(𝐺𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛))))))
2827imbi2d 342 . . 3 (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺𝑗)) = (Σ^‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛)))))))
29 eluzel2 12098 . . . . . . . . 9 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
301, 29syl 17 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
31 fzsn 12799 . . . . . . . 8 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
3230, 31syl 17 . . . . . . 7 (𝜑 → (𝑀...𝑀) = {𝑀})
3332mpteq1d 5049 . . . . . 6 (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛))))
3433fveq2d 6542 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛)))))
35 caratheodorylem1.o . . . . . . . . 9 (𝜑𝑂 ∈ OutMeas)
3635adantr 481 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
37 eqid 2795 . . . . . . . 8 dom 𝑂 = dom 𝑂
38 caratheodorylem1.s . . . . . . . . . . . 12 𝑆 = (CaraGen‘𝑂)
3938caragenss 42328 . . . . . . . . . . 11 (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
4036, 39syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
41 caratheodorylem1.e . . . . . . . . . . . 12 (𝜑𝐸:𝑍𝑆)
4241adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ {𝑀}) → 𝐸:𝑍𝑆)
43 elsni 4489 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
4443adantl 482 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
45 uzid 12108 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
4630, 45syl 17 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ𝑀))
47 caratheodorylem1.z . . . . . . . . . . . . . 14 𝑍 = (ℤ𝑀)
4846, 47syl6eleqr 2894 . . . . . . . . . . . . 13 (𝜑𝑀𝑍)
4948adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ {𝑀}) → 𝑀𝑍)
5044, 49eqeltrd 2883 . . . . . . . . . . 11 ((𝜑𝑛 ∈ {𝑀}) → 𝑛𝑍)
5142, 50ffvelrnd 6717 . . . . . . . . . 10 ((𝜑𝑛 ∈ {𝑀}) → (𝐸𝑛) ∈ 𝑆)
5240, 51sseldd 3890 . . . . . . . . 9 ((𝜑𝑛 ∈ {𝑀}) → (𝐸𝑛) ∈ dom 𝑂)
53 elssuni 4774 . . . . . . . . 9 ((𝐸𝑛) ∈ dom 𝑂 → (𝐸𝑛) ⊆ dom 𝑂)
5452, 53syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ {𝑀}) → (𝐸𝑛) ⊆ dom 𝑂)
5536, 37, 54omecl 42327 . . . . . . 7 ((𝜑𝑛 ∈ {𝑀}) → (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞))
56 eqid 2795 . . . . . . 7 (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛)))
5755, 56fmptd 6741 . . . . . 6 (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛))):{𝑀}⟶(0[,]+∞))
5830, 57sge0sn 42203 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛)))‘𝑀))
59 eqidd 2796 . . . . . 6 (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛))))
6032iuneq1d 4851 . . . . . . . . . 10 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) = 𝑖 ∈ {𝑀} (𝐸𝑖))
61 fveq2 6538 . . . . . . . . . . . 12 (𝑖 = 𝑀 → (𝐸𝑖) = (𝐸𝑀))
6261iunxsng 4911 . . . . . . . . . . 11 (𝑀𝑍 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
6348, 62syl 17 . . . . . . . . . 10 (𝜑 𝑖 ∈ {𝑀} (𝐸𝑖) = (𝐸𝑀))
64 eqidd 2796 . . . . . . . . . 10 (𝜑 → (𝐸𝑀) = (𝐸𝑀))
6560, 63, 643eqtrrd 2836 . . . . . . . . 9 (𝜑 → (𝐸𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
6665adantr 481 . . . . . . . 8 ((𝜑𝑛 = 𝑀) → (𝐸𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
67 fveq2 6538 . . . . . . . . 9 (𝑛 = 𝑀 → (𝐸𝑛) = (𝐸𝑀))
6867adantl 482 . . . . . . . 8 ((𝜑𝑛 = 𝑀) → (𝐸𝑛) = (𝐸𝑀))
69 caratheodorylem1.g . . . . . . . . . 10 𝐺 = (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖))
70 oveq2 7024 . . . . . . . . . . 11 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
7170iuneq1d 4851 . . . . . . . . . 10 (𝑛 = 𝑀 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
72 ovex 7048 . . . . . . . . . . . 12 (𝑀...𝑀) ∈ V
73 fvex 6551 . . . . . . . . . . . 12 (𝐸𝑖) ∈ V
7472, 73iunex 7525 . . . . . . . . . . 11 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V
7574a1i 11 . . . . . . . . . 10 (𝜑 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖) ∈ V)
7669, 71, 48, 75fvmptd3 6657 . . . . . . . . 9 (𝜑 → (𝐺𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
7776adantr 481 . . . . . . . 8 ((𝜑𝑛 = 𝑀) → (𝐺𝑀) = 𝑖 ∈ (𝑀...𝑀)(𝐸𝑖))
7866, 68, 773eqtr4d 2841 . . . . . . 7 ((𝜑𝑛 = 𝑀) → (𝐸𝑛) = (𝐺𝑀))
7978fveq2d 6542 . . . . . 6 ((𝜑𝑛 = 𝑀) → (𝑂‘(𝐸𝑛)) = (𝑂‘(𝐺𝑀)))
80 snidg 4504 . . . . . . 7 (𝑀𝑍𝑀 ∈ {𝑀})
8148, 80syl 17 . . . . . 6 (𝜑𝑀 ∈ {𝑀})
82 fvexd 6553 . . . . . 6 (𝜑 → (𝑂‘(𝐺𝑀)) ∈ V)
8359, 79, 81, 82fvmptd 6641 . . . . 5 (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸𝑛)))‘𝑀) = (𝑂‘(𝐺𝑀)))
8434, 58, 833eqtrrd 2836 . . . 4 (𝜑 → (𝑂‘(𝐺𝑀)) = (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛)))))
8584a1i 11 . . 3 (𝑁 ∈ (ℤ𝑀) → (𝜑 → (𝑂‘(𝐺𝑀)) = (Σ^‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸𝑛))))))
86 simp3 1131 . . . . 5 ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) ∧ 𝜑) → 𝜑)
87 simp1 1129 . . . . 5 ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
88 id 22 . . . . . . 7 ((𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))))
8988imp 407 . . . . . 6 (((𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))))
90893adant1 1123 . . . . 5 ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))))
91 elfzoel1 12886 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
92 elfzoelz 12888 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
9392peano2zd 11939 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
9491, 93, 933jca 1121 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑁) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
9591zred 11936 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
9693zred 11936 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
9792zred 11936 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
98 elfzole1 12896 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑀..^𝑁) → 𝑀𝑖)
9997ltp1d 11418 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
10095, 97, 96, 98, 99lelttrd 10645 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
10195, 96, 100ltled 10635 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
102 leid 10583 . . . . . . . . . . . . . . . 16 ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
10396, 102syl 17 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
10494, 101, 103jca32 516 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑁) → ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1))))
105 elfz2 12749 . . . . . . . . . . . . . 14 ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) ↔ ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1))))
106104, 105sylibr 235 . . . . . . . . . . . . 13 (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
107106adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
108 fveq2 6538 . . . . . . . . . . . . 13 (𝑗 = (𝑖 + 1) → (𝐸𝑗) = (𝐸‘(𝑖 + 1)))
109108ssiun2s 4871 . . . . . . . . . . . 12 ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗))
110107, 109syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗))
111 fveq2 6538 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → (𝐸𝑖) = (𝐸𝑗))
112111cbviunv 4866 . . . . . . . . . . . . . . 15 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖) = 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗)
113112mpteq2i 5052 . . . . . . . . . . . . . 14 (𝑛𝑍 𝑖 ∈ (𝑀...𝑛)(𝐸𝑖)) = (𝑛𝑍 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗))
11469, 113eqtri 2819 . . . . . . . . . . . . 13 𝐺 = (𝑛𝑍 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗))
115 oveq2 7024 . . . . . . . . . . . . . 14 (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
116115iuneq1d 4851 . . . . . . . . . . . . 13 (𝑛 = (𝑖 + 1) → 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗) = 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗))
11730adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
11892adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
119118peano2zd 11939 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
120117zred 11936 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
121119zred 11936 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
122118zred 11936 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
12398adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑀𝑖)
124122ltp1d 11418 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
125120, 122, 121, 123, 124lelttrd 10645 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
126120, 121, 125ltled 10635 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
127117, 119, 1263jca 1121 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
128 eluz2 12099 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
129127, 128sylibr 235 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ𝑀))
13047eqcomi 2804 . . . . . . . . . . . . . 14 (ℤ𝑀) = 𝑍
131129, 130syl6eleq 2893 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
132 ovex 7048 . . . . . . . . . . . . . . 15 (𝑀...(𝑖 + 1)) ∈ V
133 fvex 6551 . . . . . . . . . . . . . . 15 (𝐸𝑗) ∈ V
134132, 133iunex 7525 . . . . . . . . . . . . . 14 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ∈ V
135134a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ∈ V)
136114, 116, 131, 135fvmptd3 6657 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗))
137136eqcomd 2801 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) = (𝐺‘(𝑖 + 1)))
138110, 137sseqtrd 3928 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
139 sseqin2 4112 . . . . . . . . . . 11 ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
140139biimpi 217 . . . . . . . . . 10 ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
141138, 140syl 17 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
142141fveq2d 6542 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
143 nfcv 2949 . . . . . . . . . . . . 13 𝑗(𝐸‘(𝑖 + 1))
144 elfzouz 12892 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ𝑀))
145144adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ𝑀))
146143, 145, 108iunp1 40867 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) = ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))))
147136, 146eqtrd 2831 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))))
148147difeq1d 4019 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
149 caratheodorylem1.dj . . . . . . . . . . . . . . 15 (𝜑Disj 𝑛𝑍 (𝐸𝑛))
150 fveq2 6538 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑗 → (𝐸𝑛) = (𝐸𝑗))
151150cbvdisjv 4941 . . . . . . . . . . . . . . 15 (Disj 𝑛𝑍 (𝐸𝑛) ↔ Disj 𝑗𝑍 (𝐸𝑗))
152149, 151sylib 219 . . . . . . . . . . . . . 14 (𝜑Disj 𝑗𝑍 (𝐸𝑗))
153152adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗𝑍 (𝐸𝑗))
154 fzssuz 12798 . . . . . . . . . . . . . . 15 (𝑀...𝑖) ⊆ (ℤ𝑀)
155154, 130sseqtri 3924 . . . . . . . . . . . . . 14 (𝑀...𝑖) ⊆ 𝑍
156155a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
157 fzp1nel 12841 . . . . . . . . . . . . . . . 16 ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
158157a1i 11 . . . . . . . . . . . . . . 15 (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
159158adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
160131, 159eldifd 3870 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
161153, 156, 160, 108disjiun2 40859 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
162 undif4 4330 . . . . . . . . . . . 12 (( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
163161, 162syl 17 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
164163eqcomd 2801 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
165 simpl 483 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
166145, 130syl6eleq 2893 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑖𝑍)
167114a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → 𝐺 = (𝑛𝑍 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗)))
168 simpr 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
169168oveq2d 7032 . . . . . . . . . . . . . . . 16 (((𝜑𝑖𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
170169iuneq1d 4851 . . . . . . . . . . . . . . 15 (((𝜑𝑖𝑍) ∧ 𝑛 = 𝑖) → 𝑗 ∈ (𝑀...𝑛)(𝐸𝑗) = 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗))
171 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → 𝑖𝑍)
172 ovex 7048 . . . . . . . . . . . . . . . . 17 (𝑀...𝑖) ∈ V
173172, 133iunex 7525 . . . . . . . . . . . . . . . 16 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∈ V
174173a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∈ V)
175167, 170, 171, 174fvmptd 6641 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑍) → (𝐺𝑖) = 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗))
176165, 166, 175syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐺𝑖) = 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗))
177176eqcomd 2801 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) = (𝐺𝑖))
178 difid 4250 . . . . . . . . . . . . 13 ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
179178a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
180177, 179uneq12d 4061 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺𝑖) ∪ ∅))
181 un0 4264 . . . . . . . . . . . 12 ((𝐺𝑖) ∪ ∅) = (𝐺𝑖)
182181a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝐺𝑖) ∪ ∅) = (𝐺𝑖))
183180, 182eqtrd 2831 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺𝑖))
184148, 164, 1833eqtrd 2835 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺𝑖))
185184fveq2d 6542 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺𝑖)))
186142, 185oveq12d 7034 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺𝑖))))
1871863adant3 1125 . . . . . 6 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺𝑖))))
18835adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
18941adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍𝑆)
190189, 131ffvelrnd 6717 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
191 simpll 763 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
19291adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
193 elfzelz 12758 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
194193adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
195 elfzle1 12760 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀𝑗)
196195adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀𝑗)
197192, 194, 1963jca 1121 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀𝑗))
198 eluz2 12099 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀𝑗))
199197, 198sylibr 235 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ𝑀))
200199, 130syl6eleq 2893 . . . . . . . . . . . . . 14 ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗𝑍)
201200adantll 710 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗𝑍)
20235, 39syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑆 ⊆ dom 𝑂)
203202adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍) → 𝑆 ⊆ dom 𝑂)
20441ffvelrnda 6716 . . . . . . . . . . . . . . 15 ((𝜑𝑗𝑍) → (𝐸𝑗) ∈ 𝑆)
205203, 204sseldd 3890 . . . . . . . . . . . . . 14 ((𝜑𝑗𝑍) → (𝐸𝑗) ∈ dom 𝑂)
206 elssuni 4774 . . . . . . . . . . . . . 14 ((𝐸𝑗) ∈ dom 𝑂 → (𝐸𝑗) ⊆ dom 𝑂)
207205, 206syl 17 . . . . . . . . . . . . 13 ((𝜑𝑗𝑍) → (𝐸𝑗) ⊆ dom 𝑂)
208191, 201, 207syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸𝑗) ⊆ dom 𝑂)
209208ralrimiva 3149 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ⊆ dom 𝑂)
210 iunss 4868 . . . . . . . . . . 11 ( 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ⊆ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ⊆ dom 𝑂)
211209, 210sylibr 235 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸𝑗) ⊆ dom 𝑂)
212136, 211eqsstrd 3926 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ dom 𝑂)
213188, 38, 37, 190, 212caragensplit 42324 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
214213eqcomd 2801 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
2152143adant3 1125 . . . . . 6 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
216188adantr 481 . . . . . . . . . 10 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
217165adantr 481 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
218 elfzuz 12754 . . . . . . . . . . . . 13 (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ𝑀))
219218, 130syl6eleq 2893 . . . . . . . . . . . 12 (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛𝑍)
220219adantl 482 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛𝑍)
22141, 202fssd 6396 . . . . . . . . . . . . 13 (𝜑𝐸:𝑍⟶dom 𝑂)
222221ffvelrnda 6716 . . . . . . . . . . . 12 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ dom 𝑂)
223222, 53syl 17 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ dom 𝑂)
224217, 220, 223syl2anc 584 . . . . . . . . . 10 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸𝑛) ⊆ dom 𝑂)
225216, 37, 224omecl 42327 . . . . . . . . 9 (((𝜑𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞))
226 2fveq3 6543 . . . . . . . . 9 (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
227145, 225, 226sge0p1 42238 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))) = ((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
2282273adant3 1125 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))) = ((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
229 id 22 . . . . . . . . . 10 ((𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))))
230229eqcomd 2801 . . . . . . . . 9 ((𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) → (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) = (𝑂‘(𝐺𝑖)))
231230oveq1d 7031 . . . . . . . 8 ((𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) → ((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
2322313ad2ant3 1128 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → ((Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛)))) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
233 simpl 483 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...𝑖)) → 𝜑)
234155sseli 3885 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (𝑀...𝑖) → 𝑗𝑍)
235234adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝑀...𝑖)) → 𝑗𝑍)
236233, 235, 207syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (𝑀...𝑖)) → (𝐸𝑗) ⊆ dom 𝑂)
237236adantlr 711 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸𝑗) ⊆ dom 𝑂)
238237ralrimiva 3149 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ⊆ dom 𝑂)
239 iunss 4868 . . . . . . . . . . . . 13 ( 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ⊆ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ⊆ dom 𝑂)
240238, 239sylibr 235 . . . . . . . . . . . 12 ((𝜑𝑖𝑍) → 𝑗 ∈ (𝑀...𝑖)(𝐸𝑗) ⊆ dom 𝑂)
241175, 240eqsstrd 3926 . . . . . . . . . . 11 ((𝜑𝑖𝑍) → (𝐺𝑖) ⊆ dom 𝑂)
242165, 166, 241syl2anc 584 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐺𝑖) ⊆ dom 𝑂)
243188, 37, 242omexrcl 42331 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺𝑖)) ∈ ℝ*)
244110, 211sstrd 3899 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ dom 𝑂)
245188, 37, 244omexrcl 42331 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ*)
246243, 245xaddcomd 41133 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺𝑖))))
2472463adant3 1125 . . . . . . 7 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → ((𝑂‘(𝐺𝑖)) +𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺𝑖))))
248228, 232, 2473eqtrd 2835 . . . . . 6 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +𝑒 (𝑂‘(𝐺𝑖))))
249187, 215, 2483eqtr4d 2841 . . . . 5 ((𝜑𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))))
25086, 87, 90, 249syl3anc 1364 . . . 4 ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))))
2512503exp 1112 . . 3 (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺𝑖)) = (Σ^‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸𝑛)))))))
25210, 16, 22, 28, 85, 251fzind2 13005 . 2 (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛))))))
2533, 4, 252sylc 65 1 (𝜑 → (𝑂‘(𝐺𝑁)) = (Σ^‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸𝑛)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1080   = wceq 1522  wcel 2081  wral 3105  Vcvv 3437  cdif 3856  cun 3857  cin 3858  wss 3859  c0 4211  {csn 4472   cuni 4745   ciun 4825  Disj wdisj 4930   class class class wbr 4962  cmpt 5041  dom cdm 5443  wf 6221  cfv 6225  (class class class)co 7016  cr 10382  0cc0 10383  1c1 10384   + caddc 10386  +∞cpnf 10518  cle 10522  cz 11829  cuz 12093   +𝑒 cxad 12355  [,]cicc 12591  ...cfz 12742  ..^cfzo 12883  Σ^csumge0 42186  OutMeascome 42313  CaraGenccaragen 42315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460  ax-pre-sup 10461
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-disj 4931  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-se 5403  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-isom 6234  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-fin 8361  df-sup 8752  df-oi 8820  df-card 9214  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-div 11146  df-nn 11487  df-2 11548  df-3 11549  df-n0 11746  df-z 11830  df-uz 12094  df-rp 12240  df-xadd 12358  df-ico 12594  df-icc 12595  df-fz 12743  df-fzo 12884  df-seq 13220  df-exp 13280  df-hash 13541  df-cj 14292  df-re 14293  df-im 14294  df-sqrt 14428  df-abs 14429  df-clim 14679  df-sum 14877  df-sumge0 42187  df-ome 42314  df-caragen 42316
This theorem is referenced by:  caratheodorylem2  42351
  Copyright terms: Public domain W3C validator