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 6391 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) ∈ V) |
8 | 4, 7 | fvmpt2d 6202 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛)))) |
9 | | vonioolem1.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) |
10 | 9 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:𝑋⟶ℝ) |
11 | 10 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
12 | | nnrecre 10934 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → (1 /
𝑛) ∈
ℝ) |
13 | 12 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
14 | 11, 13 | readdcld 9948 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ ℝ) |
15 | 14 | elexd 3187 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) ∈ V) |
16 | 8, 15 | fvmpt2d 6202 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐴‘𝑘) + (1 / 𝑛))) |
17 | 16 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = ((𝐵‘𝑘) − ((𝐴‘𝑘) + (1 / 𝑛)))) |
18 | | vonioolem1.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) |
19 | 18 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
20 | 19 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
21 | 20 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℂ) |
22 | 11 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℂ) |
23 | 13 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℂ) |
24 | 21, 22, 23 | subsub4d 10302 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)) = ((𝐵‘𝑘) − ((𝐴‘𝑘) + (1 / 𝑛)))) |
25 | 17, 24 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
26 | 25 | prodeq2dv 14492 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) = ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
27 | 26 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)))) |
28 | 2, 27 | eqtrd 2644 |
. . 3
⊢ (𝜑 → 𝑇 = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛)))) |
29 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑘𝜑 |
30 | | rpssre 11719 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
31 | | vonioolem1.t |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) < (𝐵‘𝑘)) |
32 | 9 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
33 | | difrp 11744 |
. . . . . . . 8
⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → ((𝐴‘𝑘) < (𝐵‘𝑘) ↔ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+)) |
34 | 32, 19, 33 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) < (𝐵‘𝑘) ↔ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+)) |
35 | 31, 34 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈
ℝ+) |
36 | 30, 35 | sseldi 3566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℝ) |
37 | 36 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℂ) |
38 | | eqid 2610 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) |
39 | 29, 5, 37, 38 | fprodsubrecnncnv 38795 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (((𝐵‘𝑘) − (𝐴‘𝑘)) − (1 / 𝑛))) ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
40 | 28, 39 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → 𝑇 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |
41 | | vonioolem1.z |
. . 3
⊢ 𝑍 =
(ℤ≥‘𝑁) |
42 | | nnex 10903 |
. . . . . 6
⊢ ℕ
∈ V |
43 | 42 | mptex 6390 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) ∈ V |
44 | 43 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) ∈ V) |
45 | 1, 44 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
46 | | vonioolem1.s |
. . . 4
⊢ 𝑆 = (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) |
47 | 42 | mptex 6390 |
. . . . 5
⊢ (𝑛 ∈ ℕ ↦
((voln‘𝑋)‘(𝐷‘𝑛))) ∈ V |
48 | 47 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((voln‘𝑋)‘(𝐷‘𝑛))) ∈ V) |
49 | 46, 48 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑆 ∈ V) |
50 | | vonioolem1.n |
. . . 4
⊢ 𝑁 = ((⌊‘(1 / 𝐸)) + 1) |
51 | | 1rp 11712 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
52 | 51 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ+) |
53 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) = (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
54 | 29, 53, 35 | rnmptssd 38380 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆
ℝ+) |
55 | | vonioolem1.e |
. . . . . . . . . . 11
⊢ 𝐸 = inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) |
56 | | ltso 9997 |
. . . . . . . . . . . . 13
⊢ < Or
ℝ |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → < Or
ℝ) |
58 | 53 | rnmptfi 38346 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
59 | 5, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
60 | | vonioolem1.u |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋 ≠ ∅) |
61 | 29, 35, 53, 60 | rnmptn0 38408 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ≠ ∅) |
62 | 30 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ+
⊆ ℝ) |
63 | 54, 62 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ) |
64 | | fiinfcl 8290 |
. . . . . . . . . . . 12
⊢ (( <
Or ℝ ∧ (ran (𝑘
∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ≠ ∅ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ)) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
65 | 57, 59, 61, 63, 64 | syl13anc 1320 |
. . . . . . . . . . 11
⊢ (𝜑 → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
66 | 55, 65 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
67 | 54, 66 | sseldd 3569 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
68 | 52, 67 | rpdivcld 11765 |
. . . . . . . 8
⊢ (𝜑 → (1 / 𝐸) ∈
ℝ+) |
69 | 68 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → (1 / 𝐸) ∈ ℝ) |
70 | 68 | rpge0d 11752 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (1 / 𝐸)) |
71 | | flge0nn0 12483 |
. . . . . . 7
⊢ (((1 /
𝐸) ∈ ℝ ∧ 0
≤ (1 / 𝐸)) →
(⌊‘(1 / 𝐸))
∈ ℕ0) |
72 | 69, 70, 71 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (⌊‘(1 / 𝐸)) ∈
ℕ0) |
73 | | nn0p1nn 11209 |
. . . . . 6
⊢
((⌊‘(1 / 𝐸)) ∈ ℕ0 →
((⌊‘(1 / 𝐸)) +
1) ∈ ℕ) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢ (𝜑 → ((⌊‘(1 / 𝐸)) + 1) ∈
ℕ) |
75 | 74 | nnzd 11357 |
. . . 4
⊢ (𝜑 → ((⌊‘(1 / 𝐸)) + 1) ∈
ℤ) |
76 | 50, 75 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℤ) |
77 | 50 | recnnltrp 38534 |
. . . . . . . . . . . . 13
⊢ (𝐸 ∈ ℝ+
→ (𝑁 ∈ ℕ
∧ (1 / 𝑁) < 𝐸)) |
78 | 67, 77 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ (1 / 𝑁) < 𝐸)) |
79 | 78 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
80 | | uznnssnn 11611 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(ℤ≥‘𝑁) ⊆ ℕ) |
81 | 79, 80 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(ℤ≥‘𝑁) ⊆ ℕ) |
82 | 41, 81 | syl5eqss 3612 |
. . . . . . . . 9
⊢ (𝜑 → 𝑍 ⊆ ℕ) |
83 | 82 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑍 ⊆ ℕ) |
84 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ 𝑍) |
85 | 83, 84 | sseldd 3569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℕ) |
86 | | vonioolem1.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
87 | 86 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = (𝑛 ∈ ℕ ↦ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
88 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
89 | | eqid 2610 |
. . . . . . . . . 10
⊢ dom
(voln‘𝑋) = dom
(voln‘𝑋) |
90 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) = (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))) |
91 | 14, 90 | fmptd 6292 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ) |
92 | 8 | feq1d 5943 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐶‘𝑛):𝑋⟶ℝ ↔ (𝑘 ∈ 𝑋 ↦ ((𝐴‘𝑘) + (1 / 𝑛))):𝑋⟶ℝ)) |
93 | 91, 92 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘𝑛):𝑋⟶ℝ) |
94 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐵:𝑋⟶ℝ) |
95 | 88, 89, 93, 94 | hoimbl 39521 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ dom (voln‘𝑋)) |
96 | 95 | elexd 3187 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) ∈ V) |
97 | 87, 96 | fvmpt2d 6202 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
98 | 85, 97 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐷‘𝑛) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) |
99 | 98 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
100 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑋 ∈ Fin) |
101 | 60 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑋 ≠ ∅) |
102 | 85, 93 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐶‘𝑛):𝑋⟶ℝ) |
103 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝐵:𝑋⟶ℝ) |
104 | | eqid 2610 |
. . . . . 6
⊢ X𝑘 ∈
𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) = X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)) |
105 | 100, 101,
102, 103, 104 | vonn0hoi 39561 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘X𝑘 ∈ 𝑋 (((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘)))) |
106 | 102 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) ∈ ℝ) |
107 | 85, 20 | syldanl 731 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) |
108 | | volico 38876 |
. . . . . . . 8
⊢ ((((𝐶‘𝑛)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0)) |
109 | 106, 107,
108 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0)) |
110 | 85, 16 | syldanl 731 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) = ((𝐴‘𝑘) + (1 / 𝑛))) |
111 | 85, 13 | syldanl 731 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ∈ ℝ) |
112 | 79 | nnrecred 10943 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / 𝑁) ∈ ℝ) |
113 | 112 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) ∈ ℝ) |
114 | 36 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ℝ) |
115 | 41 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ 𝑍 ↔ 𝑛 ∈ (ℤ≥‘𝑁)) |
116 | 115 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ (ℤ≥‘𝑁)) |
117 | | eluzle 11576 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑛) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝑍 → 𝑁 ≤ 𝑛) |
119 | 118 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑁 ≤ 𝑛) |
120 | 79 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
121 | 120 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑁 ∈
ℝ+) |
122 | | nnrp 11718 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ+) |
123 | 85, 122 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → 𝑛 ∈ ℝ+) |
124 | 121, 123 | lerecd 11767 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑁 ≤ 𝑛 ↔ (1 / 𝑛) ≤ (1 / 𝑁))) |
125 | 119, 124 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (1 / 𝑛) ≤ (1 / 𝑁)) |
126 | 125 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) ≤ (1 / 𝑁)) |
127 | 112 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) ∈ ℝ) |
128 | 30, 67 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 ∈ ℝ) |
129 | 128 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐸 ∈ ℝ) |
130 | 78 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 𝑁) < 𝐸) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < 𝐸) |
132 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ) |
133 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin) |
134 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋) |
135 | | ovex 6577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ V |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ V) |
137 | 53 | elrnmpt1 5295 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑋 ∧ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ V) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
138 | 134, 136,
137 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑋 → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
139 | 138 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
140 | | infrefilb 38541 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ⊆ ℝ ∧ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))) ∈ Fin ∧ ((𝐵‘𝑘) − (𝐴‘𝑘)) ∈ ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘)))) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
141 | 132, 133,
139, 140 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → inf(ran (𝑘 ∈ 𝑋 ↦ ((𝐵‘𝑘) − (𝐴‘𝑘))), ℝ, < ) ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
142 | 55, 141 | syl5eqbr 4618 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → 𝐸 ≤ ((𝐵‘𝑘) − (𝐴‘𝑘))) |
143 | 127, 129,
36, 131, 142 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
144 | 143 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑁) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
145 | 111, 113,
114, 126, 144 | lelttrd 10074 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (1 / 𝑛) < ((𝐵‘𝑘) − (𝐴‘𝑘))) |
146 | 85, 11 | syldanl 731 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) |
147 | 146, 111,
107 | ltaddsub2d 10507 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (((𝐴‘𝑘) + (1 / 𝑛)) < (𝐵‘𝑘) ↔ (1 / 𝑛) < ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
148 | 145, 147 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘) + (1 / 𝑛)) < (𝐵‘𝑘)) |
149 | 110, 148 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → ((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘)) |
150 | 149 | iftrued 4044 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → if(((𝐶‘𝑛)‘𝑘) < (𝐵‘𝑘), ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)), 0) = ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
151 | 109, 150 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑘 ∈ 𝑋) → (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
152 | 151 | prodeq2dv 14492 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∏𝑘 ∈ 𝑋 (vol‘(((𝐶‘𝑛)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
153 | 99, 105, 152 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
154 | | fvex 6113 |
. . . . . 6
⊢
((voln‘𝑋)‘(𝐷‘𝑛)) ∈ V |
155 | 154 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((voln‘𝑋)‘(𝐷‘𝑛)) ∈ V) |
156 | 46 | fvmpt2 6200 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
((voln‘𝑋)‘(𝐷‘𝑛)) ∈ V) → (𝑆‘𝑛) = ((voln‘𝑋)‘(𝐷‘𝑛))) |
157 | 85, 155, 156 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑆‘𝑛) = ((voln‘𝑋)‘(𝐷‘𝑛))) |
158 | | prodex 14476 |
. . . . . 6
⊢
∏𝑘 ∈
𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V |
159 | 158 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V) |
160 | 1 | fvmpt2 6200 |
. . . . 5
⊢ ((𝑛 ∈ ℕ ∧
∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘)) ∈ V) → (𝑇‘𝑛) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
161 | 85, 159, 160 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑇‘𝑛) = ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − ((𝐶‘𝑛)‘𝑘))) |
162 | 153, 157,
161 | 3eqtr4rd 2655 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑇‘𝑛) = (𝑆‘𝑛)) |
163 | 41, 45, 49, 76, 162 | climeq 14146 |
. 2
⊢ (𝜑 → (𝑇 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)) ↔ 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘)))) |
164 | 40, 163 | mpbid 221 |
1
⊢ (𝜑 → 𝑆 ⇝ ∏𝑘 ∈ 𝑋 ((𝐵‘𝑘) − (𝐴‘𝑘))) |