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 47412

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 12943	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
3	1, 2	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
4		meaiininclem.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑁)
5	3, 4	sseqtrrdi 3972	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ 𝑍)
6	5	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
7		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
8	6, 7	sseldd 3932	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ 𝑍)
9		meaiininclem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
11		meaiininclem.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ Meas)
12		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ dom 𝑀 = dom 𝑀
13	11, 12	dmmeasal 47378	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
14	13	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
15	1, 4	eleqtrrdi 2871	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ 𝑍)
16		meaiininclem.e	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
17	16	ffvelcdmda 7073	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
18	15, 17	mpdan 700	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝐾) ∈ dom 𝑀)
19	18	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
20	16	ffvelcdmda 7073	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
21		saldifcl2 47254	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ (𝐸‘𝑛) ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
22	14, 19, 20, 21	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
23	22	elexd 3473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ V)
24	10, 23	fvmpt2d 6996	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
25	8, 24	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
26	25	fveq2d 6878	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
27	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑀 ∈ Meas)
28	18	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝐾) ∈ dom 𝑀)
29		meaiininclem.r	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
30	29	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
31	8, 20	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ∈ dom 𝑀)
32		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
33	32, 5	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
34		elfzouz 13752	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ_≥‘𝐾))
35	34	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ_≥‘𝐾))
36	33, 35	sseldd 3932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ 𝑍)
37		eleq1w 2843	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ 𝑍 ↔ 𝑚 ∈ 𝑍))
38	37	anbi2d 642	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑚 ∈ 𝑍)))
39		fvoveq1 7432	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40		fveq2 6874	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚))
41	39, 40	sseq12d 3964	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚)))
42	38, 41	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) ↔ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))))
43		meaiininclem.i	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))
44	42, 43	chvarvv 2022	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
45	32, 36, 44	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
46	45	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
47	7, 46	ssdec 46018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
48	27, 28, 30, 31, 47	meadif 47405	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
49	26, 48	eqtrd 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
50	49	oveq2d 7425	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))))
51	29	recnd 11294	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
52	51	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
53	27, 28, 30, 47, 31	meassre 47403	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ)
54	53	recnd 11294	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℂ)
55	52, 54	nncand 11631	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))) = (𝑀‘(𝐸‘𝑛)))
56	50, 55	eqtr2d 2796	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))))
57	56	mpteq2dva 5198	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))))
58		nfv 1947	. . . . 5 ⊢ Ⅎ𝑛𝜑
59		eqid 2760	. . . . 5 ⊢ (ℤ_≥‘𝐾) = (ℤ_≥‘𝐾)
60	1	eluzelzd 46302	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
61		difssd 4084	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ (𝐸‘𝐾))
62	24, 61	eqsstrd 3965	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
63	8, 62	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
64	22, 9	fmptd 7103	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑍⟶dom 𝑀)
65	64	ffvelcdmda 7073	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ dom 𝑀)
66	8, 65	syldan 603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ∈ dom 𝑀)
67	27, 28, 30, 63, 66	meassre 47403	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℝ)
68	67	recnd 11294	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℂ)
69		meaiininclem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
70	43	sscond 4093	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
71	40	difeq2d 4074	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
72	71	cbvmptv 5209	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
73	9, 72	eqtri 2783	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
74		fveq2 6874	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1)))
75	74	difeq2d 4074	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝐸‘𝐾) ∖ (𝐸‘𝑚)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
76	4	peano2uzs 12984	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
77	76	adantl 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
78		fvex 6887	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐾) ∈ V
79	78	difexi 5292	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
81	73, 75, 77, 80	fvmptd3 7006	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
82	24, 81	sseq12d 3964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1)))))
83	70, 82	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)))
84	11	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
85	84, 12, 65, 19, 62	meassle 47389	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐺‘𝑛)) ≤ (𝑀‘(𝐸‘𝐾)))
86		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛)))
87	11, 69, 4, 64, 83, 29, 85, 86	meaiuninc2 47408	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
88		eqid 2760	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛)))
89	4, 86, 15, 88	climresmpt 46585	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))))
90	87, 89	mpbird 260	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
91		meaiininclem.f	. . . . . . . . 9 ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)
92	91	eqcomi 2769	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = 𝐹
93	92	fveq2i 6877	. . . . . . 7 ⊢ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹)
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹))
95	90, 94	breqtrd 5131	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘𝐹))
96	58, 59, 60, 51, 68, 95	climsubc1mpt 46588	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
97	57, 96	eqbrtrd 5127	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
98		eqid 2760	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
99		eqid 2760	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛)))
100	4, 98, 15, 99	climresmpt 46585	. . 3 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
101	97, 100	mpbid 235	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
102		meaiininclem.s	. . . 4 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
103	102	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
104		eqidd 2761	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))))
105	4	uzct 45995	. . . . . . . . . 10 ⊢ 𝑍 ≼ ω
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≼ ω)
107	13, 106, 65	saliuncl 47249	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ∈ dom 𝑀)
108	91, 107	eqeltrid 2864	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ dom 𝑀)
109		saldifcl2 47254	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ 𝐹 ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
110	13, 18, 108, 109	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
111		disjdif 4426	. . . . . . . 8 ⊢ (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅)
113	62	iunssd 5009	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
114	91, 113	eqsstrid 3969	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸‘𝐾))
115	11, 18, 29, 114, 108	meassre 47403	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℝ)
116		difssd 4084	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ (𝐸‘𝐾))
117	11, 18, 29, 116, 110	meassre 47403	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℝ)
118	11, 12, 108, 110, 112, 115, 117	meadjunre 47402	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))))
119		undif 4438	. . . . . . . 8 ⊢ (𝐹 ⊆ (𝐸‘𝐾) ↔ (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
120	114, 119	sylib 221	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
121	120	fveq2d 6878	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
122	104, 118, 121	3eqtr3d 2803	. . . . 5 ⊢ (𝜑 → ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
123	115	recnd 11294	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℂ)
124	117	recnd 11294	. . . . . 6 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℂ)
125	51, 123, 124	subaddd 11644	. . . . 5 ⊢ (𝜑 → (((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ↔ ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾))))
126	122, 125	mpbird 260	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)))
127		simpllr 788	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
128		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑛 ∈ 𝑍)
129		eldifi 4078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸‘𝐾))
130	129	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
131		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑛))
132	130, 131	eldifd 3910	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
133		rspe 3252	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
134	128, 132, 133	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
135		eliun 4955	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
136	134, 135	sylibr 237	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
137	136	adantlll 731	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
138	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))
139	24	iuneq2dv 4976	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
140	138, 139	eqtrd 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
141	140	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
142	141	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
143	137, 142	eleqtrd 2862	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ 𝐹)
144		elndif 4080	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
145	143, 144	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
146	127, 145	condan 830	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
147	146	ralrimiva 3154	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
148		vex 3454	. . . . . . . . 9 ⊢ 𝑥 ∈ V
149		eliin 4956	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛)))
150	148, 149	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
151	147, 150	sylibr 237	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
152	151	ssd 46012	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
153		ssid 3953	. . . . . . . . . . . 12 ⊢ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)
154	153	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝐾) ⊆ (𝐸‘𝐾))
155		fveq2 6874	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾))
156	155	sseq1d 3962	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ⊆ (𝐸‘𝐾) ↔ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)))
157	156	rspcev 3576	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝑍 ∧ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)) → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
158	15, 154, 157	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
159		iinss 5015	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
160	158, 159	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
161	160	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
162		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
163	161, 162	sseldd 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
164		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑥
165		nfii1 4987	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
166	164, 165	nfel 2936	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
167		iinss2 5016	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
168	167	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
169		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
170	168, 169	sseldd 3932	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
171		elndif 4080	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐸‘𝑛) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
172	170, 171	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
173	172	ex 418	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → (𝑛 ∈ 𝑍 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
174	166, 173	ralrimi 3260	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
175		ralnex 3088	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
176	174, 175	sylib 221	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
177	176, 135	sylnibr 332	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
178	177	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
179	140	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
180	178, 179	neleqtrrd 2883	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ 𝐹)
181	163, 180	eldifd 3910	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
182	152, 181	eqelssd 3952	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) = ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
183	182	fveq2d 6878	. . . 4 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) = (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
184	126, 183	eqtr2d 2796	. . 3 ⊢ (𝜑 → (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
185	103, 184	breq12d 5116	. 2 ⊢ (𝜑 → (𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
186	101, 185	mpbird 260	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ∪ ciun 4951 ∩ ciin 4952 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5648 ⟶wf 6524 ‘cfv 6528 (class class class)co 7409 ωcom 7861 ≼ cdom 8950 ℂcc 11155 ℝcr 11156 1c1 11158 + caddc 11160 − cmin 11498 ℤcz 12648 ℤ_≥cuz 12920 ..^cfzo 13742 ⇝ cli 15604 SAlgcsalg 47234 Meascmea 47375

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7735 ax-inf2 9620 ax-cnex 11213 ax-resscn 11214 ax-1cn 11215 ax-icn 11216 ax-addcl 11217 ax-addrcl 11218 ax-mulcl 11219 ax-mulrcl 11220 ax-mulcom 11221 ax-addass 11222 ax-mulass 11223 ax-distr 11224 ax-i2m1 11225 ax-1ne0 11226 ax-1rid 11227 ax-rnegex 11228 ax-rrecex 11229 ax-cnre 11230 ax-pre-lttri 11231 ax-pre-lttrn 11232 ax-pre-ltadd 11233 ax-pre-mulgt0 11234 ax-pre-sup 11235

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-se 5602 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6294 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-isom 6537 df-riota 7366 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8455 df-2o 8456 df-oadd 8459 df-omul 8460 df-er 8696 df-map 8828 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-oi 9482 df-card 9977 df-acn 9980 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11500 df-neg 11501 df-div 11929 df-nn 12291 df-2 12360 df-3 12361 df-n0 12562 df-z 12649 df-uz 12921 df-rp 13076 df-xadd 13197 df-ico 13437 df-icc 13438 df-fz 13595 df-fzo 13743 df-seq 14099 df-exp 14159 df-hash 14428 df-cj 15219 df-re 15220 df-im 15221 df-sqrt 15355 df-abs 15356 df-clim 15608 df-sum 15807 df-salg 47235 df-sumge0 47289 df-mea 47376

This theorem is used by: meaiininc 47413

W3C validator