Step | Hyp | Ref
| Expression |
1 | | vonioolem2.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | 1 | vonmea 39464 |
. . . 4
⊢ (𝜑 → (voln‘𝑋) ∈ Meas) |
3 | | 1zzd 11285 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
4 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
5 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
6 | | eqid 2610 |
. . . . . 6
⊢ dom
(voln‘𝑋) = dom
(voln‘𝑋) |
7 | | vonioolem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ) |
9 | 8 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
10 | | nnrecre 10934 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
11 | 10 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
12 | 9, 11 | readdcld 9948 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
13 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) |
14 | 12, 13 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ) |
15 | | vonioolem2.c |
. . . . . . . . . 10
⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))))) |
17 | 1 | mptexd 6391 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
19 | 16, 18 | fvmpt2d 6202 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
20 | 19 | feq1d 5943 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐶‘𝑛):𝑋⟶ℝ ↔ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ)) |
21 | 14, 20 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
22 | | vonioolem2.b |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵:𝑋⟶ℝ) |
24 | 5, 6, 21, 23 | hoimbl 39521 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom (voln‘𝑋)) |
25 | | vonioolem2.d |
. . . . 5
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
26 | 24, 25 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐷:ℕ⟶dom (voln‘𝑋)) |
27 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
28 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (1 / 𝑛) = (1 / 𝑚)) |
29 | 28 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘) + (1 / 𝑛)) = ((𝐴‘𝑘) + (1 / 𝑚))) |
30 | 29 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚)))) |
31 | 30 | cbvmptv 4678 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚)))) |
32 | 15, 31 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚)))) |
33 | 32 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚))))) |
34 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1))) |
35 | 34 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → ((𝐴‘𝑘) + (1 / 𝑚)) = ((𝐴‘𝑘) + (1 / (𝑛 + 1)))) |
36 | 35 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / (𝑛 + 1))))) |
37 | 36 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 = (𝑛 + 1)) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / (𝑛 + 1))))) |
38 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
39 | 38 | peano2nnd 10914 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
40 | 5 | mptexd 6391 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / (𝑛 + 1)))) ∈ V) |
41 | 33, 37, 39, 40 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘(𝑛 + 1)) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / (𝑛 + 1))))) |
42 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐴‘𝑘) + (1 / (𝑛 + 1))) ∈ V |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / (𝑛 + 1))) ∈ V) |
44 | 41, 43 | fvmpt2d 6202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) = ((𝐴‘𝑘) + (1 / (𝑛 + 1)))) |
45 | | 1red 9934 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
46 | | nnre 10904 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
47 | 46, 45 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℝ) |
48 | | peano2nn 10909 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
49 | | nnne0 10930 |
. . . . . . . . . . . . 13
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ≠
0) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0) |
51 | 45, 47, 50 | redivcld 10732 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) ∈
ℝ) |
52 | 51 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / (𝑛 + 1)) ∈ ℝ) |
53 | 9, 52 | readdcld 9948 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / (𝑛 + 1))) ∈ ℝ) |
54 | 44, 53 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) ∈ ℝ) |
55 | 54 | rexrd 9968 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) ∈
ℝ*) |
56 | | ressxr 9962 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
57 | 22 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
58 | 56, 57 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
59 | 58 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) |
60 | 46 | ltp1d 10833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 < (𝑛 + 1)) |
61 | | nnrp 11718 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
62 | 48 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℝ+) |
63 | 61, 62 | ltrecd 11766 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 < (𝑛 + 1) ↔ (1 / (𝑛 + 1)) < (1 / 𝑛))) |
64 | 60, 63 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) < (1 / 𝑛)) |
65 | 51, 10, 64 | ltled 10064 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) ≤ (1 / 𝑛)) |
66 | 65 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / (𝑛 + 1)) ≤ (1 / 𝑛)) |
67 | 52, 11, 9, 66 | leadd2dd 10521 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / (𝑛 + 1))) ≤ ((𝐴‘𝑘) + (1 / 𝑛))) |
68 | 12 | elexd 3187 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ V) |
69 | 19, 68 | fvmpt2d 6202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐴‘𝑘) + (1 / 𝑛))) |
70 | 44, 69 | breq12d 4596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘) ↔ ((𝐴‘𝑘) + (1 / (𝑛 + 1))) ≤ ((𝐴‘𝑘) + (1 / 𝑛)))) |
71 | 67, 70 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘)) |
72 | 57 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
73 | | eqidd 2611 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) = (𝐵‘𝑘)) |
74 | 72, 73 | eqled 10019 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ≤ (𝐵‘𝑘)) |
75 | | icossico 12114 |
. . . . . . 7
⊢
(((((𝐶‘(𝑛 + 1))‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) ∧ (((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘) ∧ (𝐵‘𝑘) ≤ (𝐵‘𝑘))) → (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ⊆ (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
76 | 55, 59, 71, 74, 75 | syl22anc 1319 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ⊆ (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
77 | 27, 76 | ixpssixp 38297 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
78 | 25 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
79 | 24 | elexd 3187 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ V) |
80 | 78, 79 | fvmpt2d 6202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
81 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐶‘𝑛) = (𝐶‘𝑚)) |
82 | 81 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘)) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘))) |
84 | 83 | ixpeq2dv 7810 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘))) |
85 | 84 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘))) |
86 | 25, 85 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐷 = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘))) |
87 | 86 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘)))) |
88 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝐶‘𝑚) = (𝐶‘(𝑛 + 1))) |
89 | 88 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((𝐶‘𝑚)‘𝑘) = ((𝐶‘(𝑛 + 1))‘𝑘)) |
90 | 89 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) = (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
91 | 90 | ixpeq2dv 7810 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → X𝑘 ∈ 𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
92 | 91 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 = (𝑛 + 1)) → X𝑘 ∈ 𝑋 (((𝐶‘𝑚)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
93 | | ovex 6577 |
. . . . . . . . . 10
⊢ (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V |
94 | 93 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑘 ∈
𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V |
95 | | ixpexg 7818 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V → X𝑘 ∈
𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V) |
96 | 94, 95 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑘 ∈
𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V |
97 | 96 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)) ∈ V) |
98 | 87, 92, 39, 97 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘(𝑛 + 1)) = X𝑘 ∈ 𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘))) |
99 | 80, 98 | sseq12d 3597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘𝑛) ⊆ (𝐷‘(𝑛 + 1)) ↔ X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 (((𝐶‘(𝑛 + 1))‘𝑘)[,)(𝐵‘𝑘)))) |
100 | 77, 99 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ⊆ (𝐷‘(𝑛 + 1))) |
101 | 1, 6, 7, 22 | hoimbl 39521 |
. . . . 5
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ∈ dom (voln‘𝑋)) |
102 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
103 | 7 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
104 | 102, 1, 103, 57 | vonhoire 39563 |
. . . . 5
⊢ (𝜑 → ((voln‘𝑋)‘X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ) |
105 | | vonioolem2.i |
. . . . . . 7
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) |
106 | 105 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
107 | | nftru 1721 |
. . . . . . . . 9
⊢
Ⅎ𝑘⊤ |
108 | | ioossico 12133 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ 𝑋) → ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
110 | 107, 109 | ixpssixp 38297 |
. . . . . . . 8
⊢ (⊤
→ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
111 | 110 | trud 1484 |
. . . . . . 7
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) |
112 | 111 | a1i 11 |
. . . . . 6
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
113 | 106, 112 | eqsstrd 3602 |
. . . . 5
⊢ (𝜑 → 𝐼 ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) |
114 | 56 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℝ*) |
115 | 7, 114 | fssd 5970 |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑋⟶ℝ*) |
116 | 22, 114 | fssd 5970 |
. . . . . . 7
⊢ (𝜑 → 𝐵:𝑋⟶ℝ*) |
117 | 1, 6, 115, 116 | ioovonmbl 39568 |
. . . . . 6
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)) ∈ dom (voln‘𝑋)) |
118 | 105, 117 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ dom (voln‘𝑋)) |
119 | 2, 101, 104, 113, 118 | meassre 39370 |
. . . 4
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) ∈ ℝ) |
120 | 2 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (voln‘𝑋) ∈ Meas) |
121 | 80, 24 | eqeltrd 2688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ∈ dom (voln‘𝑋)) |
122 | 118 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐼 ∈ dom (voln‘𝑋)) |
123 | 56, 103 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
124 | 123 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
125 | 61 | rpreccld 11758 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
126 | 125 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈
ℝ+) |
127 | 9, 126 | ltaddrpd 11781 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < ((𝐴‘𝑘) + (1 / 𝑛))) |
128 | | icossioo 12135 |
. . . . . . . 8
⊢ ((((𝐴‘𝑘) ∈ ℝ* ∧ (𝐵‘𝑘) ∈ ℝ*) ∧ ((𝐴‘𝑘) < ((𝐴‘𝑘) + (1 / 𝑛)) ∧ (𝐵‘𝑘) ≤ (𝐵‘𝑘))) → (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
129 | 124, 59, 127, 74, 128 | syl22anc 1319 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘)) ⊆ ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
130 | 27, 129 | ixpssixp 38297 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
131 | 69 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘))) |
132 | 131 | ixpeq2dva 7809 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘))) |
133 | 80, 132 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘))) |
134 | 105 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
135 | 133, 134 | sseq12d 3597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘𝑛) ⊆ 𝐼 ↔ X𝑘 ∈ 𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘)))) |
136 | 130, 135 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) ⊆ 𝐼) |
137 | 120, 6, 121, 122, 136 | meassle 39356 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷‘𝑛)) ≤ ((voln‘𝑋)‘𝐼)) |
138 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
139 | 2, 3, 4, 26, 100, 119, 137, 138 | meaiuninc2 39375 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘∪
𝑛 ∈ ℕ (𝐷‘𝑛))) |
140 | 102, 1, 103, 58 | iunhoiioo 39567 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)(,)(𝐵‘𝑘))) |
141 | 133 | iuneq2dv 4478 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐷‘𝑛) = ∪ 𝑛 ∈ ℕ X𝑘 ∈
𝑋 (((𝐴‘𝑘) + (1 / 𝑛))[,)(𝐵‘𝑘))) |
142 | 140, 141,
106 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐷‘𝑛) = 𝐼) |
143 | 142 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → 𝐼 = ∪ 𝑛 ∈ ℕ (𝐷‘𝑛)) |
144 | 143 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∪
𝑛 ∈ ℕ (𝐷‘𝑛))) |
145 | 144 | eqcomd 2616 |
. . 3
⊢ (𝜑 → ((voln‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐷‘𝑛)) = ((voln‘𝑋)‘𝐼)) |
146 | 139, 145 | breqtrd 4609 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘𝐼)) |
147 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐷‘𝑛) = (𝐷‘𝑚)) |
148 | 147 | fveq2d 6107 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((voln‘𝑋)‘(𝐷‘𝑛)) = ((voln‘𝑋)‘(𝐷‘𝑚))) |
149 | 148 | cbvmptv 4678 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚))) |
150 | 149 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚)))) |
151 | | vonioolem2.n |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
152 | | vonioolem2.t |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
153 | 149 | eqcomi 2619 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑚))) = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
154 | | eqcom 2617 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 ↔ 𝑚 = 𝑛) |
155 | 154 | imbi1i 338 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑚 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘)) ↔ (𝑚 = 𝑛 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘))) |
156 | | eqcom 2617 |
. . . . . . . . . 10
⊢ (((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘) ↔ ((𝐶‘𝑚)‘𝑘) = ((𝐶‘𝑛)‘𝑘)) |
157 | 156 | imbi2i 325 |
. . . . . . . . 9
⊢ ((𝑚 = 𝑛 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘)) ↔ (𝑚 = 𝑛 → ((𝐶‘𝑚)‘𝑘) = ((𝐶‘𝑛)‘𝑘))) |
158 | 155, 157 | bitri 263 |
. . . . . . . 8
⊢ ((𝑛 = 𝑚 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘)) ↔ (𝑚 = 𝑛 → ((𝐶‘𝑚)‘𝑘) = ((𝐶‘𝑛)‘𝑘))) |
159 | 82, 158 | mpbi 219 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚)‘𝑘) = ((𝐶‘𝑛)‘𝑘)) |
160 | 159 | oveq2d 6565 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐵‘𝑘) − ((𝐶‘𝑚)‘𝑘)) = ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
161 | 160 | prodeq2ad 38659 |
. . . . 5
⊢ (𝑚 = 𝑛 → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑚)‘𝑘)) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
162 | 161 | cbvmptv 4678 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑚)‘𝑘))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
163 | | eqid 2610 |
. . . 4
⊢ inf(ran
(𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) |
164 | | eqid 2610 |
. . . 4
⊢
((⌊‘(1 / inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ))) + 1) =
((⌊‘(1 / inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ))) + 1) |
165 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝐵‘𝑗) = (𝐵‘𝑘)) |
166 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝐴‘𝑗) = (𝐴‘𝑘)) |
167 | 165, 166 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝐵‘𝑗) − (𝐴‘𝑗)) = ((𝐵‘𝑘) − (𝐴‘𝑘))) |
168 | 167 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
169 | 168 | rneqi 5273 |
. . . . . . . . 9
⊢ ran
(𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))) = ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
170 | 169 | infeq1i 8267 |
. . . . . . . 8
⊢ inf(ran
(𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))), ℝ, < ) = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) |
171 | 170 | oveq2i 6560 |
. . . . . . 7
⊢ (1 /
inf(ran (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))), ℝ, < )) = (1 / inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < )) |
172 | 171 | fveq2i 6106 |
. . . . . 6
⊢
(⌊‘(1 / inf(ran (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))), ℝ, < ))) = (⌊‘(1 /
inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ))) |
173 | 172 | oveq1i 6559 |
. . . . 5
⊢
((⌊‘(1 / inf(ran (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))), ℝ, < ))) + 1) =
((⌊‘(1 / inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ))) + 1) |
174 | 173 | fveq2i 6106 |
. . . 4
⊢
(ℤ≥‘((⌊‘(1 / inf(ran (𝑗 ∈ 𝑋 ↦ ((𝐵‘𝑗) − (𝐴‘𝑗))), ℝ, < ))) + 1)) =
(ℤ≥‘((⌊‘(1 / inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ))) + 1)) |
175 | 1, 7, 22, 151, 152, 15, 25, 153, 162, 163, 164, 174 | vonioolem1 39571 |
. . 3
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
176 | 150, 175 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
177 | | climuni 14131 |
. 2
⊢ (((𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘𝐼) ∧ (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
178 | 146, 176,
177 | syl2anc 691 |
1
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |