vitalilem4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vitalilem4		Structured version Visualization version GIF version

Theorem vitalilem4 23186

Description: Lemma for vitali 23188. (Contributed by Mario Carneiro, 16-Jun-2014.)

**Hypotheses**
Ref	Expression
vitali.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
vitali.2	⊢ 𝑆 = ((0[,]1) / ∼ )
vitali.3	⊢ (𝜑 → 𝐹 Fn 𝑆)
vitali.4	⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
vitali.5	⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
vitali.6	⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
vitali.7	⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))

**Assertion**
Ref	Expression
vitalilem4	⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0)

Distinct variable groups: 𝑚,𝑛,𝑠,𝑥,𝑦,𝑧,𝐺 𝜑,𝑚,𝑛,𝑥,𝑧 𝑧,𝑆 𝑇,𝑚,𝑥 𝑚,𝐹,𝑛,𝑠,𝑥,𝑦,𝑧 ∼ ,𝑚,𝑛,𝑠,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑦,𝑠) 𝑆(𝑥,𝑦,𝑚,𝑛,𝑠) 𝑇(𝑦,𝑧,𝑛,𝑠)

Proof of Theorem vitalilem4 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6103	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (𝐺‘𝑛) = (𝐺‘𝑚))
2	1	oveq2d 6565	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (𝑠 − (𝐺‘𝑛)) = (𝑠 − (𝐺‘𝑚)))
3	2	eleq1d 2672	. . . . . . 7 ⊢ (𝑛 = 𝑚 → ((𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹 ↔ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹))
4	3	rabbidv 3164	. . . . . 6 ⊢ (𝑛 = 𝑚 → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
5		vitali.6	. . . . . 6 ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹})
6		reex 9906	. . . . . . 7 ⊢ ℝ ∈ V
7	6	rabex 4740	. . . . . 6 ⊢ {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} ∈ V
8	4, 5, 7	fvmpt 6191	. . . . 5 ⊢ (𝑚 ∈ ℕ → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
9	8	adantl 481	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
10	9	fveq2d 6107	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) = (vol‘{𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}))
11		vitali.1	. . . . . . . 8 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (0[,]1) ∧ 𝑦 ∈ (0[,]1)) ∧ (𝑥 − 𝑦) ∈ ℚ)}
12		vitali.2	. . . . . . . 8 ⊢ 𝑆 = ((0[,]1) / ∼ )
13		vitali.3	. . . . . . . 8 ⊢ (𝜑 → 𝐹 Fn 𝑆)
14		vitali.4	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ 𝑆 (𝑧 ≠ ∅ → (𝐹‘𝑧) ∈ 𝑧))
15		vitali.5	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)))
16		vitali.7	. . . . . . . 8 ⊢ (𝜑 → ¬ ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
17	11, 12, 13, 14, 15, 5, 16	vitalilem2 23184	. . . . . . 7 ⊢ (𝜑 → (ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∧ ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2)))
18	17	simp1d 1066	. . . . . 6 ⊢ (𝜑 → ran 𝐹 ⊆ (0[,]1))
19		unitssre 12190	. . . . . 6 ⊢ (0[,]1) ⊆ ℝ
20	18, 19	syl6ss 3580	. . . . 5 ⊢ (𝜑 → ran 𝐹 ⊆ ℝ)
21	20	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ran 𝐹 ⊆ ℝ)
22		neg1rr 11002	. . . . . 6 ⊢ -1 ∈ ℝ
23		1re 9918	. . . . . 6 ⊢ 1 ∈ ℝ
24		iccssre 12126	. . . . . 6 ⊢ ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → (-1[,]1) ⊆ ℝ)
25	22, 23, 24	mp2an 704	. . . . 5 ⊢ (-1[,]1) ⊆ ℝ
26		inss2 3796	. . . . . 6 ⊢ (ℚ ∩ (-1[,]1)) ⊆ (-1[,]1)
27		f1of 6050	. . . . . . . 8 ⊢ (𝐺:ℕ–1-1-onto→(ℚ ∩ (-1[,]1)) → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
28	15, 27	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐺:ℕ⟶(ℚ ∩ (-1[,]1)))
29	28	ffvelrnda 6267	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (ℚ ∩ (-1[,]1)))
30	26, 29	sseldi 3566	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ (-1[,]1))
31	25, 30	sseldi 3566	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) ∈ ℝ)
32		eqidd 2611	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹} = {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹})
33	21, 31, 32	ovolshft 23086	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘ran 𝐹) = (vol‘{𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑚)) ∈ ran 𝐹}))
34	10, 33	eqtr4d 2647	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) = (vol‘ran 𝐹))
35		3re 10971	. . . . . . . 8 ⊢ 3 ∈ ℝ
36	35	rexri 9976	. . . . . . 7 ⊢ 3 ∈ ℝ^*
37	36	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → 3 ∈ ℝ^)
38		3nn 11063	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℕ
39		nnrp 11718	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℕ → 3 ∈ ℝ⁺)
40	38, 39	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℝ⁺
41		0re 9919	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ∈ ℝ
42		0le1 10430	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 ≤ 1
43		ovolicc 23098	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1) → (vol*‘(0[,]1)) = (1 − 0))
44	41, 23, 42, 43	mp3an 1416	. . . . . . . . . . . . . . . . . . 19 ⊢ (vol*‘(0[,]1)) = (1 − 0)
45		1m0e1 11008	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 − 0) = 1
46	44, 45	eqtri 2632	. . . . . . . . . . . . . . . . . 18 ⊢ (vol*‘(0[,]1)) = 1
47	46, 23	eqeltri 2684	. . . . . . . . . . . . . . . . 17 ⊢ (vol*‘(0[,]1)) ∈ ℝ
48		ovolsscl 23061	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝐹 ⊆ (0[,]1) ∧ (0[,]1) ⊆ ℝ ∧ (vol‘(0[,]1)) ∈ ℝ) → (vol‘ran 𝐹) ∈ ℝ)
49	19, 47, 48	mp3an23 1408	. . . . . . . . . . . . . . . 16 ⊢ (ran 𝐹 ⊆ (0[,]1) → (vol*‘ran 𝐹) ∈ ℝ)
50	18, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (vol*‘ran 𝐹) ∈ ℝ)
51	50	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘ran 𝐹) ∈ ℝ)
52		simpr 476	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → 0 < (vol‘ran 𝐹))
53	51, 52	elrpd 11745	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘ran 𝐹) ∈ ℝ⁺)
54		rpdivcl 11732	. . . . . . . . . . . . 13 ⊢ ((3 ∈ ℝ⁺ ∧ (vol‘ran 𝐹) ∈ ℝ⁺) → (3 / (vol‘ran 𝐹)) ∈ ℝ⁺)
55	40, 53, 54	sylancr 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (3 / (vol‘ran 𝐹)) ∈ ℝ⁺)
56	55	rpred 11748	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (3 / (vol‘ran 𝐹)) ∈ ℝ)
57	55	rpge0d 11752	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → 0 ≤ (3 / (vol‘ran 𝐹)))
58		flge0nn0 12483	. . . . . . . . . . 11 ⊢ (((3 / (vol‘ran 𝐹)) ∈ ℝ ∧ 0 ≤ (3 / (vol‘ran 𝐹))) → (⌊‘(3 / (vol*‘ran 𝐹))) ∈ ℕ₀)
59	56, 57, 58	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (⌊‘(3 / (vol‘ran 𝐹))) ∈ ℕ₀)
60		nn0p1nn 11209	. . . . . . . . . 10 ⊢ ((⌊‘(3 / (vol‘ran 𝐹))) ∈ ℕ₀ → ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ∈ ℕ)
61	59, 60	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ∈ ℕ)
62	61	nnred 10912	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ∈ ℝ)
63	62, 51	remulcld 9949	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol*‘ran 𝐹)) ∈ ℝ)
64	63	rexrd 9968	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)) ∈ ℝ^)
65	6	elpw2 4755	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ)
66	20, 65	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ran 𝐹 ∈ 𝒫 ℝ)
67	66	anim1i 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
68		eldif 3550	. . . . . . . . . . . . . . . . 17 ⊢ (ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol) ↔ (ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol))
69	67, 68	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ ran 𝐹 ∈ dom vol) → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol))
70	69	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ (𝒫 ℝ ∖ dom vol)))
71	16, 70	mt3d 139	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐹 ∈ dom vol)
72	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ran 𝐹 ∈ dom vol)
73		inss1 3795	. . . . . . . . . . . . . . . 16 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℚ
74		qssre 11674	. . . . . . . . . . . . . . . 16 ⊢ ℚ ⊆ ℝ
75	73, 74	sstri 3577	. . . . . . . . . . . . . . 15 ⊢ (ℚ ∩ (-1[,]1)) ⊆ ℝ
76		fss 5969	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:ℕ⟶(ℚ ∩ (-1[,]1)) ∧ (ℚ ∩ (-1[,]1)) ⊆ ℝ) → 𝐺:ℕ⟶ℝ)
77	28, 75, 76	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:ℕ⟶ℝ)
78	77	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ)
79		shftmbl 23113	. . . . . . . . . . . . 13 ⊢ ((ran 𝐹 ∈ dom vol ∧ (𝐺‘𝑛) ∈ ℝ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol)
80	72, 78, 79	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑠 ∈ ℝ ∣ (𝑠 − (𝐺‘𝑛)) ∈ ran 𝐹} ∈ dom vol)
81	80, 5	fmptd 6292	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:ℕ⟶dom vol)
82	81	ffvelrnda 6267	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑇‘𝑚) ∈ dom vol)
83	82	ralrimiva 2949	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
84		iunmbl 23128	. . . . . . . . 9 ⊢ (∀𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
85	83, 84	syl 17	. . . . . . . 8 ⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
86		mblss 23106	. . . . . . . 8 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ)
87		ovolcl 23053	. . . . . . . 8 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ ℝ → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ^)
88	85, 86, 87	3syl 18	. . . . . . 7 ⊢ (𝜑 → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ^)
89	88	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ^*)
90		flltp1 12463	. . . . . . . 8 ⊢ ((3 / (vol‘ran 𝐹)) ∈ ℝ → (3 / (vol‘ran 𝐹)) < ((⌊‘(3 / (vol*‘ran 𝐹))) + 1))
91	56, 90	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (3 / (vol‘ran 𝐹)) < ((⌊‘(3 / (vol*‘ran 𝐹))) + 1))
92	35	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → 3 ∈ ℝ)
93	92, 62, 53	ltdivmul2d 11800	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ((3 / (vol‘ran 𝐹)) < ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ↔ 3 < (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol*‘ran 𝐹))))
94	91, 93	mpbid 221	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → 3 < (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol*‘ran 𝐹)))
95		nnuz 11599	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
96		1zzd 11285	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → 1 ∈ ℤ)
97		mblvol 23105	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇‘𝑚) ∈ dom vol → (vol‘(𝑇‘𝑚)) = (vol*‘(𝑇‘𝑚)))
98	82, 97	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) = (vol*‘(𝑇‘𝑚)))
99	98, 34	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) = (vol*‘ran 𝐹))
100	50	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘ran 𝐹) ∈ ℝ)
101	99, 100	eqeltrd 2688	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) ∈ ℝ)
102	101	adantlr 747	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 0 < (vol*‘ran 𝐹)) ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) ∈ ℝ)
103		eqid 2610	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))
104	102, 103	fmptd 6292	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))):ℕ⟶ℝ)
105	104	ffvelrnda 6267	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 0 < (vol*‘ran 𝐹)) ∧ 𝑘 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))‘𝑘) ∈ ℝ)
106	95, 96, 105	serfre 12692	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))):ℕ⟶ℝ)
107		frn 5966	. . . . . . . . . 10 ⊢ (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))):ℕ⟶ℝ → ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) ⊆ ℝ)
108	106, 107	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) ⊆ ℝ)
109		ressxr 9962	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ^*
110	108, 109	syl6ss 3580	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) ⊆ ℝ^)
111	99	adantlr 747	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 0 < (vol‘ran 𝐹)) ∧ 𝑚 ∈ ℕ) → (vol‘(𝑇‘𝑚)) = (vol‘ran 𝐹))
112	111	mpteq2dva 4672	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))) = (𝑚 ∈ ℕ ↦ (vol‘ran 𝐹)))
113		fconstmpt 5085	. . . . . . . . . . . . 13 ⊢ (ℕ × {(vol‘ran 𝐹)}) = (𝑚 ∈ ℕ ↦ (vol‘ran 𝐹))
114	112, 113	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))) = (ℕ × {(vol‘ran 𝐹)}))
115	114	seqeq3d 12671	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) = seq1( + , (ℕ × {(vol‘ran 𝐹)})))
116	115	fveq1d 6105	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) = (seq1( + , (ℕ × {(vol‘ran 𝐹)}))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)))
117	51	recnd 9947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘ran 𝐹) ∈ ℂ)
118		ser1const 12719	. . . . . . . . . . 11 ⊢ (((vol‘ran 𝐹) ∈ ℂ ∧ ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ∈ ℕ) → (seq1( + , (ℕ × {(vol‘ran 𝐹)}))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) = (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)))
119	117, 61, 118	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (seq1( + , (ℕ × {(vol‘ran 𝐹)}))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) = (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol*‘ran 𝐹)))
120	116, 119	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) = (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)))
121		ffn 5958	. . . . . . . . . . 11 ⊢ (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))):ℕ⟶ℝ → seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) Fn ℕ)
122	106, 121	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) Fn ℕ)
123		fnfvelrn 6264	. . . . . . . . . 10 ⊢ ((seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) Fn ℕ ∧ ((⌊‘(3 / (vol‘ran 𝐹))) + 1) ∈ ℕ) → (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) ∈ ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))))
124	122, 61, 123	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))‘((⌊‘(3 / (vol‘ran 𝐹))) + 1)) ∈ ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))))
125	120, 124	eqeltrrd 2689	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol*‘ran 𝐹)) ∈ ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))))
126		supxrub 12026	. . . . . . . 8 ⊢ ((ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) ⊆ ℝ^* ∧ (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)) ∈ ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))), ℝ^*, < ))
127	110, 125, 126	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)) ≤ sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))), ℝ^, < ))
128	85	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol)
129		mblvol 23105	. . . . . . . . 9 ⊢ (∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ∈ dom vol → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
130	128, 129	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
131	82, 101	jca 553	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑇‘𝑚) ∈ dom vol ∧ (vol‘(𝑇‘𝑚)) ∈ ℝ))
132	131	ralrimiva 2949	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑇‘𝑚) ∈ dom vol ∧ (vol‘(𝑇‘𝑚)) ∈ ℝ))
133	132	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → ∀𝑚 ∈ ℕ ((𝑇‘𝑚) ∈ dom vol ∧ (vol‘(𝑇‘𝑚)) ∈ ℝ))
134	11, 12, 13, 14, 15, 5, 16	vitalilem3 23185	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))
135	134	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → Disj 𝑚 ∈ ℕ (𝑇‘𝑚))
136		eqid 2610	. . . . . . . . . 10 ⊢ seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))) = seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚))))
137	136, 103	voliun 23129	. . . . . . . . 9 ⊢ ((∀𝑚 ∈ ℕ ((𝑇‘𝑚) ∈ dom vol ∧ (vol‘(𝑇‘𝑚)) ∈ ℝ) ∧ Disj 𝑚 ∈ ℕ (𝑇‘𝑚)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))), ℝ^*, < ))
138	133, 135, 137	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))), ℝ^, < ))
139	130, 138	eqtr3d 2646	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) = sup(ran seq1( + , (𝑚 ∈ ℕ ↦ (vol‘(𝑇‘𝑚)))), ℝ^*, < ))
140	127, 139	breqtrrd 4611	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (((⌊‘(3 / (vol‘ran 𝐹))) + 1) · (vol‘ran 𝐹)) ≤ (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
141	37, 64, 89, 94, 140	xrltletrd 11868	. . . . 5 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → 3 < (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
142	17	simp3d 1068	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))
143	142	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 0 < (vol*‘ran 𝐹)) → ∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2))
144		2re 10967	. . . . . . . . 9 ⊢ 2 ∈ ℝ
145		iccssre 12126	. . . . . . . . 9 ⊢ ((-1 ∈ ℝ ∧ 2 ∈ ℝ) → (-1[,]2) ⊆ ℝ)
146	22, 144, 145	mp2an 704	. . . . . . . 8 ⊢ (-1[,]2) ⊆ ℝ
147		ovolss 23060	. . . . . . . 8 ⊢ ((∪ 𝑚 ∈ ℕ (𝑇‘𝑚) ⊆ (-1[,]2) ∧ (-1[,]2) ⊆ ℝ) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ (vol‘(-1[,]2)))
148	143, 146, 147	sylancl 693	. . . . . . 7 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ (vol*‘(-1[,]2)))
149		2cn 10968	. . . . . . . . 9 ⊢ 2 ∈ ℂ
150		ax-1cn 9873	. . . . . . . . 9 ⊢ 1 ∈ ℂ
151	149, 150	subnegi 10239	. . . . . . . 8 ⊢ (2 − -1) = (2 + 1)
152		neg1lt0 11004	. . . . . . . . . . 11 ⊢ -1 < 0
153		2pos 10989	. . . . . . . . . . 11 ⊢ 0 < 2
154	22, 41, 144	lttri 10042	. . . . . . . . . . 11 ⊢ ((-1 < 0 ∧ 0 < 2) → -1 < 2)
155	152, 153, 154	mp2an 704	. . . . . . . . . 10 ⊢ -1 < 2
156	22, 144, 155	ltleii 10039	. . . . . . . . 9 ⊢ -1 ≤ 2
157		ovolicc 23098	. . . . . . . . 9 ⊢ ((-1 ∈ ℝ ∧ 2 ∈ ℝ ∧ -1 ≤ 2) → (vol*‘(-1[,]2)) = (2 − -1))
158	22, 144, 156, 157	mp3an 1416	. . . . . . . 8 ⊢ (vol*‘(-1[,]2)) = (2 − -1)
159		df-3 10957	. . . . . . . 8 ⊢ 3 = (2 + 1)
160	151, 158, 159	3eqtr4i 2642	. . . . . . 7 ⊢ (vol*‘(-1[,]2)) = 3
161	148, 160	syl6breq 4624	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 3)
162		xrlenlt 9982	. . . . . . 7 ⊢ (((vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ∈ ℝ^ ∧ 3 ∈ ℝ^) → ((vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 3 ↔ ¬ 3 < (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))
163	89, 36, 162	sylancl 693	. . . . . 6 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ((vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)) ≤ 3 ↔ ¬ 3 < (vol*‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚))))
164	161, 163	mpbid 221	. . . . 5 ⊢ ((𝜑 ∧ 0 < (vol‘ran 𝐹)) → ¬ 3 < (vol‘∪ 𝑚 ∈ ℕ (𝑇‘𝑚)))
165	141, 164	pm2.65da 598	. . . 4 ⊢ (𝜑 → ¬ 0 < (vol*‘ran 𝐹))
166		ovolge0 23056	. . . . . . 7 ⊢ (ran 𝐹 ⊆ ℝ → 0 ≤ (vol*‘ran 𝐹))
167	20, 166	syl 17	. . . . . 6 ⊢ (𝜑 → 0 ≤ (vol*‘ran 𝐹))
168		0xr 9965	. . . . . . 7 ⊢ 0 ∈ ℝ^*
169		ovolcl 23053	. . . . . . . 8 ⊢ (ran 𝐹 ⊆ ℝ → (vol‘ran 𝐹) ∈ ℝ^)
170	20, 169	syl 17	. . . . . . 7 ⊢ (𝜑 → (vol‘ran 𝐹) ∈ ℝ^)
171		xrleloe 11853	. . . . . . 7 ⊢ ((0 ∈ ℝ^* ∧ (vol‘ran 𝐹) ∈ ℝ^) → (0 ≤ (vol‘ran 𝐹) ↔ (0 < (vol‘ran 𝐹) ∨ 0 = (vol*‘ran 𝐹))))
172	168, 170, 171	sylancr 694	. . . . . 6 ⊢ (𝜑 → (0 ≤ (vol‘ran 𝐹) ↔ (0 < (vol‘ran 𝐹) ∨ 0 = (vol*‘ran 𝐹))))
173	167, 172	mpbid 221	. . . . 5 ⊢ (𝜑 → (0 < (vol‘ran 𝐹) ∨ 0 = (vol‘ran 𝐹)))
174	173	ord 391	. . . 4 ⊢ (𝜑 → (¬ 0 < (vol‘ran 𝐹) → 0 = (vol‘ran 𝐹)))
175	165, 174	mpd 15	. . 3 ⊢ (𝜑 → 0 = (vol*‘ran 𝐹))
176	175	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 0 = (vol*‘ran 𝐹))
177	34, 176	eqtr4d 2647	1 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (vol*‘(𝑇‘𝑚)) = 0)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 {crab 2900 ∖ cdif 3537 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 𝒫 cpw 4108 {csn 4125 ∪ ciun 4455 Disj wdisj 4553 class class class wbr 4583 {copab 4642 ↦ cmpt 4643 × cxp 5036 dom cdm 5038 ran crn 5039 Fn wfn 5799 ⟶wf 5800 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 / cqs 7628 supcsup 8229 ℂcc 9813 ℝcr 9814 0cc0 9815 1c1 9816 + caddc 9818 · cmul 9820 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 -cneg 10146 / cdiv 10563 ℕcn 10897 2c2 10947 3c3 10948 ℕ₀cn0 11169 ℚcq 11664 ℝ⁺crp 11708 [,]cicc 12049 ⌊cfl 12453 seqcseq 12663 vol*covol 23038 volcvol 23039

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cc 9140 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-ec 7631 df-qs 7635 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-rlim 14068 df-sum 14265 df-rest 15906 df-topgen 15927 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-top 20521 df-bases 20522 df-topon 20523 df-cmp 21000 df-ovol 23040 df-vol 23041

This theorem is referenced by: vitalilem5 23187

W3C validator