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 46767

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 12776	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
3	1, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
4		meaiininclem.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑁)
5	3, 4	sseqtrrdi 3974	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ 𝑍)
6	5	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
7		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
8	6, 7	sseldd 3933	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ 𝑍)
9		meaiininclem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
11		meaiininclem.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ Meas)
12		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ dom 𝑀 = dom 𝑀
13	11, 12	dmmeasal 46733	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
14	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
15	1, 4	eleqtrrdi 2846	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ 𝑍)
16		meaiininclem.e	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
17	16	ffvelcdmda 7029	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
18	15, 17	mpdan 688	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝐾) ∈ dom 𝑀)
19	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
20	16	ffvelcdmda 7029	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
21		saldifcl2 46609	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ (𝐸‘𝑛) ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
22	14, 19, 20, 21	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
23	22	elexd 3463	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ V)
24	10, 23	fvmpt2d 6954	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
25	8, 24	syldan 592	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
26	25	fveq2d 6837	. . . . . . . 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 13581	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ_≥‘𝐾))
35	34	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ_≥‘𝐾))
36	33, 35	sseldd 3933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ 𝑍)
37		eleq1w 2818	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ 𝑍 ↔ 𝑚 ∈ 𝑍))
38	37	anbi2d 631	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑚 ∈ 𝑍)))
39		fvoveq1 7381	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40		fveq2 6833	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚))
41	39, 40	sseq12d 3966	. . . . . . . . . . . . . 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 45369	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
48	27, 28, 30, 31, 47	meadif 46760	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
49	26, 48	eqtrd 2770	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
50	49	oveq2d 7374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))))
51	29	recnd 11162	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
52	51	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
53	27, 28, 30, 47, 31	meassre 46758	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ)
54	53	recnd 11162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℂ)
55	52, 54	nncand 11499	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))) = (𝑀‘(𝐸‘𝑛)))
56	50, 55	eqtr2d 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))))
57	56	mpteq2dva 5190	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))))
58		nfv 1916	. . . . 5 ⊢ Ⅎ𝑛𝜑
59		eqid 2735	. . . . 5 ⊢ (ℤ_≥‘𝐾) = (ℤ_≥‘𝐾)
60	1	eluzelzd 45656	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
61		difssd 4088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ (𝐸‘𝐾))
62	24, 61	eqsstrd 3967	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
63	8, 62	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
64	22, 9	fmptd 7059	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑍⟶dom 𝑀)
65	64	ffvelcdmda 7029	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ dom 𝑀)
66	8, 65	syldan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ∈ dom 𝑀)
67	27, 28, 30, 63, 66	meassre 46758	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℝ)
68	67	recnd 11162	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℂ)
69		meaiininclem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
70	43	sscond 4097	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
71	40	difeq2d 4077	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
72	71	cbvmptv 5201	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
73	9, 72	eqtri 2758	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
74		fveq2 6833	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1)))
75	74	difeq2d 4077	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝐸‘𝐾) ∖ (𝐸‘𝑚)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
76	4	peano2uzs 12817	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
77	76	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
78		fvex 6846	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐾) ∈ V
79	78	difexi 5274	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
81	73, 75, 77, 80	fvmptd3 6964	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
82	24, 81	sseq12d 3966	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1)))))
83	70, 82	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)))
84	11	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
85	84, 12, 65, 19, 62	meassle 46744	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐺‘𝑛)) ≤ (𝑀‘(𝐸‘𝐾)))
86		eqid 2735	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛)))
87	11, 69, 4, 64, 83, 29, 85, 86	meaiuninc2 46763	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
88		eqid 2735	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛)))
89	4, 86, 15, 88	climresmpt 45940	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))))
90	87, 89	mpbird 257	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
91		meaiininclem.f	. . . . . . . . 9 ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)
92	91	eqcomi 2744	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = 𝐹
93	92	fveq2i 6836	. . . . . . 7 ⊢ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹)
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹))
95	90, 94	breqtrd 5123	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘𝐹))
96	58, 59, 60, 51, 68, 95	climsubc1mpt 45943	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
97	57, 96	eqbrtrd 5119	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
98		eqid 2735	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
99		eqid 2735	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛)))
100	4, 98, 15, 99	climresmpt 45940	. . 3 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
101	97, 100	mpbid 232	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
102		meaiininclem.s	. . . 4 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
103	102	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
104		eqidd 2736	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))))
105	4	uzct 45345	. . . . . . . . . 10 ⊢ 𝑍 ≼ ω
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≼ ω)
107	13, 106, 65	saliuncl 46604	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ∈ dom 𝑀)
108	91, 107	eqeltrid 2839	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ dom 𝑀)
109		saldifcl2 46609	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ 𝐹 ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
110	13, 18, 108, 109	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
111		disjdif 4423	. . . . . . . 8 ⊢ (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅)
113	62	iunssd 5005	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
114	91, 113	eqsstrid 3971	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸‘𝐾))
115	11, 18, 29, 114, 108	meassre 46758	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℝ)
116		difssd 4088	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ (𝐸‘𝐾))
117	11, 18, 29, 116, 110	meassre 46758	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℝ)
118	11, 12, 108, 110, 112, 115, 117	meadjunre 46757	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))))
119		undif 4433	. . . . . . . 8 ⊢ (𝐹 ⊆ (𝐸‘𝐾) ↔ (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
120	114, 119	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
121	120	fveq2d 6837	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
122	104, 118, 121	3eqtr3d 2778	. . . . 5 ⊢ (𝜑 → ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
123	115	recnd 11162	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℂ)
124	117	recnd 11162	. . . . . 6 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℂ)
125	51, 123, 124	subaddd 11512	. . . . 5 ⊢ (𝜑 → (((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ↔ ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾))))
126	122, 125	mpbird 257	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)))
127		simpllr 776	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
128		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑛 ∈ 𝑍)
129		eldifi 4082	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸‘𝐾))
130	129	ad2antrr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
131		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑛))
132	130, 131	eldifd 3911	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
133		rspe 3225	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
134	128, 132, 133	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
135		eliun 4949	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
136	134, 135	sylibr 234	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
137	136	adantlll 719	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
138	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))
139	24	iuneq2dv 4970	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
140	138, 139	eqtrd 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
141	140	eqcomd 2741	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
142	141	ad3antrrr 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
143	137, 142	eleqtrd 2837	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ 𝐹)
144		elndif 4084	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
145	143, 144	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
146	127, 145	condan 818	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
147	146	ralrimiva 3127	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
148		vex 3443	. . . . . . . . 9 ⊢ 𝑥 ∈ V
149		eliin 4950	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛)))
150	148, 149	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
151	147, 150	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
152	151	ssd 45362	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
153		ssid 3955	. . . . . . . . . . . 12 ⊢ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)
154	153	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝐾) ⊆ (𝐸‘𝐾))
155		fveq2 6833	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾))
156	155	sseq1d 3964	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ⊆ (𝐸‘𝐾) ↔ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)))
157	156	rspcev 3575	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝑍 ∧ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)) → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
158	15, 154, 157	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
159		iinss 5011	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
160	158, 159	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
161	160	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
162		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
163	161, 162	sseldd 3933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
164		nfcv 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑥
165		nfii1 4983	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
166	164, 165	nfel 2912	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
167		iinss2 5012	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
168	167	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
169		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
170	168, 169	sseldd 3933	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
171		elndif 4084	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐸‘𝑛) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
172	170, 171	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
173	172	ex 412	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → (𝑛 ∈ 𝑍 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
174	166, 173	ralrimi 3233	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
175		ralnex 3061	. . . . . . . . . . 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 2858	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ 𝐹)
181	163, 180	eldifd 3911	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
182	152, 181	eqelssd 3954	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) = ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
183	182	fveq2d 6837	. . . 4 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) = (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
184	126, 183	eqtr2d 2771	. . 3 ⊢ (𝜑 → (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
185	103, 184	breq12d 5110	. 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 3050 ∃wrex 3059 Vcvv 3439 ∖ cdif 3897 ∪ cun 3898 ∩ cin 3899 ⊆ wss 3900 ∅c0 4284 ∪ ciun 4945 ∩ ciin 4946 class class class wbr 5097 ↦ cmpt 5178 dom cdm 5623 ⟶wf 6487 ‘cfv 6491 (class class class)co 7358 ωcom 7808 ≼ cdom 8883 ℂcc 11026 ℝcr 11027 1c1 11029 + caddc 11031 − cmin 11366 ℤcz 12490 ℤ_≥cuz 12753 ..^cfzo 13572 ⇝ cli 15409 SAlgcsalg 46589 Meascmea 46730

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 2183 ax-ext 2707 ax-rep 5223 ax-sep 5240 ax-nul 5250 ax-pow 5309 ax-pr 5376 ax-un 7680 ax-inf2 9552 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

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 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3349 df-reu 3350 df-rab 3399 df-v 3441 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4285 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4902 df-iun 4947 df-iin 4948 df-disj 5065 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6258 df-ord 6319 df-on 6320 df-lim 6321 df-suc 6322 df-iota 6447 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-isom 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-omul 8402 df-er 8635 df-map 8767 df-en 8886 df-dom 8887 df-sdom 8888 df-fin 8889 df-sup 9347 df-oi 9417 df-card 9853 df-acn 9856 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-n0 12404 df-z 12491 df-uz 12754 df-rp 12908 df-xadd 13029 df-ico 13269 df-icc 13270 df-fz 13426 df-fzo 13573 df-seq 13927 df-exp 13987 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-salg 46590 df-sumge0 46644 df-mea 46731

This theorem is referenced by: meaiininc 46768

W3C validator