meaiininclem - Mathbox for Glauco Siliprandi

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

Theorem meaiininclem 45137

Description: Measures are continuous from above: if 𝐸 is a nonincreasing sequence of measurable sets, and any of the sets has finite measure, then the measure of the intersection is the limit of the measures. This is Proposition 112C (f) of [Fremlin1] p. 16. (Contributed by Glauco Siliprandi, 8-Apr-2021.)

**Hypotheses**
Ref	Expression
meaiininclem.m	⊢ (𝜑 → 𝑀 ∈ Meas)
meaiininclem.n	⊢ (𝜑 → 𝑁 ∈ ℤ)
meaiininclem.z	⊢ 𝑍 = (ℤ_≥‘𝑁)
meaiininclem.e	⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
meaiininclem.i	⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))
meaiininclem.k	⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘𝑁))
meaiininclem.r	⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
meaiininclem.s	⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
meaiininclem.g	⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
meaiininclem.f	⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)

**Assertion**
Ref	Expression
meaiininclem	⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Distinct variable groups: 𝑛,𝐸 𝑛,𝐹 𝑛,𝐺 𝑛,𝐾 𝑛,𝑀 𝑛,𝑁 𝑛,𝑍 𝜑,𝑛 Allowed substitution hint: 𝑆(𝑛)

Proof of Theorem meaiininclem Dummy variables 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		meaiininclem.k	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘𝑁))
2		uzss 12841	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
3	1, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
4		meaiininclem.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑁)
5	3, 4	sseqtrrdi 4032	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ 𝑍)
6	5	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
7		simpr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
8	6, 7	sseldd 3982	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ 𝑍)
9		meaiininclem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
11		meaiininclem.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ Meas)
12		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ dom 𝑀 = dom 𝑀
13	11, 12	dmmeasal 45103	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
14	13	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
15	1, 4	eleqtrrdi 2845	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ 𝑍)
16		meaiininclem.e	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
17	16	ffvelcdmda 7082	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
18	15, 17	mpdan 686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝐾) ∈ dom 𝑀)
19	18	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
20	16	ffvelcdmda 7082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
21		saldifcl2 44979	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ (𝐸‘𝑛) ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
22	14, 19, 20, 21	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
23	22	elexd 3495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ V)
24	10, 23	fvmpt2d 7007	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
25	8, 24	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
26	25	fveq2d 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
27	11	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑀 ∈ Meas)
28	18	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝐾) ∈ dom 𝑀)
29		meaiininclem.r	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
30	29	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
31	8, 20	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ∈ dom 𝑀)
32		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
33	32, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
34		elfzouz 13632	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ_≥‘𝐾))
35	34	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ_≥‘𝐾))
36	33, 35	sseldd 3982	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ 𝑍)
37		eleq1w 2817	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ 𝑍 ↔ 𝑚 ∈ 𝑍))
38	37	anbi2d 630	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑚 ∈ 𝑍)))
39		fvoveq1 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40		fveq2 6888	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚))
41	39, 40	sseq12d 4014	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚)))
42	38, 41	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) ↔ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))))
43		meaiininclem.i	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))
44	42, 43	chvarvv 2003	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
45	32, 36, 44	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
46	45	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
47	7, 46	ssdec 43710	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
48	27, 28, 30, 31, 47	meadif 45130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
49	26, 48	eqtrd 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
50	49	oveq2d 7420	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))))
51	29	recnd 11238	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
52	51	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
53	27, 28, 30, 47, 31	meassre 45128	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ)
54	53	recnd 11238	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℂ)
55	52, 54	nncand 11572	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))) = (𝑀‘(𝐸‘𝑛)))
56	50, 55	eqtr2d 2774	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))))
57	56	mpteq2dva 5247	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))))
58		nfv 1918	. . . . 5 ⊢ Ⅎ𝑛𝜑
59		eqid 2733	. . . . 5 ⊢ (ℤ_≥‘𝐾) = (ℤ_≥‘𝐾)
60	1	eluzelzd 44020	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
61		difssd 4131	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ (𝐸‘𝐾))
62	24, 61	eqsstrd 4019	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
63	8, 62	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
64	22, 9	fmptd 7109	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑍⟶dom 𝑀)
65	64	ffvelcdmda 7082	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ dom 𝑀)
66	8, 65	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ∈ dom 𝑀)
67	27, 28, 30, 63, 66	meassre 45128	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℝ)
68	67	recnd 11238	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℂ)
69		meaiininclem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
70	43	sscond 4140	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
71	40	difeq2d 4121	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
72	71	cbvmptv 5260	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
73	9, 72	eqtri 2761	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
74		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1)))
75	74	difeq2d 4121	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝐸‘𝐾) ∖ (𝐸‘𝑚)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
76	4	peano2uzs 12882	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
77	76	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
78		fvex 6901	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐾) ∈ V
79	78	difexi 5327	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
81	73, 75, 77, 80	fvmptd3 7017	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
82	24, 81	sseq12d 4014	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1)))))
83	70, 82	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)))
84	11	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
85	84, 12, 65, 19, 62	meassle 45114	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐺‘𝑛)) ≤ (𝑀‘(𝐸‘𝐾)))
86		eqid 2733	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛)))
87	11, 69, 4, 64, 83, 29, 85, 86	meaiuninc2 45133	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
88		eqid 2733	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛)))
89	4, 86, 15, 88	climresmpt 44310	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))))
90	87, 89	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
91		meaiininclem.f	. . . . . . . . 9 ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)
92	91	eqcomi 2742	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = 𝐹
93	92	fveq2i 6891	. . . . . . 7 ⊢ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹)
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹))
95	90, 94	breqtrd 5173	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘𝐹))
96	58, 59, 60, 51, 68, 95	climsubc1mpt 44313	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
97	57, 96	eqbrtrd 5169	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
98		eqid 2733	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
99		eqid 2733	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛)))
100	4, 98, 15, 99	climresmpt 44310	. . 3 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
101	97, 100	mpbid 231	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
102		meaiininclem.s	. . . 4 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
103	102	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
104		eqidd 2734	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))))
105	4	uzct 43683	. . . . . . . . . 10 ⊢ 𝑍 ≼ ω
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≼ ω)
107	13, 106, 65	saliuncl 44974	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ∈ dom 𝑀)
108	91, 107	eqeltrid 2838	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ dom 𝑀)
109		saldifcl2 44979	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ 𝐹 ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
110	13, 18, 108, 109	syl3anc 1372	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
111		disjdif 4470	. . . . . . . 8 ⊢ (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅)
113	62	iunssd 5052	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
114	91, 113	eqsstrid 4029	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸‘𝐾))
115	11, 18, 29, 114, 108	meassre 45128	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℝ)
116		difssd 4131	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ (𝐸‘𝐾))
117	11, 18, 29, 116, 110	meassre 45128	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℝ)
118	11, 12, 108, 110, 112, 115, 117	meadjunre 45127	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))))
119		undif 4480	. . . . . . . 8 ⊢ (𝐹 ⊆ (𝐸‘𝐾) ↔ (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
120	114, 119	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
121	120	fveq2d 6892	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
122	104, 118, 121	3eqtr3d 2781	. . . . 5 ⊢ (𝜑 → ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
123	115	recnd 11238	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℂ)
124	117	recnd 11238	. . . . . 6 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℂ)
125	51, 123, 124	subaddd 11585	. . . . 5 ⊢ (𝜑 → (((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ↔ ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾))))
126	122, 125	mpbird 257	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)))
127		simpllr 775	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
128		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑛 ∈ 𝑍)
129		eldifi 4125	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸‘𝐾))
130	129	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
131		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑛))
132	130, 131	eldifd 3958	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
133		rspe 3247	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
134	128, 132, 133	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
135		eliun 5000	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
136	134, 135	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
137	136	adantlll 717	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
138	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))
139	24	iuneq2dv 5020	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
140	138, 139	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
141	140	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
142	141	ad3antrrr 729	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
143	137, 142	eleqtrd 2836	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ 𝐹)
144		elndif 4127	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
145	143, 144	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
146	127, 145	condan 817	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
147	146	ralrimiva 3147	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
148		vex 3479	. . . . . . . . 9 ⊢ 𝑥 ∈ V
149		eliin 5001	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛)))
150	148, 149	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
151	147, 150	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
152	151	ssd 43702	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
153		ssid 4003	. . . . . . . . . . . 12 ⊢ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)
154	153	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝐾) ⊆ (𝐸‘𝐾))
155		fveq2 6888	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾))
156	155	sseq1d 4012	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ⊆ (𝐸‘𝐾) ↔ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)))
157	156	rspcev 3612	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝑍 ∧ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)) → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
158	15, 154, 157	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
159		iinss 5058	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
160	158, 159	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
161	160	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
162		simpr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
163	161, 162	sseldd 3982	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
164		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑥
165		nfii1 5031	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
166	164, 165	nfel 2918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
167		iinss2 5059	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
168	167	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
169		simpl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
170	168, 169	sseldd 3982	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
171		elndif 4127	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐸‘𝑛) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
172	170, 171	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
173	172	ex 414	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → (𝑛 ∈ 𝑍 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
174	166, 173	ralrimi 3255	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
175		ralnex 3073	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
176	174, 175	sylib 217	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
177	176, 135	sylnibr 329	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
178	177	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
179	140	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
180	178, 179	neleqtrrd 2857	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ 𝐹)
181	163, 180	eldifd 3958	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
182	152, 181	eqelssd 4002	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) = ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
183	182	fveq2d 6892	. . . 4 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) = (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
184	126, 183	eqtr2d 2774	. . 3 ⊢ (𝜑 → (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
185	103, 184	breq12d 5160	. 2 ⊢ (𝜑 → (𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
186	101, 185	mpbird 257	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ∪ ciun 4996 ∩ ciin 4997 class class class wbr 5147 ↦ cmpt 5230 dom cdm 5675 ⟶wf 6536 ‘cfv 6540 (class class class)co 7404 ωcom 7850 ≼ cdom 8933 ℂcc 11104 ℝcr 11105 1c1 11107 + caddc 11109 − cmin 11440 ℤcz 12554 ℤ_≥cuz 12818 ..^cfzo 13623 ⇝ cli 15424 SAlgcsalg 44959 Meascmea 45100

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7360 df-ov 7407 df-oprab 7408 df-mpo 7409 df-om 7851 df-1st 7970 df-2nd 7971 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-oadd 8465 df-omul 8466 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-oi 9501 df-card 9930 df-acn 9933 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-z 12555 df-uz 12819 df-rp 12971 df-xadd 13089 df-ico 13326 df-icc 13327 df-fz 13481 df-fzo 13624 df-seq 13963 df-exp 14024 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629 df-salg 44960 df-sumge0 45014 df-mea 45101

This theorem is referenced by: meaiininc 45138

W3C validator