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 46938

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 12806	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
3	1, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
4		meaiininclem.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑁)
5	3, 4	sseqtrrdi 3964	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ 𝑍)
6	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
7		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
8	6, 7	sseldd 3923	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ 𝑍)
9		meaiininclem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
11		meaiininclem.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ Meas)
12		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ dom 𝑀 = dom 𝑀
13	11, 12	dmmeasal 46904	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
14	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
15	1, 4	eleqtrrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ 𝑍)
16		meaiininclem.e	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
17	16	ffvelcdmda 7032	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
18	15, 17	mpdan 688	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝐾) ∈ dom 𝑀)
19	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
20	16	ffvelcdmda 7032	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
21		saldifcl2 46780	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ (𝐸‘𝑛) ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
22	14, 19, 20, 21	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
23	22	elexd 3454	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ V)
24	10, 23	fvmpt2d 6957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
25	8, 24	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
26	25	fveq2d 6840	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
27	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑀 ∈ Meas)
28	18	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝐾) ∈ dom 𝑀)
29		meaiininclem.r	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
30	29	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
31	8, 20	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ∈ dom 𝑀)
32		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
33	32, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
34		elfzouz 13613	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ_≥‘𝐾))
35	34	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ_≥‘𝐾))
36	33, 35	sseldd 3923	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ 𝑍)
37		eleq1w 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ 𝑍 ↔ 𝑚 ∈ 𝑍))
38	37	anbi2d 631	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑚 ∈ 𝑍)))
39		fvoveq1 7385	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40		fveq2 6836	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚))
41	39, 40	sseq12d 3956	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚)))
42	38, 41	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) ↔ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))))
43		meaiininclem.i	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))
44	42, 43	chvarvv 1991	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
45	32, 36, 44	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
46	45	adantlr 716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
47	7, 46	ssdec 45542	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
48	27, 28, 30, 31, 47	meadif 46931	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
49	26, 48	eqtrd 2772	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
50	49	oveq2d 7378	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))))
51	29	recnd 11168	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
52	51	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
53	27, 28, 30, 47, 31	meassre 46929	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ)
54	53	recnd 11168	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℂ)
55	52, 54	nncand 11505	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))) = (𝑀‘(𝐸‘𝑛)))
56	50, 55	eqtr2d 2773	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))))
57	56	mpteq2dva 5179	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))))
58		nfv 1916	. . . . 5 ⊢ Ⅎ𝑛𝜑
59		eqid 2737	. . . . 5 ⊢ (ℤ_≥‘𝐾) = (ℤ_≥‘𝐾)
60	1	eluzelzd 45828	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
61		difssd 4078	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ (𝐸‘𝐾))
62	24, 61	eqsstrd 3957	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
63	8, 62	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
64	22, 9	fmptd 7062	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑍⟶dom 𝑀)
65	64	ffvelcdmda 7032	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ dom 𝑀)
66	8, 65	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ∈ dom 𝑀)
67	27, 28, 30, 63, 66	meassre 46929	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℝ)
68	67	recnd 11168	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℂ)
69		meaiininclem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
70	43	sscond 4087	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
71	40	difeq2d 4067	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
72	71	cbvmptv 5190	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
73	9, 72	eqtri 2760	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
74		fveq2 6836	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1)))
75	74	difeq2d 4067	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝐸‘𝐾) ∖ (𝐸‘𝑚)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
76	4	peano2uzs 12847	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
77	76	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
78		fvex 6849	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐾) ∈ V
79	78	difexi 5268	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
81	73, 75, 77, 80	fvmptd3 6967	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
82	24, 81	sseq12d 3956	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1)))))
83	70, 82	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)))
84	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
85	84, 12, 65, 19, 62	meassle 46915	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐺‘𝑛)) ≤ (𝑀‘(𝐸‘𝐾)))
86		eqid 2737	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛)))
87	11, 69, 4, 64, 83, 29, 85, 86	meaiuninc2 46934	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
88		eqid 2737	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛)))
89	4, 86, 15, 88	climresmpt 46111	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))))
90	87, 89	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
91		meaiininclem.f	. . . . . . . . 9 ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)
92	91	eqcomi 2746	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = 𝐹
93	92	fveq2i 6839	. . . . . . 7 ⊢ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹)
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹))
95	90, 94	breqtrd 5112	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘𝐹))
96	58, 59, 60, 51, 68, 95	climsubc1mpt 46114	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
97	57, 96	eqbrtrd 5108	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
98		eqid 2737	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
99		eqid 2737	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛)))
100	4, 98, 15, 99	climresmpt 46111	. . 3 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
101	97, 100	mpbid 232	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
102		meaiininclem.s	. . . 4 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
103	102	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
104		eqidd 2738	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))))
105	4	uzct 45518	. . . . . . . . . 10 ⊢ 𝑍 ≼ ω
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≼ ω)
107	13, 106, 65	saliuncl 46775	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ∈ dom 𝑀)
108	91, 107	eqeltrid 2841	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ dom 𝑀)
109		saldifcl2 46780	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ 𝐹 ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
110	13, 18, 108, 109	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
111		disjdif 4413	. . . . . . . 8 ⊢ (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅)
113	62	iunssd 4994	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
114	91, 113	eqsstrid 3961	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸‘𝐾))
115	11, 18, 29, 114, 108	meassre 46929	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℝ)
116		difssd 4078	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ (𝐸‘𝐾))
117	11, 18, 29, 116, 110	meassre 46929	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℝ)
118	11, 12, 108, 110, 112, 115, 117	meadjunre 46928	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))))
119		undif 4423	. . . . . . . 8 ⊢ (𝐹 ⊆ (𝐸‘𝐾) ↔ (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
120	114, 119	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
121	120	fveq2d 6840	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
122	104, 118, 121	3eqtr3d 2780	. . . . 5 ⊢ (𝜑 → ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
123	115	recnd 11168	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℂ)
124	117	recnd 11168	. . . . . 6 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℂ)
125	51, 123, 124	subaddd 11518	. . . . 5 ⊢ (𝜑 → (((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ↔ ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾))))
126	122, 125	mpbird 257	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)))
127		simpllr 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
128		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑛 ∈ 𝑍)
129		eldifi 4072	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸‘𝐾))
130	129	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
131		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑛))
132	130, 131	eldifd 3901	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
133		rspe 3228	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
134	128, 132, 133	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
135		eliun 4938	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
136	134, 135	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
137	136	adantlll 719	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
138	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))
139	24	iuneq2dv 4959	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
140	138, 139	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
141	140	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
142	141	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
143	137, 142	eleqtrd 2839	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ 𝐹)
144		elndif 4074	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
145	143, 144	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
146	127, 145	condan 818	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
147	146	ralrimiva 3130	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
148		vex 3434	. . . . . . . . 9 ⊢ 𝑥 ∈ V
149		eliin 4939	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛)))
150	148, 149	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
151	147, 150	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
152	151	ssd 45535	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
153		ssid 3945	. . . . . . . . . . . 12 ⊢ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)
154	153	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝐾) ⊆ (𝐸‘𝐾))
155		fveq2 6836	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾))
156	155	sseq1d 3954	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ⊆ (𝐸‘𝐾) ↔ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)))
157	156	rspcev 3565	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝑍 ∧ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)) → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
158	15, 154, 157	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
159		iinss 5000	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
160	158, 159	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
161	160	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
162		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
163	161, 162	sseldd 3923	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
164		nfcv 2899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑥
165		nfii1 4972	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
166	164, 165	nfel 2914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
167		iinss2 5001	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
168	167	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
169		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
170	168, 169	sseldd 3923	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
171		elndif 4074	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐸‘𝑛) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
172	170, 171	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
173	172	ex 412	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → (𝑛 ∈ 𝑍 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
174	166, 173	ralrimi 3236	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
175		ralnex 3064	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
176	174, 175	sylib 218	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
177	176, 135	sylnibr 329	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
178	177	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
179	140	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
180	178, 179	neleqtrrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ 𝐹)
181	163, 180	eldifd 3901	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
182	152, 181	eqelssd 3944	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) = ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
183	182	fveq2d 6840	. . . 4 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) = (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
184	126, 183	eqtr2d 2773	. . 3 ⊢ (𝜑 → (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
185	103, 184	breq12d 5099	. 2 ⊢ (𝜑 → (𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
186	101, 185	mpbird 257	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 ∪ ciun 4934 ∩ ciin 4935 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5626 ⟶wf 6490 ‘cfv 6494 (class class class)co 7362 ωcom 7812 ≼ cdom 8886 ℂcc 11031 ℝcr 11032 1c1 11034 + caddc 11036 − cmin 11372 ℤcz 12519 ℤ_≥cuz 12783 ..^cfzo 13603 ⇝ cli 15441 SAlgcsalg 46760 Meascmea 46901

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-inf2 9557 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-se 5580 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-isom 6503 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-omul 8405 df-er 8638 df-map 8770 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-sup 9350 df-oi 9420 df-card 9858 df-acn 9861 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-xadd 13059 df-ico 13299 df-icc 13300 df-fz 13457 df-fzo 13604 df-seq 13959 df-exp 14019 df-hash 14288 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-sum 15644 df-salg 46761 df-sumge0 46815 df-mea 46902

This theorem is referenced by: meaiininc 46939

W3C validator