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

Theorem meaiuninclem 46101
Description: Measures are continuous from below (bounded case): if 𝐸 is a sequence of increasing measurable sets (with uniformly bounded measure) then the measure of the union is the union of the measure. This is Proposition 112C (e) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
Hypotheses
Ref Expression
meaiuninclem.m (𝜑𝑀 ∈ Meas)
meaiuninclem.n (𝜑𝑁 ∈ ℤ)
meaiuninclem.z 𝑍 = (ℤ𝑁)
meaiuninclem.e (𝜑𝐸:𝑍⟶dom 𝑀)
meaiuninclem.i ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ (𝐸‘(𝑛 + 1)))
meaiuninclem.b (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥)
meaiuninclem.s 𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
meaiuninclem.f 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
Assertion
Ref Expression
meaiuninclem (𝜑𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)))
Distinct variable groups:   𝑖,𝐸,𝑛,𝑥   𝑖,𝐹,𝑛,𝑥   𝑖,𝑀,𝑛,𝑥   𝑖,𝑁,𝑛,𝑥   𝑆,𝑛,𝑥   𝑖,𝑍,𝑛,𝑥   𝜑,𝑖,𝑛,𝑥
Allowed substitution hint:   𝑆(𝑖)

Proof of Theorem meaiuninclem
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 meaiuninclem.z . . 3 𝑍 = (ℤ𝑁)
2 meaiuninclem.n . . 3 (𝜑𝑁 ∈ ℤ)
3 0xr 11311 . . . . . . 7 0 ∈ ℝ*
43a1i 11 . . . . . 6 ((𝜑𝑛𝑍) → 0 ∈ ℝ*)
5 pnfxr 11318 . . . . . . 7 +∞ ∈ ℝ*
65a1i 11 . . . . . 6 ((𝜑𝑛𝑍) → +∞ ∈ ℝ*)
7 meaiuninclem.m . . . . . . . 8 (𝜑𝑀 ∈ Meas)
87adantr 479 . . . . . . 7 ((𝜑𝑛𝑍) → 𝑀 ∈ Meas)
9 eqid 2726 . . . . . . 7 dom 𝑀 = dom 𝑀
10 meaiuninclem.e . . . . . . . 8 (𝜑𝐸:𝑍⟶dom 𝑀)
1110ffvelcdmda 7098 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ dom 𝑀)
128, 9, 11meaxrcl 46082 . . . . . 6 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) ∈ ℝ*)
138, 11meage0 46096 . . . . . 6 ((𝜑𝑛𝑍) → 0 ≤ (𝑀‘(𝐸𝑛)))
14 meaiuninclem.b . . . . . . . 8 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥)
1514adantr 479 . . . . . . 7 ((𝜑𝑛𝑍) → ∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥)
16 simp1 1133 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝜑𝑛𝑍))
17 simp2 1134 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ)
18 simp3 1135 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥)
1916simprd 494 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → 𝑛𝑍)
20 rspa 3236 . . . . . . . . . . 11 ((∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥𝑛𝑍) → (𝑀‘(𝐸𝑛)) ≤ 𝑥)
2118, 19, 20syl2anc 582 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝑀‘(𝐸𝑛)) ≤ 𝑥)
22123ad2ant1 1130 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝑀‘(𝐸𝑛)) ∈ ℝ*)
23 rexr 11310 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
24233ad2ant2 1131 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → 𝑥 ∈ ℝ*)
255a1i 11 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → +∞ ∈ ℝ*)
26 simp3 1135 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝑀‘(𝐸𝑛)) ≤ 𝑥)
27 ltpnf 13154 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑥 < +∞)
28273ad2ant2 1131 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → 𝑥 < +∞)
2922, 24, 25, 26, 28xrlelttrd 13193 . . . . . . . . . 10 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝑀‘(𝐸𝑛)) < +∞)
3016, 17, 21, 29syl3anc 1368 . . . . . . . . 9 (((𝜑𝑛𝑍) ∧ 𝑥 ∈ ℝ ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → (𝑀‘(𝐸𝑛)) < +∞)
31303exp 1116 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝑥 ∈ ℝ → (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → (𝑀‘(𝐸𝑛)) < +∞)))
3231rexlimdv 3143 . . . . . . 7 ((𝜑𝑛𝑍) → (∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → (𝑀‘(𝐸𝑛)) < +∞))
3315, 32mpd 15 . . . . . 6 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) < +∞)
344, 6, 12, 13, 33elicod 13428 . . . . 5 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) ∈ (0[,)+∞))
35 meaiuninclem.s . . . . 5 𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛)))
3634, 35fmptd 7128 . . . 4 (𝜑𝑆:𝑍⟶(0[,)+∞))
37 rge0ssre 13487 . . . . 5 (0[,)+∞) ⊆ ℝ
3837a1i 11 . . . 4 (𝜑 → (0[,)+∞) ⊆ ℝ)
3936, 38fssd 6745 . . 3 (𝜑𝑆:𝑍⟶ℝ)
401peano2uzs 12938 . . . . . . 7 (𝑛𝑍 → (𝑛 + 1) ∈ 𝑍)
4140adantl 480 . . . . . 6 ((𝜑𝑛𝑍) → (𝑛 + 1) ∈ 𝑍)
4210ffvelcdmda 7098 . . . . . 6 ((𝜑 ∧ (𝑛 + 1) ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
4341, 42syldan 589 . . . . 5 ((𝜑𝑛𝑍) → (𝐸‘(𝑛 + 1)) ∈ dom 𝑀)
44 meaiuninclem.i . . . . 5 ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ (𝐸‘(𝑛 + 1)))
458, 9, 11, 43, 44meassle 46084 . . . 4 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1))))
4635a1i 11 . . . . . 6 (𝜑𝑆 = (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))))
47 fvexd 6916 . . . . . 6 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) ∈ V)
4846, 47fvmpt2d 7022 . . . . 5 ((𝜑𝑛𝑍) → (𝑆𝑛) = (𝑀‘(𝐸𝑛)))
49 2fveq3 6906 . . . . . . . 8 (𝑛 = 𝑚 → (𝑀‘(𝐸𝑛)) = (𝑀‘(𝐸𝑚)))
5049cbvmptv 5266 . . . . . . 7 (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) = (𝑚𝑍 ↦ (𝑀‘(𝐸𝑚)))
5135, 50eqtri 2754 . . . . . 6 𝑆 = (𝑚𝑍 ↦ (𝑀‘(𝐸𝑚)))
52 2fveq3 6906 . . . . . 6 (𝑚 = (𝑛 + 1) → (𝑀‘(𝐸𝑚)) = (𝑀‘(𝐸‘(𝑛 + 1))))
53 fvexd 6916 . . . . . 6 ((𝜑𝑛𝑍) → (𝑀‘(𝐸‘(𝑛 + 1))) ∈ V)
5451, 52, 41, 53fvmptd3 7032 . . . . 5 ((𝜑𝑛𝑍) → (𝑆‘(𝑛 + 1)) = (𝑀‘(𝐸‘(𝑛 + 1))))
5548, 54breq12d 5166 . . . 4 ((𝜑𝑛𝑍) → ((𝑆𝑛) ≤ (𝑆‘(𝑛 + 1)) ↔ (𝑀‘(𝐸𝑛)) ≤ (𝑀‘(𝐸‘(𝑛 + 1)))))
5645, 55mpbird 256 . . 3 ((𝜑𝑛𝑍) → (𝑆𝑛) ≤ (𝑆‘(𝑛 + 1)))
5748eqcomd 2732 . . . . . . . . 9 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) = (𝑆𝑛))
5857breq1d 5163 . . . . . . . 8 ((𝜑𝑛𝑍) → ((𝑀‘(𝐸𝑛)) ≤ 𝑥 ↔ (𝑆𝑛) ≤ 𝑥))
5958ralbidva 3166 . . . . . . 7 (𝜑 → (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 ↔ ∀𝑛𝑍 (𝑆𝑛) ≤ 𝑥))
6059biimpd 228 . . . . . 6 (𝜑 → (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∀𝑛𝑍 (𝑆𝑛) ≤ 𝑥))
6160adantr 479 . . . . 5 ((𝜑𝑥 ∈ ℝ) → (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∀𝑛𝑍 (𝑆𝑛) ≤ 𝑥))
6261reximdva 3158 . . . 4 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑆𝑛) ≤ 𝑥))
6314, 62mpd 15 . . 3 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑆𝑛) ≤ 𝑥)
641, 2, 39, 56, 63climsup 15674 . 2 (𝜑𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
65 nfv 1910 . . . . . 6 𝑛𝜑
66 nfv 1910 . . . . . 6 𝑥𝜑
67 id 22 . . . . . . . . . . 11 (𝑛𝑍𝑛𝑍)
68 fvex 6914 . . . . . . . . . . . . 13 (𝐸𝑛) ∈ V
6968difexi 5335 . . . . . . . . . . . 12 ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V
7069a1i 11 . . . . . . . . . . 11 (𝑛𝑍 → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V)
71 meaiuninclem.f . . . . . . . . . . . 12 𝐹 = (𝑛𝑍 ↦ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
7271fvmpt2 7020 . . . . . . . . . . 11 ((𝑛𝑍 ∧ ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ V) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
7367, 70, 72syl2anc 582 . . . . . . . . . 10 (𝑛𝑍 → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
7473adantl 480 . . . . . . . . 9 ((𝜑𝑛𝑍) → (𝐹𝑛) = ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)))
757, 9dmmeasal 46073 . . . . . . . . . . 11 (𝜑 → dom 𝑀 ∈ SAlg)
7675adantr 479 . . . . . . . . . 10 ((𝜑𝑛𝑍) → dom 𝑀 ∈ SAlg)
77 fzoct 44999 . . . . . . . . . . . 12 (𝑁..^𝑛) ≼ ω
7877a1i 11 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → (𝑁..^𝑛) ≼ ω)
7910adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑁..^𝑛)) → 𝐸:𝑍⟶dom 𝑀)
80 fzossuz 44996 . . . . . . . . . . . . . . . 16 (𝑁..^𝑛) ⊆ (ℤ𝑁)
811eqcomi 2735 . . . . . . . . . . . . . . . 16 (ℤ𝑁) = 𝑍
8280, 81sseqtri 4016 . . . . . . . . . . . . . . 15 (𝑁..^𝑛) ⊆ 𝑍
8382sseli 3975 . . . . . . . . . . . . . 14 (𝑖 ∈ (𝑁..^𝑛) → 𝑖𝑍)
8483adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (𝑁..^𝑛)) → 𝑖𝑍)
8579, 84ffvelcdmd 7099 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (𝑁..^𝑛)) → (𝐸𝑖) ∈ dom 𝑀)
8685adantlr 713 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸𝑖) ∈ dom 𝑀)
8776, 78, 86saliuncl 45944 . . . . . . . . . 10 ((𝜑𝑛𝑍) → 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) ∈ dom 𝑀)
88 saldifcl2 45949 . . . . . . . . . 10 ((dom 𝑀 ∈ SAlg ∧ (𝐸𝑛) ∈ dom 𝑀 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖) ∈ dom 𝑀) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ dom 𝑀)
8976, 11, 87, 88syl3anc 1368 . . . . . . . . 9 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ∈ dom 𝑀)
9074, 89eqeltrd 2826 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ dom 𝑀)
918, 9, 90meaxrcl 46082 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑀‘(𝐹𝑛)) ∈ ℝ*)
928, 90meage0 46096 . . . . . . 7 ((𝜑𝑛𝑍) → 0 ≤ (𝑀‘(𝐹𝑛)))
93 difssd 4132 . . . . . . . . . 10 ((𝜑𝑛𝑍) → ((𝐸𝑛) ∖ 𝑖 ∈ (𝑁..^𝑛)(𝐸𝑖)) ⊆ (𝐸𝑛))
9474, 93eqsstrd 4018 . . . . . . . . 9 ((𝜑𝑛𝑍) → (𝐹𝑛) ⊆ (𝐸𝑛))
958, 9, 90, 11, 94meassle 46084 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝑀‘(𝐹𝑛)) ≤ (𝑀‘(𝐸𝑛)))
9691, 12, 6, 95, 33xrlelttrd 13193 . . . . . . 7 ((𝜑𝑛𝑍) → (𝑀‘(𝐹𝑛)) < +∞)
974, 6, 91, 92, 96elicod 13428 . . . . . 6 ((𝜑𝑛𝑍) → (𝑀‘(𝐹𝑛)) ∈ (0[,)+∞))
98 2fveq3 6906 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 → (𝑀‘(𝐸𝑛)) = (𝑀‘(𝐸𝑖)))
9998breq1d 5163 . . . . . . . . . . . . 13 (𝑛 = 𝑖 → ((𝑀‘(𝐸𝑛)) ≤ 𝑥 ↔ (𝑀‘(𝐸𝑖)) ≤ 𝑥))
10099cbvralvw 3225 . . . . . . . . . . . 12 (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 ↔ ∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥)
101100biimpi 215 . . . . . . . . . . 11 (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥)
102101adantl 480 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → ∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥)
103 eleq1w 2809 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → (𝑛𝑍𝑖𝑍))
104103anbi2d 628 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → ((𝜑𝑛𝑍) ↔ (𝜑𝑖𝑍)))
105 oveq2 7432 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑖 → (𝑁...𝑛) = (𝑁...𝑖))
106105sumeq1d 15705 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑖 → Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚)))
10798, 106eqeq12d 2742 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑖 → ((𝑀‘(𝐸𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚)) ↔ (𝑀‘(𝐸𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚))))
108104, 107imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑖 → (((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚))) ↔ ((𝜑𝑖𝑍) → (𝑀‘(𝐸𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚)))))
109 eleq1w 2809 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 → (𝑚𝑍𝑛𝑍))
110109anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ((𝜑𝑚𝑍) ↔ (𝜑𝑛𝑍)))
111 oveq2 7432 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑛 → (𝑁...𝑚) = (𝑁...𝑛))
112111iuneq1d 5028 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖))
113111iuneq1d 5028 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑛 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖) = 𝑖 ∈ (𝑁...𝑛)(𝐸𝑖))
114112, 113eqeq12d 2742 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑛 → ( 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖) ↔ 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑛)(𝐸𝑖)))
115110, 114imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (((𝜑𝑚𝑍) → 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖)) ↔ ((𝜑𝑛𝑍) → 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑛)(𝐸𝑖))))
116 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = 𝑛 → (𝐹𝑖) = (𝐹𝑛))
117116cbviunv 5048 . . . . . . . . . . . . . . . . . . . . . 22 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛)
118117a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛))
11965, 1, 10, 71iundjiun 46081 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛)) ∧ Disj 𝑛𝑍 (𝐹𝑛)))
120119simplld 766 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
121120adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → ∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
122 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑚𝑍) → 𝑚𝑍)
123 rspa 3236 . . . . . . . . . . . . . . . . . . . . . 22 ((∀𝑚𝑍 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) ∧ 𝑚𝑍) → 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
124121, 122, 123syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → 𝑛 ∈ (𝑁...𝑚)(𝐹𝑛) = 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛))
125 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝐸𝑛) = (𝐸𝑖))
126125cbviunv 5048 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) = 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖)
127126a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑚𝑍) → 𝑛 ∈ (𝑁...𝑚)(𝐸𝑛) = 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖))
128118, 124, 1273eqtrd 2770 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚𝑍) → 𝑖 ∈ (𝑁...𝑚)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑚)(𝐸𝑖))
129115, 128chvarvv 1995 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝑍) → 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖) = 𝑖 ∈ (𝑁...𝑛)(𝐸𝑖))
13067, 1eleqtrdi 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑛𝑍𝑛 ∈ (ℤ𝑁))
131130adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑛𝑍) → 𝑛 ∈ (ℤ𝑁))
132 fvoveq1 7447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑖 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑖 + 1)))
133125, 132sseq12d 4013 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → ((𝐸𝑛) ⊆ (𝐸‘(𝑛 + 1)) ↔ (𝐸𝑖) ⊆ (𝐸‘(𝑖 + 1))))
134104, 133imbi12d 343 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ (𝐸‘(𝑛 + 1))) ↔ ((𝜑𝑖𝑍) → (𝐸𝑖) ⊆ (𝐸‘(𝑖 + 1)))))
135134, 44chvarvv 1995 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖𝑍) → (𝐸𝑖) ⊆ (𝐸‘(𝑖 + 1)))
13684, 135syldan 589 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (𝑁..^𝑛)) → (𝐸𝑖) ⊆ (𝐸‘(𝑖 + 1)))
137136adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛𝑍) ∧ 𝑖 ∈ (𝑁..^𝑛)) → (𝐸𝑖) ⊆ (𝐸‘(𝑖 + 1)))
138131, 137iunincfi 44695 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝑍) → 𝑖 ∈ (𝑁...𝑛)(𝐸𝑖) = (𝐸𝑛))
139129, 138eqtr2d 2767 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (𝐸𝑛) = 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖))
140139fveq2d 6905 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) = (𝑀 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖)))
141 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑖(𝜑𝑛𝑍)
142 elfzuz 13551 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (𝑁...𝑛) → 𝑖 ∈ (ℤ𝑁))
143142, 81eleqtrdi 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 ∈ (𝑁...𝑛) → 𝑖𝑍)
144143adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑁...𝑛)) → 𝑖𝑍)
145 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → (𝐹𝑛) = (𝐹𝑖))
146145eleq1d 2811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑖 → ((𝐹𝑛) ∈ dom 𝑀 ↔ (𝐹𝑖) ∈ dom 𝑀))
147104, 146imbi12d 343 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑖 → (((𝜑𝑛𝑍) → (𝐹𝑛) ∈ dom 𝑀) ↔ ((𝜑𝑖𝑍) → (𝐹𝑖) ∈ dom 𝑀)))
148147, 90chvarvv 1995 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖𝑍) → (𝐹𝑖) ∈ dom 𝑀)
149144, 148syldan 589 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑁...𝑛)) → (𝐹𝑖) ∈ dom 𝑀)
150149adantlr 713 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝐹𝑖) ∈ dom 𝑀)
151 fzct 44994 . . . . . . . . . . . . . . . . . . 19 (𝑁...𝑛) ≼ ω
152151a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (𝑁...𝑛) ≼ ω)
153144ssd 44681 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑁...𝑛) ⊆ 𝑍)
154119simprd 494 . . . . . . . . . . . . . . . . . . . . 21 (𝜑Disj 𝑛𝑍 (𝐹𝑛))
155145cbvdisjv 5129 . . . . . . . . . . . . . . . . . . . . 21 (Disj 𝑛𝑍 (𝐹𝑛) ↔ Disj 𝑖𝑍 (𝐹𝑖))
156154, 155sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑Disj 𝑖𝑍 (𝐹𝑖))
157 disjss1 5124 . . . . . . . . . . . . . . . . . . . 20 ((𝑁...𝑛) ⊆ 𝑍 → (Disj 𝑖𝑍 (𝐹𝑖) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖)))
158153, 156, 157sylc 65 . . . . . . . . . . . . . . . . . . 19 (𝜑Disj 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖))
159158adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → Disj 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖))
160141, 8, 9, 150, 152, 159meadjiun 46087 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (𝑀 𝑖 ∈ (𝑁...𝑛)(𝐹𝑖)) = (Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹𝑖)))))
161 fzfid 13993 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑛𝑍) → (𝑁...𝑛) ∈ Fin)
162 2fveq3 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑖 → (𝑀‘(𝐹𝑛)) = (𝑀‘(𝐹𝑖)))
163162eleq1d 2811 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑖 → ((𝑀‘(𝐹𝑛)) ∈ (0[,)+∞) ↔ (𝑀‘(𝐹𝑖)) ∈ (0[,)+∞)))
164104, 163imbi12d 343 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑖 → (((𝜑𝑛𝑍) → (𝑀‘(𝐹𝑛)) ∈ (0[,)+∞)) ↔ ((𝜑𝑖𝑍) → (𝑀‘(𝐹𝑖)) ∈ (0[,)+∞))))
165164, 97chvarvv 1995 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖𝑍) → (𝑀‘(𝐹𝑖)) ∈ (0[,)+∞))
166144, 165syldan 589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹𝑖)) ∈ (0[,)+∞))
167166adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛𝑍) ∧ 𝑖 ∈ (𝑁...𝑛)) → (𝑀‘(𝐹𝑖)) ∈ (0[,)+∞))
168161, 167sge0fsummpt 46011 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → (Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹𝑖)))) = Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑖)))
169 2fveq3 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (𝑀‘(𝐹𝑖)) = (𝑀‘(𝐹𝑚)))
170169cbvsumv 15700 . . . . . . . . . . . . . . . . . . 19 Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚))
171170a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛𝑍) → Σ𝑖 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑖)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚)))
172168, 171eqtrd 2766 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛𝑍) → (Σ^‘(𝑖 ∈ (𝑁...𝑛) ↦ (𝑀‘(𝐹𝑖)))) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚)))
173140, 160, 1723eqtrd 2770 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝑀‘(𝐸𝑛)) = Σ𝑚 ∈ (𝑁...𝑛)(𝑀‘(𝐹𝑚)))
174108, 173chvarvv 1995 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → (𝑀‘(𝐸𝑖)) = Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚)))
175 2fveq3 6906 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑀‘(𝐹𝑚)) = (𝑀‘(𝐹𝑛)))
176175cbvsumv 15700 . . . . . . . . . . . . . . . 16 Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))
177176a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑍) → Σ𝑚 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑚)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)))
178174, 177eqtrd 2766 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑍) → (𝑀‘(𝐸𝑖)) = Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)))
179178breq1d 5163 . . . . . . . . . . . . 13 ((𝜑𝑖𝑍) → ((𝑀‘(𝐸𝑖)) ≤ 𝑥 ↔ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥))
180179ralbidva 3166 . . . . . . . . . . . 12 (𝜑 → (∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥 ↔ ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥))
181180biimpd 228 . . . . . . . . . . 11 (𝜑 → (∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥 → ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥))
182181imp 405 . . . . . . . . . 10 ((𝜑 ∧ ∀𝑖𝑍 (𝑀‘(𝐸𝑖)) ≤ 𝑥) → ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥)
183102, 182syldan 589 . . . . . . . . 9 ((𝜑 ∧ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥) → ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥)
184183ex 411 . . . . . . . 8 (𝜑 → (∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥))
185184reximdv 3160 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℝ ∀𝑛𝑍 (𝑀‘(𝐸𝑛)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥))
18614, 185mpd 15 . . . . . 6 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑖𝑍 Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛)) ≤ 𝑥)
18765, 66, 2, 1, 97, 186sge0reuzb 46069 . . . . 5 (𝜑 → (Σ^‘(𝑛𝑍 ↦ (𝑀‘(𝐹𝑛)))) = sup(ran (𝑖𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))), ℝ, < ))
18898cbvmptv 5266 . . . . . . . . . 10 (𝑛𝑍 ↦ (𝑀‘(𝐸𝑛))) = (𝑖𝑍 ↦ (𝑀‘(𝐸𝑖)))
18935, 188eqtri 2754 . . . . . . . . 9 𝑆 = (𝑖𝑍 ↦ (𝑀‘(𝐸𝑖)))
190189a1i 11 . . . . . . . 8 (𝜑𝑆 = (𝑖𝑍 ↦ (𝑀‘(𝐸𝑖))))
191178mpteq2dva 5253 . . . . . . . 8 (𝜑 → (𝑖𝑍 ↦ (𝑀‘(𝐸𝑖))) = (𝑖𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))))
192190, 191eqtrd 2766 . . . . . . 7 (𝜑𝑆 = (𝑖𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))))
193192rneqd 5944 . . . . . 6 (𝜑 → ran 𝑆 = ran (𝑖𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))))
194193supeq1d 9489 . . . . 5 (𝜑 → sup(ran 𝑆, ℝ, < ) = sup(ran (𝑖𝑍 ↦ Σ𝑛 ∈ (𝑁...𝑖)(𝑀‘(𝐹𝑛))), ℝ, < ))
195187, 194eqtr4d 2769 . . . 4 (𝜑 → (Σ^‘(𝑛𝑍 ↦ (𝑀‘(𝐹𝑛)))) = sup(ran 𝑆, ℝ, < ))
196195eqcomd 2732 . . 3 (𝜑 → sup(ran 𝑆, ℝ, < ) = (Σ^‘(𝑛𝑍 ↦ (𝑀‘(𝐹𝑛)))))
1971uzct 44664 . . . . . 6 𝑍 ≼ ω
198197a1i 11 . . . . 5 (𝜑𝑍 ≼ ω)
19965, 7, 9, 90, 198, 154meadjiun 46087 . . . 4 (𝜑 → (𝑀 𝑛𝑍 (𝐹𝑛)) = (Σ^‘(𝑛𝑍 ↦ (𝑀‘(𝐹𝑛)))))
200199eqcomd 2732 . . 3 (𝜑 → (Σ^‘(𝑛𝑍 ↦ (𝑀‘(𝐹𝑛)))) = (𝑀 𝑛𝑍 (𝐹𝑛)))
201119simplrd 768 . . . 4 (𝜑 𝑛𝑍 (𝐹𝑛) = 𝑛𝑍 (𝐸𝑛))
202201fveq2d 6905 . . 3 (𝜑 → (𝑀 𝑛𝑍 (𝐹𝑛)) = (𝑀 𝑛𝑍 (𝐸𝑛)))
203196, 200, 2023eqtrd 2770 . 2 (𝜑 → sup(ran 𝑆, ℝ, < ) = (𝑀 𝑛𝑍 (𝐸𝑛)))
20464, 203breqtrd 5179 1 (𝜑𝑆 ⇝ (𝑀 𝑛𝑍 (𝐸𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1534  wcel 2099  wral 3051  wrex 3060  Vcvv 3462  cdif 3944  wss 3947   ciun 5001  Disj wdisj 5118   class class class wbr 5153  cmpt 5236  dom cdm 5682  ran crn 5683  wf 6550  cfv 6554  (class class class)co 7424  ωcom 7876  cdom 8972  supcsup 9483  cr 11157  0cc0 11158  1c1 11159   + caddc 11161  +∞cpnf 11295  *cxr 11297   < clt 11298  cle 11299  cz 12610  cuz 12874  [,)cico 13380  ...cfz 13538  ..^cfzo 13681  cli 15486  Σcsu 15690  SAlgcsalg 45929  Σ^csumge0 45983  Meascmea 46070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-disj 5119  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-oadd 8500  df-omul 8501  df-er 8734  df-map 8857  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-sup 9485  df-oi 9553  df-card 9982  df-acn 9985  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12611  df-uz 12875  df-rp 13029  df-xadd 13147  df-ico 13384  df-icc 13385  df-fz 13539  df-fzo 13682  df-seq 14022  df-exp 14082  df-hash 14348  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-clim 15490  df-sum 15691  df-salg 45930  df-sumge0 45984  df-mea 46071
This theorem is referenced by:  meaiuninc  46102
  Copyright terms: Public domain W3C validator