Step | Hyp | Ref
| Expression |
1 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑛𝜑 |
2 | | vonicclem2.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
3 | 2 | vonmea 39464 |
. . . 4
⊢ (𝜑 → (voln‘𝑋) ∈ Meas) |
4 | | 1zzd 11285 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
5 | | nnuz 11599 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
6 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
7 | | eqid 2610 |
. . . . . 6
⊢ dom
(voln‘𝑋) = dom
(voln‘𝑋) |
8 | | vonicclem2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ) |
10 | | vonicclem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
11 | 10 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
12 | 11 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
13 | | nnrecre 10934 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
14 | 13 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
15 | 12, 14 | readdcld 9948 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
16 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) |
17 | 15, 16 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ) |
18 | | vonicclem2.c |
. . . . . . . . . 10
⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))) |
20 | 2 | mptexd 6391 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) ∈ V) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) ∈ V) |
22 | 19, 21 | fvmpt2d 6202 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) |
23 | 22 | feq1d 5943 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐶‘𝑛):𝑋⟶ℝ ↔ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ)) |
24 | 17, 23 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
25 | 6, 7, 9, 24 | hoimbl 39521 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) ∈ dom (voln‘𝑋)) |
26 | | vonicclem2.d |
. . . . 5
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
27 | 25, 26 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐷:ℕ⟶dom (voln‘𝑋)) |
28 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑛 ∈ ℕ) |
29 | | ressxr 9962 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
30 | 8 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
31 | 29, 30 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
32 | 31 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈
ℝ*) |
33 | 15 | elexd 3187 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / 𝑛)) ∈ V) |
34 | 22, 33 | fvmpt2d 6202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐵‘𝑘) + (1 / 𝑛))) |
35 | 34, 15 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈ ℝ) |
36 | 35 | rexrd 9968 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈
ℝ*) |
37 | 9 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
38 | 37 | leidd 10473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐴‘𝑘)) |
39 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
40 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
41 | 40, 39 | readdcld 9948 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℝ) |
42 | | peano2nn 10909 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
43 | | nnne0 10930 |
. . . . . . . . . . . 12
⊢ ((𝑛 + 1) ∈ ℕ →
(𝑛 + 1) ≠
0) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ≠ 0) |
45 | 39, 41, 44 | redivcld 10732 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) ∈
ℝ) |
46 | 45 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / (𝑛 + 1)) ∈ ℝ) |
47 | 40 | ltp1d 10833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 < (𝑛 + 1)) |
48 | | nnrp 11718 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
49 | 42 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℝ+) |
50 | 48, 49 | ltrecd 11766 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (𝑛 < (𝑛 + 1) ↔ (1 / (𝑛 + 1)) < (1 / 𝑛))) |
51 | 47, 50 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) < (1 / 𝑛)) |
52 | 45, 13, 51 | ltled 10064 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
(𝑛 + 1)) ≤ (1 / 𝑛)) |
53 | 52 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / (𝑛 + 1)) ≤ (1 / 𝑛)) |
54 | 46, 14, 12, 53 | leadd2dd 10521 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / (𝑛 + 1))) ≤ ((𝐵‘𝑘) + (1 / 𝑛))) |
55 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (1 / 𝑛) = (1 / 𝑚)) |
56 | 55 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑚 → ((𝐵‘𝑘) + (1 / 𝑛)) = ((𝐵‘𝑘) + (1 / 𝑚))) |
57 | 56 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑚 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) |
58 | 57 | cbvmptv 4678 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) |
59 | 18, 58 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ 𝐶 = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚)))) |
60 | 59 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 = (𝑚 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))))) |
61 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1))) |
62 | 61 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → ((𝐵‘𝑘) + (1 / 𝑚)) = ((𝐵‘𝑘) + (1 / (𝑛 + 1)))) |
63 | 62 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / (𝑛 + 1))))) |
64 | 63 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 = (𝑛 + 1)) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑚))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / (𝑛 + 1))))) |
65 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
66 | 65 | peano2nnd 10914 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
67 | 6 | mptexd 6391 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / (𝑛 + 1)))) ∈ V) |
68 | 60, 64, 66, 67 | fvmptd 6197 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘(𝑛 + 1)) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / (𝑛 + 1))))) |
69 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐵‘𝑘) + (1 / (𝑛 + 1))) ∈ V |
70 | 69 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / (𝑛 + 1))) ∈ V) |
71 | 68, 70 | fvmpt2d 6202 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) = ((𝐵‘𝑘) + (1 / (𝑛 + 1)))) |
72 | 71, 34 | breq12d 4596 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘) ↔ ((𝐵‘𝑘) + (1 / (𝑛 + 1))) ≤ ((𝐵‘𝑘) + (1 / 𝑛)))) |
73 | 54, 72 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘)) |
74 | | icossico 12114 |
. . . . . . 7
⊢ ((((𝐴‘𝑘) ∈ ℝ* ∧ ((𝐶‘𝑛)‘𝑘) ∈ ℝ*) ∧ ((𝐴‘𝑘) ≤ (𝐴‘𝑘) ∧ ((𝐶‘(𝑛 + 1))‘𝑘) ≤ ((𝐶‘𝑛)‘𝑘))) → ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ⊆ ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
75 | 32, 36, 38, 73, 74 | syl22anc 1319 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ⊆ ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
76 | 28, 75 | ixpssixp 38297 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
77 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐶‘𝑛) = (𝐶‘𝑚)) |
78 | 77 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘𝑚)‘𝑘)) |
79 | 78 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘))) |
80 | 79 | ixpeq2dv 7810 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘))) |
81 | 80 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘))) |
82 | 26, 81 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐷 = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘))) |
83 | 82 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 = (𝑚 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘)))) |
84 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → (𝐶‘𝑚) = (𝐶‘(𝑛 + 1))) |
85 | 84 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 + 1) → ((𝐶‘𝑚)‘𝑘) = ((𝐶‘(𝑛 + 1))‘𝑘)) |
86 | 85 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 + 1) → ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘)) = ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘))) |
87 | 86 | ixpeq2dv 7810 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 + 1) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘))) |
88 | 87 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 = (𝑛 + 1)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑚)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘))) |
89 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V |
90 | 89 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V |
91 | | ixpexg 7818 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V |
93 | 92 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ∈ V) |
94 | 83, 88, 66, 93 | fvmptd 6197 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘(𝑛 + 1)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘))) |
95 | 26 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)))) |
96 | 25 | elexd 3187 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) ∈ V) |
97 | 95, 96 | fvmpt2d 6202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
98 | 94, 97 | sseq12d 3597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘(𝑛 + 1)) ⊆ (𝐷‘𝑛) ↔ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘(𝑛 + 1))‘𝑘)) ⊆ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)))) |
99 | 76, 98 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘(𝑛 + 1)) ⊆ (𝐷‘𝑛)) |
100 | | 1nn 10908 |
. . . . . 6
⊢ 1 ∈
ℕ |
101 | 100, 5 | eleqtri 2686 |
. . . . 5
⊢ 1 ∈
(ℤ≥‘1) |
102 | 101 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
(ℤ≥‘1)) |
103 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝐶‘𝑛) = (𝐶‘1)) |
104 | 103 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → ((𝐶‘𝑛)‘𝑘) = ((𝐶‘1)‘𝑘)) |
105 | 104 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑛 = 1 → ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘))) |
106 | 105 | ixpeq2dv 7810 |
. . . . . . . 8
⊢ (𝑛 = 1 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘))) |
107 | 106 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 = 1) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘))) |
108 | 100 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℕ) |
109 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V |
110 | 109 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V |
111 | | ixpexg 7818 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V) |
112 | 110, 111 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V |
113 | 112 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)) ∈ V) |
114 | 95, 107, 108, 113 | fvmptd 6197 |
. . . . . 6
⊢ (𝜑 → (𝐷‘1) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘))) |
115 | 114 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → ((voln‘𝑋)‘(𝐷‘1)) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘)))) |
116 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘𝜑 |
117 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝜑) |
118 | 100 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 1 ∈ ℕ) |
119 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) |
120 | 100 | elexi 3186 |
. . . . . . . 8
⊢ 1 ∈
V |
121 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (𝑛 ∈ ℕ ↔ 1 ∈
ℕ)) |
122 | 121 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → ((𝜑 ∧ 𝑛 ∈ ℕ) ↔ (𝜑 ∧ 1 ∈ ℕ))) |
123 | 122 | anbi1d 737 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) ↔ ((𝜑 ∧ 1 ∈ ℕ) ∧ 𝑘 ∈ 𝑋))) |
124 | 104 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (((𝐶‘𝑛)‘𝑘) ∈ ℝ ↔ ((𝐶‘1)‘𝑘) ∈ ℝ)) |
125 | 123, 124 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑛 = 1 → ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈ ℝ) ↔ (((𝜑 ∧ 1 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘1)‘𝑘) ∈ ℝ))) |
126 | 120, 125,
35 | vtocl 3232 |
. . . . . . 7
⊢ (((𝜑 ∧ 1 ∈ ℕ) ∧
𝑘 ∈ 𝑋) → ((𝐶‘1)‘𝑘) ∈ ℝ) |
127 | 117, 118,
119, 126 | syl21anc 1317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐶‘1)‘𝑘) ∈ ℝ) |
128 | 116, 2, 30, 127 | vonhoire 39563 |
. . . . 5
⊢ (𝜑 → ((voln‘𝑋)‘X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘1)‘𝑘))) ∈ ℝ) |
129 | 115, 128 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → ((voln‘𝑋)‘(𝐷‘1)) ∈ ℝ) |
130 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
131 | 1, 3, 4, 5, 27, 99, 102, 129, 130 | meaiininc 39377 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘∩
𝑛 ∈ ℕ (𝐷‘𝑛))) |
132 | 116, 30, 11 | iinhoiicc 39565 |
. . . . . . 7
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐵‘𝑘) + (1 / 𝑛))) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))) |
133 | 34 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = ((𝐴‘𝑘)[,)((𝐵‘𝑘) + (1 / 𝑛)))) |
134 | 133 | ixpeq2dva 7809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐵‘𝑘) + (1 / 𝑛)))) |
135 | 97, 134 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐵‘𝑘) + (1 / 𝑛)))) |
136 | 135 | iineq2dv 4479 |
. . . . . . 7
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐷‘𝑛) = ∩ 𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐵‘𝑘) + (1 / 𝑛)))) |
137 | | vonicclem2.i |
. . . . . . . 8
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘)) |
138 | 137 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,](𝐵‘𝑘))) |
139 | 132, 136,
138 | 3eqtr4d 2654 |
. . . . . 6
⊢ (𝜑 → ∩ 𝑛 ∈ ℕ (𝐷‘𝑛) = 𝐼) |
140 | 139 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → 𝐼 = ∩ 𝑛 ∈ ℕ (𝐷‘𝑛)) |
141 | 140 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ((voln‘𝑋)‘∩
𝑛 ∈ ℕ (𝐷‘𝑛))) |
142 | 141 | eqcomd 2616 |
. . 3
⊢ (𝜑 → ((voln‘𝑋)‘∩ 𝑛 ∈ ℕ (𝐷‘𝑛)) = ((voln‘𝑋)‘𝐼)) |
143 | 131, 142 | breqtrd 4609 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘𝐼)) |
144 | | fveq2 6103 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐷‘𝑛) = (𝐷‘𝑚)) |
145 | 144 | fveq2d 6107 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((voln‘𝑋)‘(𝐷‘𝑛)) = ((voln‘𝑋)‘(𝐷‘𝑚))) |
146 | 145 | cbvmptv 4678 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚))) |
147 | 146 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚)))) |
148 | | vonicclem2.n |
. . . 4
⊢ (𝜑 → 𝑋 ≠ ∅) |
149 | | vonicclem2.t |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) |
150 | 146 | eqcomi 2619 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑚))) = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
151 | 2, 8, 10, 148, 149, 18, 26, 150 | vonicclem1 39574 |
. . 3
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑚))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
152 | 147, 151 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
153 | | climuni 14131 |
. 2
⊢ (((𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ((voln‘𝑋)‘𝐼) ∧ (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
154 | 143, 152,
153 | syl2anc 691 |
1
⊢ (𝜑 → ((voln‘𝑋)‘𝐼) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |