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 44717

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 12786	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (ℤ_≥‘𝑁) → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
3	1, 2	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ (ℤ_≥‘𝑁))
4		meaiininclem.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (ℤ_≥‘𝑁)
5	3, 4	sseqtrrdi 3995	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℤ_≥‘𝐾) ⊆ 𝑍)
6	5	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
7		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ (ℤ_≥‘𝐾))
8	6, 7	sseldd 3945	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑛 ∈ 𝑍)
9		meaiininclem.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
11		meaiininclem.m	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ Meas)
12		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ dom 𝑀 = dom 𝑀
13	11, 12	dmmeasal 44683	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝑀 ∈ SAlg)
14	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom 𝑀 ∈ SAlg)
15	1, 4	eleqtrrdi 2849	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐾 ∈ 𝑍)
16		meaiininclem.e	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑀)
17	16	ffvelcdmda 7035	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
18	15, 17	mpdan 685	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘𝐾) ∈ dom 𝑀)
19	18	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝐾) ∈ dom 𝑀)
20	16	ffvelcdmda 7035	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑀)
21		saldifcl2 44559	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ (𝐸‘𝑛) ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
22	14, 19, 20, 21	syl3anc 1371	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ dom 𝑀)
23	22	elexd 3465	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ∈ V)
24	10, 23	fvmpt2d 6961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
25	8, 24	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) = ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
26	25	fveq2d 6846	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
27	11	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → 𝑀 ∈ Meas)
28	18	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝐾) ∈ dom 𝑀)
29		meaiininclem.r	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
30	29	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℝ)
31	8, 20	syldan 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ∈ dom 𝑀)
32		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝜑)
33	32, 5	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (ℤ_≥‘𝐾) ⊆ 𝑍)
34		elfzouz 13576	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (𝐾..^𝑛) → 𝑚 ∈ (ℤ_≥‘𝐾))
35	34	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ (ℤ_≥‘𝐾))
36	33, 35	sseldd 3945	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → 𝑚 ∈ 𝑍)
37		eleq1w 2820	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝑛 ∈ 𝑍 ↔ 𝑚 ∈ 𝑍))
38	37	anbi2d 629	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ 𝑍) ↔ (𝜑 ∧ 𝑚 ∈ 𝑍)))
39		fvoveq1 7380	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘(𝑛 + 1)) = (𝐸‘(𝑚 + 1)))
40		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑚 → (𝐸‘𝑛) = (𝐸‘𝑚))
41	39, 40	sseq12d 3977	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑚 → ((𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛) ↔ (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚)))
42	38, 41	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛)) ↔ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))))
43		meaiininclem.i	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘(𝑛 + 1)) ⊆ (𝐸‘𝑛))
44	42, 43	chvarvv 2002	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
45	32, 36, 44	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
46	45	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) ∧ 𝑚 ∈ (𝐾..^𝑛)) → (𝐸‘(𝑚 + 1)) ⊆ (𝐸‘𝑚))
47	7, 46	ssdec 43288	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
48	27, 28, 30, 31, 47	meadif 44710	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
49	26, 48	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛))))
50	49	oveq2d 7373	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))) = ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))))
51	29	recnd 11183	. . . . . . . 8 ⊢ (𝜑 → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
52	51	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝐾)) ∈ ℂ)
53	27, 28, 30, 47, 31	meassre 44708	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℝ)
54	53	recnd 11183	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) ∈ ℂ)
55	52, 54	nncand 11517	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → ((𝑀‘(𝐸‘𝐾)) − ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐸‘𝑛)))) = (𝑀‘(𝐸‘𝑛)))
56	50, 55	eqtr2d 2777	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛))))
57	56	mpteq2dva 5205	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))))
58		nfv 1917	. . . . 5 ⊢ Ⅎ𝑛𝜑
59		eqid 2736	. . . . 5 ⊢ (ℤ_≥‘𝐾) = (ℤ_≥‘𝐾)
60	1	eluzelzd 43599	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
61		difssd 4092	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ (𝐸‘𝐾))
62	24, 61	eqsstrd 3982	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
63	8, 62	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
64	22, 9	fmptd 7062	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑍⟶dom 𝑀)
65	64	ffvelcdmda 7035	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ dom 𝑀)
66	8, 65	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝐺‘𝑛) ∈ dom 𝑀)
67	27, 28, 30, 63, 66	meassre 44708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℝ)
68	67	recnd 11183	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘𝐾)) → (𝑀‘(𝐺‘𝑛)) ∈ ℂ)
69		meaiininclem.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
70	43	sscond 4101	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
71	40	difeq2d 4082	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑚 → ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
72	71	cbvmptv 5218	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
73	9, 72	eqtri 2764	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑚 ∈ 𝑍 ↦ ((𝐸‘𝐾) ∖ (𝐸‘𝑚)))
74		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (𝐸‘𝑚) = (𝐸‘(𝑛 + 1)))
75	74	difeq2d 4082	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((𝐸‘𝐾) ∖ (𝐸‘𝑚)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
76	4	peano2uzs 12827	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ 𝑍 → (𝑛 + 1) ∈ 𝑍)
77	76	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑛 + 1) ∈ 𝑍)
78		fvex 6855	. . . . . . . . . . . . 13 ⊢ (𝐸‘𝐾) ∈ V
79	78	difexi 5285	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V
80	79	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))) ∈ V)
81	73, 75, 77, 80	fvmptd3 6971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘(𝑛 + 1)) = ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1))))
82	24, 81	sseq12d 3977	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)) ↔ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ⊆ ((𝐸‘𝐾) ∖ (𝐸‘(𝑛 + 1)))))
83	70, 82	mpbird 256	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ⊆ (𝐺‘(𝑛 + 1)))
84	11	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑀 ∈ Meas)
85	84, 12, 65, 19, 62	meassle 44694	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑀‘(𝐺‘𝑛)) ≤ (𝑀‘(𝐸‘𝐾)))
86		eqid 2736	. . . . . . . 8 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛)))
87	11, 69, 4, 64, 83, 29, 85, 86	meaiuninc2 44713	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
88		eqid 2736	. . . . . . . 8 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛)))
89	4, 86, 15, 88	climresmpt 43890	. . . . . . 7 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))))
90	87, 89	mpbird 256	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)))
91		meaiininclem.f	. . . . . . . . 9 ⊢ 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)
92	91	eqcomi 2745	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = 𝐹
93	92	fveq2i 6845	. . . . . . 7 ⊢ (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹)
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝑀‘∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛)) = (𝑀‘𝐹))
95	90, 94	breqtrd 5131	. . . . 5 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐺‘𝑛))) ⇝ (𝑀‘𝐹))
96	58, 59, 60, 51, 68, 95	climsubc1mpt 43893	. . . 4 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘(𝐺‘𝑛)))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
97	57, 96	eqbrtrd 5127	. . 3 ⊢ (𝜑 → (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
98		eqid 2736	. . . 4 ⊢ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
99		eqid 2736	. . . 4 ⊢ (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) = (𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛)))
100	4, 98, 15, 99	climresmpt 43890	. . 3 ⊢ (𝜑 → ((𝑛 ∈ (ℤ_≥‘𝐾) ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
101	97, 100	mpbid 231	. 2 ⊢ (𝜑 → (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
102		meaiininclem.s	. . . 4 ⊢ 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛)))
103	102	a1i 11	. . 3 ⊢ (𝜑 → 𝑆 = (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))))
104		eqidd 2737	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))))
105	4	uzct 43261	. . . . . . . . . 10 ⊢ 𝑍 ≼ ω
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑍 ≼ ω)
107	13, 106, 65	saliuncl 44554	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ∈ dom 𝑀)
108	91, 107	eqeltrid 2842	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ dom 𝑀)
109		saldifcl2 44559	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ SAlg ∧ (𝐸‘𝐾) ∈ dom 𝑀 ∧ 𝐹 ∈ dom 𝑀) → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
110	13, 18, 108, 109	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ∈ dom 𝑀)
111		disjdif 4431	. . . . . . . 8 ⊢ (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅
112	111	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∩ ((𝐸‘𝐾) ∖ 𝐹)) = ∅)
113	62	iunssd 5010	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) ⊆ (𝐸‘𝐾))
114	91, 113	eqsstrid 3992	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝐸‘𝐾))
115	11, 18, 29, 114, 108	meassre 44708	. . . . . . 7 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℝ)
116		difssd 4092	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ (𝐸‘𝐾))
117	11, 18, 29, 116, 110	meassre 44708	. . . . . . 7 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℝ)
118	11, 12, 108, 110, 112, 115, 117	meadjunre 44707	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))))
119		undif 4441	. . . . . . . 8 ⊢ (𝐹 ⊆ (𝐸‘𝐾) ↔ (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
120	114, 119	sylib 217	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹)) = (𝐸‘𝐾))
121	120	fveq2d 6846	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝐹 ∪ ((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
122	104, 118, 121	3eqtr3d 2784	. . . . 5 ⊢ (𝜑 → ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾)))
123	115	recnd 11183	. . . . . 6 ⊢ (𝜑 → (𝑀‘𝐹) ∈ ℂ)
124	117	recnd 11183	. . . . . 6 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ∈ ℂ)
125	51, 123, 124	subaddd 11530	. . . . 5 ⊢ (𝜑 → (((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) ↔ ((𝑀‘𝐹) + (𝑀‘((𝐸‘𝐾) ∖ 𝐹))) = (𝑀‘(𝐸‘𝐾))))
126	122, 125	mpbird 256	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)) = (𝑀‘((𝐸‘𝐾) ∖ 𝐹)))
127		simpllr 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
128		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑛 ∈ 𝑍)
129		eldifi 4086	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) → 𝑥 ∈ (𝐸‘𝐾))
130	129	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
131		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ (𝐸‘𝑛))
132	130, 131	eldifd 3921	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
133		rspe 3232	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
134	128, 132, 133	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
135		eliun 4958	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
136	134, 135	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
137	136	adantlll 716	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
138	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛))
139	24	iuneq2dv 4978	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 (𝐺‘𝑛) = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
140	138, 139	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
141	140	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
142	141	ad3antrrr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) = 𝐹)
143	137, 142	eleqtrd 2840	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → 𝑥 ∈ 𝐹)
144		elndif 4088	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐹 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
145	143, 144	syl 17	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) ∧ ¬ 𝑥 ∈ (𝐸‘𝑛)) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
146	127, 145	condan 816	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
147	146	ralrimiva 3143	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
148		vex 3449	. . . . . . . . 9 ⊢ 𝑥 ∈ V
149		eliin 4959	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛)))
150	148, 149	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ ∀𝑛 ∈ 𝑍 𝑥 ∈ (𝐸‘𝑛))
151	147, 150	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
152	151	ssd 43280	. . . . . 6 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) ⊆ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
153		ssid 3966	. . . . . . . . . . . 12 ⊢ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)
154	153	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝐾) ⊆ (𝐸‘𝐾))
155		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝐾 → (𝐸‘𝑛) = (𝐸‘𝐾))
156	155	sseq1d 3975	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝐾 → ((𝐸‘𝑛) ⊆ (𝐸‘𝐾) ↔ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)))
157	156	rspcev 3581	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ 𝑍 ∧ (𝐸‘𝐾) ⊆ (𝐸‘𝐾)) → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
158	15, 154, 157	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
159		iinss 5016	. . . . . . . . . 10 ⊢ (∃𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
160	158, 159	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
161	160	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝐾))
162		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
163	161, 162	sseldd 3945	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ (𝐸‘𝐾))
164		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛𝑥
165		nfii1 4989	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑛∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
166	164, 165	nfel 2921	. . . . . . . . . . . 12 ⊢ Ⅎ𝑛 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)
167		iinss2 5017	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝑍 → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
168	167	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ⊆ (𝐸‘𝑛))
169		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
170	168, 169	sseldd 3945	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → 𝑥 ∈ (𝐸‘𝑛))
171		elndif 4088	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐸‘𝑛) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
172	170, 171	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) ∧ 𝑛 ∈ 𝑍) → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
173	172	ex 413	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → (𝑛 ∈ 𝑍 → ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛))))
174	166, 173	ralrimi 3240	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
175		ralnex 3075	. . . . . . . . . . 11 ⊢ (∀𝑛 ∈ 𝑍 ¬ 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)) ↔ ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
176	174, 175	sylib 217	. . . . . . . . . 10 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ ∃𝑛 ∈ 𝑍 𝑥 ∈ ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
177	176, 135	sylnibr 328	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
178	177	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
179	140	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝐹 = ∪ 𝑛 ∈ 𝑍 ((𝐸‘𝐾) ∖ (𝐸‘𝑛)))
180	178, 179	neleqtrrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → ¬ 𝑥 ∈ 𝐹)
181	163, 180	eldifd 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) → 𝑥 ∈ ((𝐸‘𝐾) ∖ 𝐹))
182	152, 181	eqelssd 3965	. . . . 5 ⊢ (𝜑 → ((𝐸‘𝐾) ∖ 𝐹) = ∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛))
183	182	fveq2d 6846	. . . 4 ⊢ (𝜑 → (𝑀‘((𝐸‘𝐾) ∖ 𝐹)) = (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))
184	126, 183	eqtr2d 2777	. . 3 ⊢ (𝜑 → (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) = ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹)))
185	103, 184	breq12d 5118	. 2 ⊢ (𝜑 → (𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)) ↔ (𝑛 ∈ 𝑍 ↦ (𝑀‘(𝐸‘𝑛))) ⇝ ((𝑀‘(𝐸‘𝐾)) − (𝑀‘𝐹))))
186	101, 185	mpbird 256	1 ⊢ (𝜑 → 𝑆 ⇝ (𝑀‘∩ 𝑛 ∈ 𝑍 (𝐸‘𝑛)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ∪ ciun 4954 ∩ ciin 4955 class class class wbr 5105 ↦ cmpt 5188 dom cdm 5633 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ωcom 7802 ≼ cdom 8881 ℂcc 11049 ℝcr 11050 1c1 11052 + caddc 11054 − cmin 11385 ℤcz 12499 ℤ_≥cuz 12763 ..^cfzo 13567 ⇝ cli 15366 SAlgcsalg 44539 Meascmea 44680

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-disj 5071 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-omul 8417 df-er 8648 df-map 8767 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9378 df-oi 9446 df-card 9875 df-acn 9878 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-xadd 13034 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-sum 15571 df-salg 44540 df-sumge0 44594 df-mea 44681

This theorem is referenced by: meaiininc 44718

W3C validator