Proof of Theorem vonicclem1
Step | Hyp | Ref
| Expression |
1 | | vonicclem1.s |
. . . 4
⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛)))) |
3 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
4 | | vonicclem1.d |
. . . . . . . . . 10
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)))) |
6 | | vonicclem1.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ Fin) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
8 | | eqid 2610 |
. . . . . . . . . . 11
⊢ dom
(voln‘𝑋) = dom
(voln‘𝑋) |
9 | | vonicclem1.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
10 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ) |
11 | | vonicclem1.b |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
12 | 11 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
13 | 12 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
14 | | nnrecre 10934 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
15 | 14 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
16 | 13, 15 | readdcld 9948 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
17 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) |
18 | 16, 17 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ) |
19 | | vonicclem1.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))))) |
21 | 6 | mptexd 6391 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) ∈ V) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))) ∈ V) |
23 | 20, 22 | fvmpt2d 6202 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛)))) |
24 | 23 | feq1d 5943 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐶‘𝑛):𝑋⟶ℝ ↔ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ)) |
25 | 18, 24 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
26 | 7, 8, 10, 25 | hoimbl 39521 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) ∈ dom (voln‘𝑋)) |
27 | 26 | elexd 3187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) ∈ V) |
28 | 5, 27 | fvmpt2d 6202 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
29 | 3, 28 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) |
30 | 29 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)))) |
31 | | vonicclem1.u |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ≠ ∅) |
32 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ≠ ∅) |
33 | 3, 25 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
34 | | eqid 2610 |
. . . . . . 7
⊢ X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)) |
35 | 7, 32, 10, 33, 34 | vonn0hoi 39561 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln‘𝑋)‘X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘)))) |
36 | 10 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
37 | 3, 36 | syldanl 731 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
38 | 33 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈ ℝ) |
39 | | volico 38876 |
. . . . . . . . 9
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ ((𝐶‘𝑛)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = if((𝐴‘𝑘) < ((𝐶‘𝑛)‘𝑘), (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)), 0)) |
40 | 37, 38, 39 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = if((𝐴‘𝑘) < ((𝐶‘𝑛)‘𝑘), (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)), 0)) |
41 | 3, 13 | syldanl 731 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
42 | | vonicclem1.t |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) |
43 | 42 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ≤ (𝐵‘𝑘)) |
44 | | nnrp 11718 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
45 | 44 | rpreccld 11758 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ+) |
46 | 45 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈
ℝ+) |
47 | 41, 46 | ltaddrpd 11781 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) < ((𝐵‘𝑘) + (1 / 𝑛))) |
48 | 16 | elexd 3187 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) + (1 / 𝑛)) ∈ V) |
49 | 23, 48 | fvmpt2d 6202 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐵‘𝑘) + (1 / 𝑛))) |
50 | 3, 49 | syldanl 731 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐵‘𝑘) + (1 / 𝑛))) |
51 | 47, 50 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) < ((𝐶‘𝑛)‘𝑘)) |
52 | 37, 41, 38, 43, 51 | lelttrd 10074 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < ((𝐶‘𝑛)‘𝑘)) |
53 | 52 | iftrued 4044 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → if((𝐴‘𝑘) < ((𝐶‘𝑛)‘𝑘), (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)), 0) = (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘))) |
54 | 40, 53 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘))) |
55 | 54 | prodeq2dv 14492 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)((𝐶‘𝑛)‘𝑘))) = ∏𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘))) |
56 | 30, 35, 55 | 3eqtrd 2648 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ∏𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘))) |
57 | 49 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)) = (((𝐵‘𝑘) + (1 / 𝑛)) − (𝐴‘𝑘))) |
58 | 13 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℂ) |
59 | 15 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℂ) |
60 | 36 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℂ) |
61 | 58, 59, 60 | addsubd 10292 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐵‘𝑘) + (1 / 𝑛)) − (𝐴‘𝑘)) = (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) |
62 | 57, 61 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)) = (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) |
63 | 62 | prodeq2dv 14492 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∏𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘) − (𝐴‘𝑘)) = ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) |
64 | 56, 63 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) |
65 | 64 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛)))) |
66 | 2, 65 | eqtrd 2644 |
. 2
⊢ (𝜑 → 𝑆 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛)))) |
67 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑘𝜑 |
68 | 9 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
69 | 12, 68 | resubcld 10337 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℝ) |
70 | 69 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℂ) |
71 | | eqid 2610 |
. . 3
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) |
72 | 67, 6, 70, 71 | fprodaddrecnncnv 38797 |
. 2
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) + (1 / 𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
73 | 66, 72 | eqbrtrd 4605 |
1
⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |