caratheodorylem1 - Mathbox for Glauco Siliprandi

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

Theorem caratheodorylem1 40740

Description: Lemma used to prove that Caratheodory's construction is sigma-additive. This is the proof of the statement in the middle of Step (e) in the proof of Theorem 113C of [Fremlin1] p. 21. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
caratheodorylem1.o	⊢ (𝜑 → 𝑂 ∈ OutMeas)
caratheodorylem1.s	⊢ 𝑆 = (CaraGen‘𝑂)
caratheodorylem1.z	⊢ 𝑍 = (ℤ_≥‘𝑀)
caratheodorylem1.e	⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
caratheodorylem1.dj	⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
caratheodorylem1.g	⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
caratheodorylem1.n	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))

**Assertion**
Ref	Expression
caratheodorylem1	⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Distinct variable groups: 𝑖,𝐸,𝑛 𝑖,𝐺,𝑛 𝑖,𝑀,𝑛 𝑖,𝑁,𝑛 𝑖,𝑂,𝑛 𝑛,𝑍 𝜑,𝑖,𝑛 Allowed substitution hints: 𝑆(𝑖,𝑛) 𝑍(𝑖)

Proof of Theorem caratheodorylem1 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		caratheodorylem1.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
2		eluzfz2 12349	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝑁 ∈ (𝑀...𝑁))
4		id 22	. 2 ⊢ (𝜑 → 𝜑)
5		fveq2 6191	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝐺‘𝑗) = (𝐺‘𝑀))
6	5	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑀 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑀)))
7		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = 𝑀 → (𝑀...𝑗) = (𝑀...𝑀))
8	7	mpteq1d 4738	. . . . . 6 ⊢ (𝑗 = 𝑀 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))
9	8	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑀 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
10	6, 9	eqeq12d 2637	. . . 4 ⊢ (𝑗 = 𝑀 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
11	10	imbi2d 330	. . 3 ⊢ (𝑗 = 𝑀 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))))
12		fveq2 6191	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝐺‘𝑗) = (𝐺‘𝑖))
13	12	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑖 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑖)))
14		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = 𝑖 → (𝑀...𝑗) = (𝑀...𝑖))
15	14	mpteq1d 4738	. . . . . 6 ⊢ (𝑗 = 𝑖 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))
16	15	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑖 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
17	13, 16	eqeq12d 2637	. . . 4 ⊢ (𝑗 = 𝑖 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
18	17	imbi2d 330	. . 3 ⊢ (𝑗 = 𝑖 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))))
19		fveq2 6191	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝐺‘𝑗) = (𝐺‘(𝑖 + 1)))
20	19	fveq2d 6195	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘(𝑖 + 1))))
21		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = (𝑖 + 1) → (𝑀...𝑗) = (𝑀...(𝑖 + 1)))
22	21	mpteq1d 4738	. . . . . 6 ⊢ (𝑗 = (𝑖 + 1) → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))
23	22	fveq2d 6195	. . . . 5 ⊢ (𝑗 = (𝑖 + 1) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
24	20, 23	eqeq12d 2637	. . . 4 ⊢ (𝑗 = (𝑖 + 1) → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛))))))
25	24	imbi2d 330	. . 3 ⊢ (𝑗 = (𝑖 + 1) → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
26		fveq2 6191	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝐺‘𝑗) = (𝐺‘𝑁))
27	26	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑁 → (𝑂‘(𝐺‘𝑗)) = (𝑂‘(𝐺‘𝑁)))
28		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = 𝑁 → (𝑀...𝑗) = (𝑀...𝑁))
29	28	mpteq1d 4738	. . . . . 6 ⊢ (𝑗 = 𝑁 → (𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))
30	29	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝑁 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))
31	27, 30	eqeq12d 2637	. . . 4 ⊢ (𝑗 = 𝑁 → ((𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛)))) ↔ (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
32	31	imbi2d 330	. . 3 ⊢ (𝑗 = 𝑁 → ((𝜑 → (𝑂‘(𝐺‘𝑗)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑗) ↦ (𝑂‘(𝐸‘𝑛))))) ↔ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))))
33		eluzel2 11692	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
34	1, 33	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
35		fzsn 12383	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
36	34, 35	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑀...𝑀) = {𝑀})
37	36	mpteq1d 4738	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
38	37	fveq2d 6195	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))) = (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))))
39		caratheodorylem1.o	. . . . . . . . 9 ⊢ (𝜑 → 𝑂 ∈ OutMeas)
40	39	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑂 ∈ OutMeas)
41		eqid 2622	. . . . . . . 8 ⊢ ∪ dom 𝑂 = ∪ dom 𝑂
42		caratheodorylem1.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (CaraGen‘𝑂)
43	42	caragenss 40718	. . . . . . . . . . 11 ⊢ (𝑂 ∈ OutMeas → 𝑆 ⊆ dom 𝑂)
44	40, 43	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑆 ⊆ dom 𝑂)
45		caratheodorylem1.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸:𝑍⟶𝑆)
46	45	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝐸:𝑍⟶𝑆)
47		elsni 4194	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ {𝑀} → 𝑛 = 𝑀)
48	47	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 = 𝑀)
49		uzid 11702	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ_≥‘𝑀))
50	34, 49	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘𝑀))
51		caratheodorylem1.z	. . . . . . . . . . . . . 14 ⊢ 𝑍 = (ℤ_≥‘𝑀)
52	50, 51	syl6eleqr 2712	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ 𝑍)
53	52	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑀 ∈ 𝑍)
54	48, 53	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → 𝑛 ∈ 𝑍)
55	46, 54	ffvelrnd 6360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ 𝑆)
56	44, 55	sseldd 3604	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ∈ dom 𝑂)
57		elssuni 4467	. . . . . . . . 9 ⊢ ((𝐸‘𝑛) ∈ dom 𝑂 → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
58	56, 57	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
59	40, 41, 58	omecl 40717	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ {𝑀}) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
60		eqid 2622	. . . . . . 7 ⊢ (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))
61	59, 60	fmptd 6385	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))):{𝑀}⟶(0[,]+∞))
62	34, 61	sge0sn 40596	. . . . 5 ⊢ (𝜑 → (Σ^{^}‘(𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀))
63		eqidd 2623	. . . . . 6 ⊢ (𝜑 → (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))) = (𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛))))
64	36	iuneq1d 4545	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) = ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖))
65		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝐸‘𝑖) = (𝐸‘𝑀))
66	65	iunxsng 4602	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑍 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
67	52, 66	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ {𝑀} (𝐸‘𝑖) = (𝐸‘𝑀))
68		eqidd 2623	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘𝑀) = (𝐸‘𝑀))
69	64, 67, 68	3eqtrrd 2661	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
70	69	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
71		fveq2 6191	. . . . . . . . 9 ⊢ (𝑛 = 𝑀 → (𝐸‘𝑛) = (𝐸‘𝑀))
72	71	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐸‘𝑀))
73		caratheodorylem1.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖))
74	73	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)))
75		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
76	75	iuneq1d 4545	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑀 → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
77	76	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
78		ovex 6678	. . . . . . . . . . . 12 ⊢ (𝑀...𝑀) ∈ V
79		fvex 6201	. . . . . . . . . . . 12 ⊢ (𝐸‘𝑖) ∈ V
80	78, 79	iunex 7147	. . . . . . . . . . 11 ⊢ ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V
81	80	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖) ∈ V)
82	74, 77, 52, 81	fvmptd 6288	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
83	82	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐺‘𝑀) = ∪ 𝑖 ∈ (𝑀...𝑀)(𝐸‘𝑖))
84	70, 72, 83	3eqtr4d 2666	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝐸‘𝑛) = (𝐺‘𝑀))
85	84	fveq2d 6195	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 = 𝑀) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐺‘𝑀)))
86		snidg 4206	. . . . . . 7 ⊢ (𝑀 ∈ 𝑍 → 𝑀 ∈ {𝑀})
87	52, 86	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ {𝑀})
88		fvexd 6203	. . . . . 6 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) ∈ V)
89	63, 85, 87, 88	fvmptd 6288	. . . . 5 ⊢ (𝜑 → ((𝑛 ∈ {𝑀} ↦ (𝑂‘(𝐸‘𝑛)))‘𝑀) = (𝑂‘(𝐺‘𝑀)))
90	38, 62, 89	3eqtrrd 2661	. . . 4 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛)))))
91	90	a1i 11	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝜑 → (𝑂‘(𝐺‘𝑀)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑀) ↦ (𝑂‘(𝐸‘𝑛))))))
92		simp3 1063	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝜑)
93		simp1 1061	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → 𝑖 ∈ (𝑀..^𝑁))
94		id 22	. . . . . . 7 ⊢ ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))))
95	94	imp 445	. . . . . 6 ⊢ (((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
96	95	3adant1 1079	. . . . 5 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
97		elfzoel1 12468	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℤ)
98		elfzoelz 12470	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
99	98	peano2zd 11485	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℤ)
100	97, 99, 99	3jca 1242	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ))
101	97	zred 11482	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ∈ ℝ)
102	99	zred 11482	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ ℝ)
103	98	zred 11482	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℝ)
104		elfzole1 12478	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ 𝑖)
105	103	ltp1d 10954	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 < (𝑖 + 1))
106	101, 103, 102, 104, 105	lelttrd 10195	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 < (𝑖 + 1))
107	101, 102, 106	ltled 10185	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑀 ≤ (𝑖 + 1))
108		leid 10133	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 + 1) ∈ ℝ → (𝑖 + 1) ≤ (𝑖 + 1))
109	102, 108	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ≤ (𝑖 + 1))
110	100, 107, 109	jca32 558	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1))))
111		elfz2 12333	. . . . . . . . . . . . . 14 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) ↔ ((𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ) ∧ (𝑀 ≤ (𝑖 + 1) ∧ (𝑖 + 1) ≤ (𝑖 + 1))))
112	110, 111	sylibr 224	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (𝑀..^𝑁) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
113	112	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑀...(𝑖 + 1)))
114		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑖 + 1) → (𝐸‘𝑗) = (𝐸‘(𝑖 + 1)))
115	114	ssiun2s 4564	. . . . . . . . . . . 12 ⊢ ((𝑖 + 1) ∈ (𝑀...(𝑖 + 1)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
116	113, 115	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
117		fveq2 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗))
118	117	cbviunv 4559	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)
119	118	mpteq2i 4741	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝑍 ↦ ∪ 𝑖 ∈ (𝑀...𝑛)(𝐸‘𝑖)) = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
120	73, 119	eqtri 2644	. . . . . . . . . . . . . 14 ⊢ 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗))
121	120	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
122		oveq2 6658	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑖 + 1) → (𝑀...𝑛) = (𝑀...(𝑖 + 1)))
123	122	iuneq1d 4545	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑖 + 1) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
124	123	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 = (𝑖 + 1)) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
125	34	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
126	98	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
127	126	peano2zd 11485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℤ)
128	125	zred 11482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℝ)
129	127	zred 11482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ ℝ)
130	126	zred 11482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℝ)
131	104	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ 𝑖)
132	130	ltp1d 10954	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 < (𝑖 + 1))
133	128, 130, 129, 131, 132	lelttrd 10195	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 < (𝑖 + 1))
134	128, 129, 133	ltled 10185	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ≤ (𝑖 + 1))
135	125, 127, 134	3jca 1242	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
136		eluz2 11693	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 + 1) ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑖 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑖 + 1)))
137	135, 136	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (ℤ_≥‘𝑀))
138	51	eqcomi 2631	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) = 𝑍
139	137, 138	syl6eleq 2711	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ 𝑍)
140		ovex 6678	. . . . . . . . . . . . . . 15 ⊢ (𝑀...(𝑖 + 1)) ∈ V
141		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (𝐸‘𝑗) ∈ V
142	140, 141	iunex 7147	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V
143	142	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ∈ V)
144	121, 124, 139, 143	fvmptd 6288	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗))
145	144	eqcomd 2628	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (𝐺‘(𝑖 + 1)))
146	116, 145	sseqtrd 3641	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)))
147		sseqin2 3817	. . . . . . . . . . 11 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) ↔ ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
148	147	biimpi 206	. . . . . . . . . 10 ⊢ ((𝐸‘(𝑖 + 1)) ⊆ (𝐺‘(𝑖 + 1)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
149	146, 148	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1))) = (𝐸‘(𝑖 + 1)))
150	149	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐸‘(𝑖 + 1))))
151		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝐸‘(𝑖 + 1))
152		elfzouz 12474	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ (ℤ_≥‘𝑀))
153	152	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ (ℤ_≥‘𝑀))
154	151, 153, 114	iunp1 39235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
155	144, 154	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))))
156	155	difeq1d 3727	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
157		caratheodorylem1.dj	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛))
158		fveq2 6191	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑗 → (𝐸‘𝑛) = (𝐸‘𝑗))
159	158	cbvdisjv 4631	. . . . . . . . . . . . . . 15 ⊢ (Disj 𝑛 ∈ 𝑍 (𝐸‘𝑛) ↔ Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
160	157, 159	sylib 208	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
161	160	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → Disj 𝑗 ∈ 𝑍 (𝐸‘𝑗))
162		fzssuz 12382	. . . . . . . . . . . . . . 15 ⊢ (𝑀...𝑖) ⊆ (ℤ_≥‘𝑀)
163	162, 138	sseqtri 3637	. . . . . . . . . . . . . 14 ⊢ (𝑀...𝑖) ⊆ 𝑍
164	163	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑀...𝑖) ⊆ 𝑍)
165		fzp1nel 12424	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑖 + 1) ∈ (𝑀...𝑖)
166	165	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
167	166	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ¬ (𝑖 + 1) ∈ (𝑀...𝑖))
168	139, 167	eldifd 3585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 + 1) ∈ (𝑍 ∖ (𝑀...𝑖)))
169	161, 164, 168, 114	disjiun2 39226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅)
170		undif4 4035	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∩ (𝐸‘(𝑖 + 1))) = ∅ → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
171	169, 170	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))))
172	171	eqcomd 2628	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ (𝐸‘(𝑖 + 1))) ∖ (𝐸‘(𝑖 + 1))) = (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))))
173		simpl 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝜑)
174	153, 138	syl6eleq 2711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ 𝑍)
175	120	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝐺 = (𝑛 ∈ 𝑍 ↦ ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗)))
176		simpr 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → 𝑛 = 𝑖)
177	176	oveq2d 6666	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → (𝑀...𝑛) = (𝑀...𝑖))
178	177	iuneq1d 4545	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑛 = 𝑖) → ∪ 𝑗 ∈ (𝑀...𝑛)(𝐸‘𝑗) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
179		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → 𝑖 ∈ 𝑍)
180		ovex 6678	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑖) ∈ V
181	180, 141	iunex 7147	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V
182	181	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∈ V)
183	175, 178, 179, 182	fvmptd 6288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
184	173, 174, 183	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) = ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗))
185	184	eqcomd 2628	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) = (𝐺‘𝑖))
186		difid 3948	. . . . . . . . . . . . 13 ⊢ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅
187	186	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = ∅)
188	185, 187	uneq12d 3768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = ((𝐺‘𝑖) ∪ ∅))
189		un0 3967	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖)
190	189	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘𝑖) ∪ ∅) = (𝐺‘𝑖))
191	188, 190	eqtrd 2656	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ∪ ((𝐸‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝐺‘𝑖))
192	156, 172, 191	3eqtrd 2660	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))) = (𝐺‘𝑖))
193	192	fveq2d 6195	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1)))) = (𝑂‘(𝐺‘𝑖)))
194	150, 193	oveq12d 6668	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
195	194	3adant3 1081	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
196	39	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑂 ∈ OutMeas)
197	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝐸:𝑍⟶𝑆)
198	197, 139	ffvelrnd 6360	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ∈ 𝑆)
199		simpll 790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
200	97	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ∈ ℤ)
201		elfzelz 12342	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑗 ∈ ℤ)
202	201	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ ℤ)
203		elfzle1 12344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (𝑀...(𝑖 + 1)) → 𝑀 ≤ 𝑗)
204	203	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑀 ≤ 𝑗)
205	200, 202, 204	3jca 1242	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
206		eluz2 11693	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑀 ≤ 𝑗))
207	205, 206	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ (ℤ_≥‘𝑀))
208	207, 138	syl6eleq 2711	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
209	208	adantll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → 𝑗 ∈ 𝑍)
210	39, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑆 ⊆ dom 𝑂)
211	210	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑆 ⊆ dom 𝑂)
212	45	ffvelrnda 6359	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ 𝑆)
213	211, 212	sseldd 3604	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ∈ dom 𝑂)
214		elssuni 4467	. . . . . . . . . . . . . 14 ⊢ ((𝐸‘𝑗) ∈ dom 𝑂 → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
215	213, 214	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
216	199, 209, 215	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑗 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
217	216	ralrimiva 2966	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
218		iunss 4561	. . . . . . . . . . 11 ⊢ (∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
219	217, 218	sylibr 224	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ∪ 𝑗 ∈ (𝑀...(𝑖 + 1))(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
220	144, 219	eqsstrd 3639	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
221	196, 42, 41, 198, 220	caragensplit 40714	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))) = (𝑂‘(𝐺‘(𝑖 + 1))))
222	221	eqcomd 2628	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
223	222	3adant3 1081	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = ((𝑂‘((𝐺‘(𝑖 + 1)) ∩ (𝐸‘(𝑖 + 1)))) +_𝑒 (𝑂‘((𝐺‘(𝑖 + 1)) ∖ (𝐸‘(𝑖 + 1))))))
224	196	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑂 ∈ OutMeas)
225	173	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝜑)
226		elfzuz 12338	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ (ℤ_≥‘𝑀))
227	226, 138	syl6eleq 2711	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (𝑀...(𝑖 + 1)) → 𝑛 ∈ 𝑍)
228	227	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → 𝑛 ∈ 𝑍)
229	45, 210	fssd 6057	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:𝑍⟶dom 𝑂)
230	229	ffvelrnda 6359	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ∈ dom 𝑂)
231	230, 57	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
232	225, 228, 231	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝐸‘𝑛) ⊆ ∪ dom 𝑂)
233	224, 41, 232	omecl 40717	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) ∧ 𝑛 ∈ (𝑀...(𝑖 + 1))) → (𝑂‘(𝐸‘𝑛)) ∈ (0[,]+∞))
234		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑛 = (𝑖 + 1) → (𝐸‘𝑛) = (𝐸‘(𝑖 + 1)))
235	234	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑛 = (𝑖 + 1) → (𝑂‘(𝐸‘𝑛)) = (𝑂‘(𝐸‘(𝑖 + 1))))
236	153, 233, 235	sge0p1 40631	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
237	236	3adant3 1081	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
238		id 22	. . . . . . . . . 10 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))))
239	238	eqcomd 2628	. . . . . . . . 9 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) = (𝑂‘(𝐺‘𝑖)))
240	239	oveq1d 6665	. . . . . . . 8 ⊢ ((𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
241	240	3ad2ant3 1084	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛)))) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))))
242		simpl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝜑)
243	163	sseli 3599	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (𝑀...𝑖) → 𝑗 ∈ 𝑍)
244	243	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → 𝑗 ∈ 𝑍)
245	242, 244, 215	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
246	245	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑍) ∧ 𝑗 ∈ (𝑀...𝑖)) → (𝐸‘𝑗) ⊆ ∪ dom 𝑂)
247	246	ralrimiva 2966	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
248		iunss 4561	. . . . . . . . . . . . 13 ⊢ (∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂 ↔ ∀𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
249	247, 248	sylibr 224	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → ∪ 𝑗 ∈ (𝑀...𝑖)(𝐸‘𝑗) ⊆ ∪ dom 𝑂)
250	183, 249	eqsstrd 3639	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑍) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
251	173, 174, 250	syl2anc 693	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐺‘𝑖) ⊆ ∪ dom 𝑂)
252	196, 41, 251	omexrcl 40721	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐺‘𝑖)) ∈ ℝ^*)
253	116, 219	sstrd 3613	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝐸‘(𝑖 + 1)) ⊆ ∪ dom 𝑂)
254	196, 41, 253	omexrcl 40721	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑂‘(𝐸‘(𝑖 + 1))) ∈ ℝ^*)
255	252, 254	xaddcomd 39540	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
256	255	3adant3 1081	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → ((𝑂‘(𝐺‘𝑖)) +_𝑒 (𝑂‘(𝐸‘(𝑖 + 1)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
257	237, 241, 256	3eqtrd 2660	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))) = ((𝑂‘(𝐸‘(𝑖 + 1))) +_𝑒 (𝑂‘(𝐺‘𝑖))))
258	195, 223, 257	3eqtr4d 2666	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (𝑀..^𝑁) ∧ (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
259	92, 93, 96, 258	syl3anc 1326	. . . 4 ⊢ ((𝑖 ∈ (𝑀..^𝑁) ∧ (𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) ∧ 𝜑) → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))
260	259	3exp 1264	. . 3 ⊢ (𝑖 ∈ (𝑀..^𝑁) → ((𝜑 → (𝑂‘(𝐺‘𝑖)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑖) ↦ (𝑂‘(𝐸‘𝑛))))) → (𝜑 → (𝑂‘(𝐺‘(𝑖 + 1))) = (Σ^{^}‘(𝑛 ∈ (𝑀...(𝑖 + 1)) ↦ (𝑂‘(𝐸‘𝑛)))))))
261	11, 18, 25, 32, 91, 260	fzind2 12586	. 2 ⊢ (𝑁 ∈ (𝑀...𝑁) → (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛))))))
262	3, 4, 261	sylc 65	1 ⊢ (𝜑 → (𝑂‘(𝐺‘𝑁)) = (Σ^{^}‘(𝑛 ∈ (𝑀...𝑁) ↦ (𝑂‘(𝐸‘𝑛)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 {csn 4177 ∪ cuni 4436 ∪ ciun 4520 Disj wdisj 4620 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 +∞cpnf 10071 ≤ cle 10075 ℤcz 11377 ℤ_≥cuz 11687 +_𝑒 cxad 11944 [,]cicc 12178 ...cfz 12326 ..^cfzo 12465 Σ^{^}csumge0 40579 OutMeascome 40703 CaraGenccaragen 40705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-xadd 11947 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-sumge0 40580 df-ome 40704 df-caragen 40706

This theorem is referenced by: caratheodorylem2 40741

W3C validator