Proof of Theorem vonioolem1
| Step | Hyp | Ref
| Expression |
| 1 | | vonioolem1.r |
. . . . 5
⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)))) |
| 3 | | vonioolem1.c |
. . . . . . . . . . 11
⊢ 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 4 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = (𝑛 ∈ ℕ ↦ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))))) |
| 5 | | vonioolem1.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 6 | 5 | mptexd 7244 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
| 7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
| 8 | 4, 7 | fvmpt2d 7029 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 9 | | ovexd 7466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ V) |
| 10 | 8, 9 | fvmpt2d 7029 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐴‘𝑘) + (1 / 𝑛))) |
| 11 | 10 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = ((𝐵‘𝑘) − ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 12 | | vonioolem1.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
| 13 | 12 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 14 | 13 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 15 | 14 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℂ) |
| 16 | | vonioolem1.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
| 17 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ) |
| 18 | 17 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℂ) |
| 20 | | nnrecre 12308 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
| 21 | 20 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
| 22 | 21 | recnd 11289 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℂ) |
| 23 | 15, 19, 22 | subsub4d 11651 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)) = ((𝐵‘𝑘) − ((𝐴‘𝑘) + (1 / 𝑛)))) |
| 24 | 11, 23 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
| 25 | 24 | prodeq2dv 15958 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
| 26 | 25 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)))) |
| 27 | 2, 26 | eqtrd 2777 |
. . 3
⊢ (𝜑 → 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)))) |
| 28 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑘𝜑 |
| 29 | | rpssre 13042 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
| 30 | | vonioolem1.t |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
| 31 | 16 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 32 | | difrp 13073 |
. . . . . . . 8
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → ((𝐴‘𝑘) < (𝐵‘𝑘) ↔ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+)) |
| 33 | 31, 13, 32 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) < (𝐵‘𝑘) ↔ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+)) |
| 34 | 30, 33 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+) |
| 35 | 29, 34 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℝ) |
| 36 | 35 | recnd 11289 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℂ) |
| 37 | | eqid 2737 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
| 38 | 28, 5, 36, 37 | fprodsubrecnncnv 45923 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 39 | 27, 38 | eqbrtrd 5165 |
. 2
⊢ (𝜑 → 𝑇 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 40 | | vonioolem1.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
| 41 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 42 | 41 | mptex 7243 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) ∈ V |
| 43 | 42 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) ∈ V) |
| 44 | 1, 43 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
| 45 | | vonioolem1.s |
. . . 4
⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
| 46 | 41 | mptex 7243 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) ∈ V |
| 47 | 46 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ∈ V) |
| 48 | 45, 47 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
| 49 | | vonioolem1.n |
. . . 4
⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) |
| 50 | | 1rp 13038 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
| 51 | 50 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ+) |
| 52 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 53 | 28, 52, 34 | rnmptssd 45201 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆
ℝ+) |
| 54 | | vonioolem1.e |
. . . . . . . . . . 11
⊢ 𝐸 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) |
| 55 | | ltso 11341 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → < Or
ℝ) |
| 57 | 52 | rnmptfi 45176 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
| 58 | 5, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
| 59 | | vonioolem1.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ≠ ∅) |
| 60 | 28, 34, 52, 59 | rnmptn0 6264 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ≠ ∅) |
| 61 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 62 | 53, 61 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ) |
| 63 | | fiinfcl 9541 |
. . . . . . . . . . . 12
⊢ (( <
Or ℝ ∧ (ran (𝑘
∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ≠ ∅ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ)) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 64 | 56, 58, 60, 62, 63 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (𝜑 → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 65 | 54, 64 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 66 | 53, 65 | sseldd 3984 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 67 | 51, 66 | rpdivcld 13094 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐸) ∈
ℝ+) |
| 68 | 67 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → (1 / 𝐸) ∈ ℝ) |
| 69 | 67 | rpge0d 13081 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (1 / 𝐸)) |
| 70 | | flge0nn0 13860 |
. . . . . . 7
⊢ (((1 /
𝐸) ∈ ℝ ∧ 0
≤ (1 / 𝐸)) →
(⌊‘(1 / 𝐸))
∈ ℕ0) |
| 71 | 68, 69, 70 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (⌊‘(1 / 𝐸)) ∈
ℕ0) |
| 72 | | nn0p1nn 12565 |
. . . . . 6
⊢
((⌊‘(1 / 𝐸)) ∈ ℕ0 →
((⌊‘(1 / 𝐸)) +
1) ∈ ℕ) |
| 73 | 71, 72 | syl 17 |
. . . . 5
⊢ (𝜑 → ((⌊‘(1 / 𝐸)) + 1) ∈
ℕ) |
| 74 | 73 | nnzd 12640 |
. . . 4
⊢ (𝜑 → ((⌊‘(1 / 𝐸)) + 1) ∈
ℤ) |
| 75 | 49, 74 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 76 | 49 | recnnltrp 45388 |
. . . . . . . . . . . . 13
⊢ (𝐸 ∈ ℝ+
→ (𝑁 ∈ ℕ
∧ (1 / 𝑁) < 𝐸)) |
| 77 | 66, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ (1 / 𝑁) < 𝐸)) |
| 78 | 77 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 79 | | uznnssnn 12937 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘𝑁) ⊆ ℕ) |
| 80 | 78, 79 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ ℕ) |
| 81 | 40, 80 | eqsstrid 4022 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ⊆ ℕ) |
| 82 | 81 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑍 ⊆ ℕ) |
| 83 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
| 84 | 82, 83 | sseldd 3984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℕ) |
| 85 | | vonioolem1.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 86 | 85 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
| 87 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
| 88 | | eqid 2737 |
. . . . . . . . . 10
⊢ dom
(voln‘𝑋) = dom
(voln‘𝑋) |
| 89 | 18, 21 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
| 90 | 89 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ) |
| 91 | 8 | feq1d 6720 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐶‘𝑛):𝑋⟶ℝ ↔ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ)) |
| 92 | 90, 91 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
| 93 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵:𝑋⟶ℝ) |
| 94 | 87, 88, 92, 93 | hoimbl 46646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom (voln‘𝑋)) |
| 95 | 94 | elexd 3504 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ V) |
| 96 | 86, 95 | fvmpt2d 7029 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 97 | 84, 96 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
| 98 | 97 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
| 99 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑋 ∈ Fin) |
| 100 | 59 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑋 ≠ ∅) |
| 101 | 84, 92 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐶‘𝑛):𝑋⟶ℝ) |
| 102 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐵:𝑋⟶ℝ) |
| 103 | | eqid 2737 |
. . . . . 6
⊢ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) |
| 104 | 99, 100, 101, 102, 103 | vonn0hoi 46685 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
| 105 | 101 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈ ℝ) |
| 106 | 84, 14 | syldanl 602 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
| 107 | | volico 45998 |
. . . . . . . 8
⊢ ((((𝐶‘𝑛)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0)) |
| 108 | 105, 106,
107 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0)) |
| 109 | 84, 10 | syldanl 602 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐴‘𝑘) + (1 / 𝑛))) |
| 110 | 84, 21 | syldanl 602 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
| 111 | 78 | nnrecred 12317 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / 𝑁) ∈ ℝ) |
| 112 | 111 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) ∈ ℝ) |
| 113 | 35 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℝ) |
| 114 | 40 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑁)) |
| 115 | 114 | biimpi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
| 116 | | eluzle 12891 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑛) |
| 117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑁 ≤ 𝑛) |
| 118 | 117 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑁 ≤ 𝑛) |
| 119 | 78 | nnrpd 13075 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 120 | 119 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑁 ∈
ℝ+) |
| 121 | | nnrp 13046 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
| 122 | 84, 121 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℝ+) |
| 123 | 120, 122 | lerecd 13096 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁 ≤ 𝑛 ↔ (1 / 𝑛) ≤ (1 / 𝑁))) |
| 124 | 118, 123 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (1 / 𝑛) ≤ (1 / 𝑁)) |
| 125 | 124 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ≤ (1 / 𝑁)) |
| 126 | 111 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) ∈ ℝ) |
| 127 | 29, 66 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℝ) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐸 ∈ ℝ) |
| 129 | 77 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 𝑁) < 𝐸) |
| 130 | 129 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < 𝐸) |
| 131 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ) |
| 132 | 58 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
| 133 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋) |
| 134 | | ovexd 7466 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ V) |
| 135 | 52 | elrnmpt1 5971 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ V) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 136 | 133, 134,
135 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 137 | 136 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 138 | | infrefilb 12254 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin ∧ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 139 | 131, 132,
137, 138 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 140 | 54, 139 | eqbrtrid 5178 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐸 ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 141 | 126, 128,
35, 130, 140 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 142 | 141 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 143 | 110, 112,
113, 125, 142 | lelttrd 11419 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
| 144 | 84, 18 | syldanl 602 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
| 145 | 144, 110,
106 | ltaddsub2d 11864 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘) + (1 / 𝑛)) < (𝐵‘𝑘) ↔ (1 / 𝑛) < ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 146 | 143, 145 | mpbird 257 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) < (𝐵‘𝑘)) |
| 147 | 109, 146 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘)) |
| 148 | 147 | iftrued 4533 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0) = ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 149 | 108, 148 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 150 | 149 | prodeq2dv 15958 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 151 | 98, 104, 150 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 152 | | fvexd 6921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) ∈ V) |
| 153 | 45 | fvmpt2 7027 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
((voln‘𝑋)‘(𝐷‘𝑛)) ∈ V) → (𝑆‘𝑛) = ((voln‘𝑋)‘(𝐷‘𝑛))) |
| 154 | 84, 152, 153 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = ((voln‘𝑋)‘(𝐷‘𝑛))) |
| 155 | | prodex 15941 |
. . . . . 6
⊢
∏𝑘 ∈
𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V |
| 156 | 155 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V) |
| 157 | 1 | fvmpt2 7027 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V) → (𝑇‘𝑛) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 158 | 84, 156, 157 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑇‘𝑛) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
| 159 | 151, 154,
158 | 3eqtr4rd 2788 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑇‘𝑛) = (𝑆‘𝑛)) |
| 160 | 40, 44, 48, 75, 159 | climeq 15603 |
. 2
⊢ (𝜑 → (𝑇 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) ↔ 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
| 161 | 39, 160 | mpbid 232 |
1
⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |