Metamath Proof Explorer

Theorem vitalilem4

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

Ref Expression
Hypotheses 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 vitalilem4 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 0 [,] 1 ) ∧ 𝑦 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 − 𝑦 ) ∈ ℚ ) }
2 vitali.2 ⊢ 𝑆 = ( ( 0 [,] 1 ) / ∼ )
3 vitali.3 ⊢ ( 𝜑 → 𝐹 Fn 𝑆 )
4 vitali.4 ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 ( 𝑧 ≠ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ 𝑧 ) )
5 vitali.5 ⊢ ( 𝜑 → 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) )
6 vitali.6 ⊢ 𝑇 = ( 𝑛 ∈ ℕ ↦ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } )
7 vitali.7 ⊢ ( 𝜑 → ¬ ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
8 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑚 ) )
9 8 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) = ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) )
10 9 eleq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 ↔ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 ) )
11 10 rabbidv ⊢ ( 𝑛 = 𝑚 → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
12 reex ⊢ ℝ ∈ V
13 12 rabex ⊢ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ∈ V
14 11 6 13 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
16 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ) )
17 1 2 3 4 5 6 7 vitalilem2 ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∧ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ) )
18 17 simp1d ⊢ ( 𝜑 → ran 𝐹 ⊆ ( 0 [,] 1 ) )
19 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
20 18 19 sstrdi ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ran 𝐹 ⊆ ℝ )
22 neg1rr ⊢ - 1 ∈ ℝ
23 1re ⊢ 1 ∈ ℝ
24 iccssre ⊢ ( ( - 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( - 1 [,] 1 ) ⊆ ℝ )
25 22 23 24 mp2an ⊢ ( - 1 [,] 1 ) ⊆ ℝ
26 f1of ⊢ ( 𝐺 : ℕ –1-1-onto→ ( ℚ ∩ ( - 1 [,] 1 ) ) → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
27 5 26 syl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) )
28 27 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ( ℚ ∩ ( - 1 [,] 1 ) ) )
29 28 elin2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ( - 1 [,] 1 ) )
30 25 29 sselid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐺 ‘ 𝑚 ) ∈ ℝ )
31 eqidd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } = { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } )
32 21 30 31 ovolshft ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ran 𝐹 ) = ( vol* ‘ { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑚 ) ) ∈ ran 𝐹 } ) )
33 16 32 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ran 𝐹 ) )
34 3re ⊢ 3 ∈ ℝ
35 34 rexri ⊢ 3 ∈ ℝ*
36 35 a1i ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 3 ∈ ℝ* )
37 3rp ⊢ 3 ∈ ℝ+
38 0re ⊢ 0 ∈ ℝ
39 0le1 ⊢ 0 ≤ 1
40 ovolicc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1 ) → ( vol* ‘ ( 0 [,] 1 ) ) = ( 1 − 0 ) )
41 38 23 39 40 mp3an ⊢ ( vol* ‘ ( 0 [,] 1 ) ) = ( 1 − 0 )
42 1m0e1 ⊢ ( 1 − 0 ) = 1
43 41 42 eqtri ⊢ ( vol* ‘ ( 0 [,] 1 ) ) = 1
44 43 23 eqeltri ⊢ ( vol* ‘ ( 0 [,] 1 ) ) ∈ ℝ
45 ovolsscl ⊢ ( ( ran 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℝ ∧ ( vol* ‘ ( 0 [,] 1 ) ) ∈ ℝ ) → ( vol* ‘ ran 𝐹 ) ∈ ℝ )
46 19 44 45 mp3an23 ⊢ ( ran 𝐹 ⊆ ( 0 [,] 1 ) → ( vol* ‘ ran 𝐹 ) ∈ ℝ )
47 18 46 syl ⊢ ( 𝜑 → ( vol* ‘ ran 𝐹 ) ∈ ℝ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ran 𝐹 ) ∈ ℝ )
49 simpr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 0 < ( vol* ‘ ran 𝐹 ) )
50 48 49 elrpd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ran 𝐹 ) ∈ ℝ+ )
51 rpdivcl ⊢ ( ( 3 ∈ ℝ+ ∧ ( vol* ‘ ran 𝐹 ) ∈ ℝ+ ) → ( 3 / ( vol* ‘ ran 𝐹 ) ) ∈ ℝ+ )
52 37 50 51 sylancr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 3 / ( vol* ‘ ran 𝐹 ) ) ∈ ℝ+ )
53 52 rpred ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 3 / ( vol* ‘ ran 𝐹 ) ) ∈ ℝ )
54 52 rpge0d ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 0 ≤ ( 3 / ( vol* ‘ ran 𝐹 ) ) )
55 flge0nn0 ⊢ ( ( ( 3 / ( vol* ‘ ran 𝐹 ) ) ∈ ℝ ∧ 0 ≤ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) → ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) ∈ ℕ0 )
56 53 54 55 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) ∈ ℕ0 )
57 nn0p1nn ⊢ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ∈ ℕ )
58 56 57 syl ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ∈ ℕ )
59 58 nnred ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ∈ ℝ )
60 59 48 remulcld ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ∈ ℝ )
61 60 rexrd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ∈ ℝ* )
62 12 elpw2 ⊢ ( ran 𝐹 ∈ 𝒫 ℝ ↔ ran 𝐹 ⊆ ℝ )
63 20 62 sylibr ⊢ ( 𝜑 → ran 𝐹 ∈ 𝒫 ℝ )
64 63 anim1i ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ∈ dom vol ) → ( ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol ) )
65 eldif ⊢ ( ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) ↔ ( ran 𝐹 ∈ 𝒫 ℝ ∧ ¬ ran 𝐹 ∈ dom vol ) )
66 64 65 sylibr ⊢ ( ( 𝜑 ∧ ¬ ran 𝐹 ∈ dom vol ) → ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) )
67 66 ex ⊢ ( 𝜑 → ( ¬ ran 𝐹 ∈ dom vol → ran 𝐹 ∈ ( 𝒫 ℝ ∖ dom vol ) ) )
68 7 67 mt3d ⊢ ( 𝜑 → ran 𝐹 ∈ dom vol )
69 inss1 ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℚ
70 qssre ⊢ ℚ ⊆ ℝ
71 69 70 sstri ⊢ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℝ
72 fss ⊢ ( ( 𝐺 : ℕ ⟶ ( ℚ ∩ ( - 1 [,] 1 ) ) ∧ ( ℚ ∩ ( - 1 [,] 1 ) ) ⊆ ℝ ) → 𝐺 : ℕ ⟶ ℝ )
73 27 71 72 sylancl ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ℝ )
74 73 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ )
75 shftmbl ⊢ ( ( ran 𝐹 ∈ dom vol ∧ ( 𝐺 ‘ 𝑛 ) ∈ ℝ ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } ∈ dom vol )
76 68 74 75 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → { 𝑠 ∈ ℝ ∣ ( 𝑠 − ( 𝐺 ‘ 𝑛 ) ) ∈ ran 𝐹 } ∈ dom vol )
77 76 6 fmptd ⊢ ( 𝜑 → 𝑇 : ℕ ⟶ dom vol )
78 77 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
79 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
80 iunmbl ⊢ ( ∀ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
81 79 80 syl ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
82 mblss ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ )
83 ovolcl ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ℝ → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* )
84 81 82 83 3syl ⊢ ( 𝜑 → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* )
85 84 adantr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* )
86 flltp1 ⊢ ( ( 3 / ( vol* ‘ ran 𝐹 ) ) ∈ ℝ → ( 3 / ( vol* ‘ ran 𝐹 ) ) < ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) )
87 53 86 syl ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 3 / ( vol* ‘ ran 𝐹 ) ) < ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) )
88 34 a1i ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 3 ∈ ℝ )
89 88 59 50 ltdivmul2d ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( 3 / ( vol* ‘ ran 𝐹 ) ) < ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ↔ 3 < ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ) )
90 87 89 mpbid ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 3 < ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) )
91 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
92 1zzd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 1 ∈ ℤ )
93 mblvol ⊢ ( ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) )
94 78 93 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) )
95 94 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ran 𝐹 ) )
96 47 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ran 𝐹 ) ∈ ℝ )
97 95 96 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ )
98 97 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ )
99 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) )
100 98 99 fmptd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) : ℕ ⟶ ℝ )
101 100 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ‘ 𝑘 ) ∈ ℝ )
102 91 92 101 serfre ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) : ℕ ⟶ ℝ )
103 102 frnd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ⊆ ℝ )
104 ressxr ⊢ ℝ ⊆ ℝ*
105 103 104 sstrdi ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ⊆ ℝ* )
106 95 adantlr ⊢ ( ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) ∧ 𝑚 ∈ ℕ ) → ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ran 𝐹 ) )
107 106 mpteq2dva ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ran 𝐹 ) ) )
108 fconstmpt ⊢ ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ran 𝐹 ) )
109 107 108 eqtr4di ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) = ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) )
110 109 seqeq3d ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) ) )
111 110 fveq1d ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) = ( seq 1 ( + , ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) )
112 48 recnd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ran 𝐹 ) ∈ ℂ )
113 ser1const ⊢ ( ( ( vol* ‘ ran 𝐹 ) ∈ ℂ ∧ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) = ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) )
114 112 58 113 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( seq 1 ( + , ( ℕ × { ( vol* ‘ ran 𝐹 ) } ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) = ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) )
115 111 114 eqtrd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) = ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) )
116 102 ffnd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) Fn ℕ )
117 fnfvelrn ⊢ ( ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) Fn ℕ ∧ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ∈ ℕ ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) ∈ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) )
118 116 58 117 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ‘ ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) ) ∈ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) )
119 115 118 eqeltrrd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ∈ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) )
120 supxrub ⊢ ( ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ⊆ ℝ* ∧ ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ∈ ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
121 105 119 120 syl2anc ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
122 81 adantr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol )
123 mblvol ⊢ ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ∈ dom vol → ( vol ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
124 122 123 syl ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
125 78 97 jca ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑇 ‘ 𝑚 ) ∈ dom vol ∧ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ ) )
126 125 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( ( 𝑇 ‘ 𝑚 ) ∈ dom vol ∧ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ ) )
127 1 2 3 4 5 6 7 vitalilem3 ⊢ ( 𝜑 → Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
128 127 adantr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) )
129 eqid ⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) )
130 129 99 voliun ⊢ ( ( ∀ 𝑚 ∈ ℕ ( ( 𝑇 ‘ 𝑚 ) ∈ dom vol ∧ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ ) ∧ Disj 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) → ( vol ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
131 126 128 130 syl2an2r ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
132 124 131 eqtr3d ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) = sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol ‘ ( 𝑇 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
133 121 132 breqtrrd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( ( ⌊ ‘ ( 3 / ( vol* ‘ ran 𝐹 ) ) ) + 1 ) · ( vol* ‘ ran 𝐹 ) ) ≤ ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
134 36 61 85 90 133 xrltletrd ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → 3 < ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
135 17 simp3d ⊢ ( 𝜑 → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) )
136 135 adantr ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) )
137 2re ⊢ 2 ∈ ℝ
138 iccssre ⊢ ( ( - 1 ∈ ℝ ∧ 2 ∈ ℝ ) → ( - 1 [,] 2 ) ⊆ ℝ )
139 22 137 138 mp2an ⊢ ( - 1 [,] 2 ) ⊆ ℝ
140 ovolss ⊢ ( ( ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ⊆ ( - 1 [,] 2 ) ∧ ( - 1 [,] 2 ) ⊆ ℝ ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ ( vol* ‘ ( - 1 [,] 2 ) ) )
141 136 139 140 sylancl ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ ( vol* ‘ ( - 1 [,] 2 ) ) )
142 2cn ⊢ 2 ∈ ℂ
143 ax-1cn ⊢ 1 ∈ ℂ
144 142 143 subnegi ⊢ ( 2 − - 1 ) = ( 2 + 1 )
145 neg1lt0 ⊢ - 1 < 0
146 2pos ⊢ 0 < 2
147 22 38 137 lttri ⊢ ( ( - 1 < 0 ∧ 0 < 2 ) → - 1 < 2 )
148 145 146 147 mp2an ⊢ - 1 < 2
149 22 137 148 ltleii ⊢ - 1 ≤ 2
150 ovolicc ⊢ ( ( - 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ - 1 ≤ 2 ) → ( vol* ‘ ( - 1 [,] 2 ) ) = ( 2 − - 1 ) )
151 22 137 149 150 mp3an ⊢ ( vol* ‘ ( - 1 [,] 2 ) ) = ( 2 − - 1 )
152 df-3 ⊢ 3 = ( 2 + 1 )
153 144 151 152 3eqtr4i ⊢ ( vol* ‘ ( - 1 [,] 2 ) ) = 3
154 141 153 breqtrdi ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 3 )
155 xrlenlt ⊢ ( ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ∈ ℝ* ∧ 3 ∈ ℝ* ) → ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 3 ↔ ¬ 3 < ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ) )
156 85 35 155 sylancl ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ( ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ≤ 3 ↔ ¬ 3 < ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) ) )
157 154 156 mpbid ⊢ ( ( 𝜑 ∧ 0 < ( vol* ‘ ran 𝐹 ) ) → ¬ 3 < ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑇 ‘ 𝑚 ) ) )
158 134 157 pm2.65da ⊢ ( 𝜑 → ¬ 0 < ( vol* ‘ ran 𝐹 ) )
159 ovolge0 ⊢ ( ran 𝐹 ⊆ ℝ → 0 ≤ ( vol* ‘ ran 𝐹 ) )
160 20 159 syl ⊢ ( 𝜑 → 0 ≤ ( vol* ‘ ran 𝐹 ) )
161 0xr ⊢ 0 ∈ ℝ*
162 ovolcl ⊢ ( ran 𝐹 ⊆ ℝ → ( vol* ‘ ran 𝐹 ) ∈ ℝ* )
163 20 162 syl ⊢ ( 𝜑 → ( vol* ‘ ran 𝐹 ) ∈ ℝ* )
164 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ ( vol* ‘ ran 𝐹 ) ∈ ℝ* ) → ( 0 ≤ ( vol* ‘ ran 𝐹 ) ↔ ( 0 < ( vol* ‘ ran 𝐹 ) ∨ 0 = ( vol* ‘ ran 𝐹 ) ) ) )
165 161 163 164 sylancr ⊢ ( 𝜑 → ( 0 ≤ ( vol* ‘ ran 𝐹 ) ↔ ( 0 < ( vol* ‘ ran 𝐹 ) ∨ 0 = ( vol* ‘ ran 𝐹 ) ) ) )
166 160 165 mpbid ⊢ ( 𝜑 → ( 0 < ( vol* ‘ ran 𝐹 ) ∨ 0 = ( vol* ‘ ran 𝐹 ) ) )
167 166 ord ⊢ ( 𝜑 → ( ¬ 0 < ( vol* ‘ ran 𝐹 ) → 0 = ( vol* ‘ ran 𝐹 ) ) )
168 158 167 mpd ⊢ ( 𝜑 → 0 = ( vol* ‘ ran 𝐹 ) )
169 168 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 0 = ( vol* ‘ ran 𝐹 ) )
170 33 169 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑇 ‘ 𝑚 ) ) = 0 )