Step | Hyp | Ref
| Expression |
1 | | ovnsubaddlem1.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | ovnsubaddlem1.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ⟶𝒫 (ℝ
↑𝑚 𝑋)) |
3 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ
↑𝑚 𝑋)) |
4 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
5 | 3, 4 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
6 | | elpwi 4117 |
. . . . . . 7
⊢ ((𝐴‘𝑛) ∈ 𝒫 (ℝ
↑𝑚 𝑋) → (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋)) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋)) |
8 | 7 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋)) |
9 | | iunss 4497 |
. . . . 5
⊢ (∪ 𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋) ↔ ∀𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋)) |
10 | 8, 9 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ (ℝ ↑𝑚
𝑋)) |
11 | 1, 10 | ovnxrcl 39459 |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ∈
ℝ*) |
12 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑚𝜑 |
13 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → ℕ ∈
V) |
15 | | icossicc 12131 |
. . . . 5
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
16 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑚 ∈ ℕ) |
17 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝜑) |
18 | 17, 1 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ Fin) |
19 | | ovnsubaddlem1.l |
. . . . . 6
⊢ 𝐿 = (𝑖 ∈ ((ℝ × ℝ)
↑𝑚 𝑋) ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘))) |
20 | | ovnsubaddlem1.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:ℕ–1-1-onto→(ℕ × ℕ)) |
21 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ⟶(ℕ ×
ℕ)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶(ℕ ×
ℕ)) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℕ⟶(ℕ ×
ℕ)) |
24 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
25 | 23, 24 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ (ℕ ×
ℕ)) |
26 | | xp1st 7089 |
. . . . . . . . 9
⊢ ((𝐹‘𝑚) ∈ (ℕ × ℕ) →
(1st ‘(𝐹‘𝑚)) ∈ ℕ) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐹‘𝑚)) ∈
ℕ) |
28 | | xp2nd 7090 |
. . . . . . . . 9
⊢ ((𝐹‘𝑚) ∈ (ℕ × ℕ) →
(2nd ‘(𝐹‘𝑚)) ∈ ℕ) |
29 | 25, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (2nd
‘(𝐹‘𝑚)) ∈
ℕ) |
30 | | fvex 6113 |
. . . . . . . . 9
⊢
(2nd ‘(𝐹‘𝑚)) ∈ V |
31 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑗 = (2nd ‘(𝐹‘𝑚)) → (𝑗 ∈ ℕ ↔ (2nd
‘(𝐹‘𝑚)) ∈
ℕ)) |
32 | 31 | 3anbi3d 1397 |
. . . . . . . . . 10
⊢ (𝑗 = (2nd ‘(𝐹‘𝑚)) → ((𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ ∧ (2nd
‘(𝐹‘𝑚)) ∈
ℕ))) |
33 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑗 = (2nd ‘(𝐹‘𝑚)) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘𝑗) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
34 | 33 | feq1d 5943 |
. . . . . . . . . 10
⊢ (𝑗 = (2nd ‘(𝐹‘𝑚)) → (((𝐼‘(1st ‘(𝐹‘𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ) ↔
((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚))):𝑋⟶(ℝ ×
ℝ))) |
35 | 32, 34 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑗 = (2nd ‘(𝐹‘𝑚)) → (((𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔
((𝜑 ∧ (1st
‘(𝐹‘𝑚)) ∈ ℕ ∧
(2nd ‘(𝐹‘𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))):𝑋⟶(ℝ ×
ℝ)))) |
36 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1st ‘(𝐹‘𝑚)) ∈ V |
37 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (𝑛 ∈ ℕ ↔ (1st
‘(𝐹‘𝑚)) ∈
ℕ)) |
38 | 37 | 3anbi2d 1396 |
. . . . . . . . . . 11
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ))) |
39 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (𝐼‘𝑛) = (𝐼‘(1st ‘(𝐹‘𝑚)))) |
40 | 39 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → ((𝐼‘𝑛)‘𝑗) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘𝑗)) |
41 | 40 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔
((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗):𝑋⟶(ℝ ×
ℝ))) |
42 | 38, 41 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔
((𝜑 ∧ (1st
‘(𝐹‘𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗):𝑋⟶(ℝ ×
ℝ)))) |
43 | | ovnsubaddlem1.c |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)})) |
45 | | sseq1 3589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝐴‘𝑛) → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ↔ (𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘))) |
46 | 45 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (𝐴‘𝑛) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴‘𝑛)) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
48 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∈
V |
49 | 48 | rabex 4740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {ℎ ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ∈ V |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ∈ V) |
51 | 44, 47, 5, 50 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘(𝐴‘𝑛)) = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
52 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . 19
⊢ {ℎ ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
54 | 51, 53 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐶‘(𝐴‘𝑛)) ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
55 | | ovnsubaddlem1.d |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)})) |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))) |
57 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = (𝐴‘𝑛) → (𝐶‘𝑎) = (𝐶‘(𝐴‘𝑛))) |
58 | 57 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = (𝐴‘𝑛) → (𝑖 ∈ (𝐶‘𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘𝑛)))) |
59 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = (𝐴‘𝑛) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘𝑛))) |
60 | 59 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = (𝐴‘𝑛) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)) |
61 | 60 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = (𝐴‘𝑛) →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒))) |
62 | 58, 61 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (𝐴‘𝑛) → ((𝑖 ∈ (𝐶‘𝑎) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)))) |
63 | 62 | rabbidva2 3162 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = (𝐴‘𝑛) → {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)}) |
64 | 63 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (𝐴‘𝑛) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)})) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴‘𝑛)) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)})) |
66 | | rpex 38503 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
ℝ+ ∈ V |
67 | 66 | mptex 6390 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)}) ∈ V |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)}) ∈ V) |
69 | 56, 65, 5, 68 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐷‘(𝐴‘𝑛)) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)})) |
70 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 = (𝐸 / (2↑𝑛)) → (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))) |
71 | 70 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = (𝐸 / (2↑𝑛)) →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) |
72 | 71 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = (𝐸 / (2↑𝑛)) → {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))}) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑𝑛))) → {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))}) |
74 | | ovnsubaddlem1.e |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐸 ∈
ℝ+) |
76 | | 2nn 11062 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 2 ∈
ℕ |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ℕ → 2 ∈
ℕ) |
78 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
79 | 77, 78 | nnexpcld 12892 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
80 | 79 | nnrpd 11746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ+) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ+) |
82 | 75, 81 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈
ℝ+) |
83 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶‘(𝐴‘𝑛)) ∈ V |
84 | 83 | rabex 4740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ∈ V) |
86 | 69, 73, 82, 85 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛))) = {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))}) |
87 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴‘𝑛)) |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ⊆ (𝐶‘(𝐴‘𝑛))) |
89 | 86, 88 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛))) ⊆ (𝐶‘(𝐴‘𝑛))) |
90 | | ovnsubaddlem1.i |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛)))) |
91 | 89, 90 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) |
92 | 54, 91 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
93 | | elmapfn 7766 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼‘𝑛) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝐼‘𝑛) Fn ℕ) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) Fn ℕ) |
95 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼‘𝑛) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝐼‘𝑛):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
97 | 96 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
98 | 97 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
99 | 94, 98 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐼‘𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋))) |
100 | 99 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋))) |
101 | | ffnfv 6295 |
. . . . . . . . . . . . 13
⊢ ((𝐼‘𝑛):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋) ↔ ((𝐼‘𝑛) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋))) |
102 | 100, 101 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐼‘𝑛):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
103 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ) |
104 | 102, 103 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
105 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ (((𝐼‘𝑛)‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋) → ((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
106 | 104, 105 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
107 | 36, 42, 106 | vtocl 3232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1st
‘(𝐹‘𝑚)) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
108 | 30, 35, 107 | vtocl 3232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1st
‘(𝐹‘𝑚)) ∈ ℕ ∧
(2nd ‘(𝐹‘𝑚)) ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))):𝑋⟶(ℝ ×
ℝ)) |
109 | 17, 27, 29, 108 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))):𝑋⟶(ℝ ×
ℝ)) |
110 | | id 22 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ) |
111 | | fvex 6113 |
. . . . . . . . . . 11
⊢ ((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚))) ∈ V |
112 | 111 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → ((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚))) ∈ V) |
113 | | ovnsubaddlem1.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
114 | 113 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ ((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚))) ∈ V) → (𝐺‘𝑚) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
115 | 110, 112,
114 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → (𝐺‘𝑚) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
116 | 115 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
117 | 116 | feq1d 5943 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐺‘𝑚):𝑋⟶(ℝ × ℝ) ↔
((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚))):𝑋⟶(ℝ ×
ℝ))) |
118 | 109, 117 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐺‘𝑚):𝑋⟶(ℝ ×
ℝ)) |
119 | 16, 18, 19, 118 | hoiprodcl2 39445 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐿‘(𝐺‘𝑚)) ∈ (0[,)+∞)) |
120 | 15, 119 | sseldi 3566 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐿‘(𝐺‘𝑚)) ∈ (0[,]+∞)) |
121 | 12, 14, 120 | sge0xrclmpt 39321 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚)))) ∈
ℝ*) |
122 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑛𝜑 |
123 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
124 | 123 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ*) |
125 | | pnfxr 9971 |
. . . . . 6
⊢ +∞
∈ ℝ* |
126 | 125 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → +∞ ∈
ℝ*) |
127 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) |
128 | | ovnsubaddlem1.z |
. . . . . . . . 9
⊢ 𝑍 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
129 | 127, 7, 128 | ovnval2b 39442 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴‘𝑛)) = if(𝑋 = ∅, 0, inf((𝑍‘(𝐴‘𝑛)), ℝ*, <
))) |
130 | | ovnsubaddlem1.n0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ ∅) |
131 | 130 | neneqd 2787 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 = ∅) |
132 | 131 | iffalsed 4047 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴‘𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴‘𝑛)), ℝ*, <
)) |
133 | 132 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if(𝑋 = ∅, 0, inf((𝑍‘(𝐴‘𝑛)), ℝ*, < )) = inf((𝑍‘(𝐴‘𝑛)), ℝ*, <
)) |
134 | 129, 133 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴‘𝑛)) = inf((𝑍‘(𝐴‘𝑛)), ℝ*, <
)) |
135 | 128 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑍 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))})) |
136 | | sseq1 3589 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝐴‘𝑛) → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
137 | 136 | anbi1d 737 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝐴‘𝑛) → ((𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
138 | 137 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝐴‘𝑛) → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
139 | 138 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝐴‘𝑛) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
140 | 139 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑎 = (𝐴‘𝑛)) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
141 | | xrex 11705 |
. . . . . . . . . . . 12
⊢
ℝ* ∈ V |
142 | 141 | rabex 4740 |
. . . . . . . . . . 11
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∈ V |
143 | 142 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ∈ V) |
144 | 135, 140,
5, 143 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑍‘(𝐴‘𝑛)) = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
145 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* |
146 | 145 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ*) |
147 | 144, 146 | eqsstrd 3602 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑍‘(𝐴‘𝑛)) ⊆
ℝ*) |
148 | | infxrcl 12035 |
. . . . . . . 8
⊢ ((𝑍‘(𝐴‘𝑛)) ⊆ ℝ* →
inf((𝑍‘(𝐴‘𝑛)), ℝ*, < ) ∈
ℝ*) |
149 | 147, 148 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → inf((𝑍‘(𝐴‘𝑛)), ℝ*, < ) ∈
ℝ*) |
150 | 134, 149 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴‘𝑛)) ∈
ℝ*) |
151 | 74 | rpred 11748 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℝ) |
152 | 151 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐸 ∈ ℝ) |
153 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
154 | 153 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ∈
ℝ) |
155 | 154, 78 | reexpcld 12887 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℝ) |
156 | 155 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ∈
ℝ) |
157 | 154 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ∈
ℂ) |
158 | | 2ne0 10990 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
159 | 158 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 2 ≠
0) |
160 | | nnz 11276 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
161 | 157, 159,
160 | expne0d 12876 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ≠
0) |
162 | 161 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2↑𝑛) ≠ 0) |
163 | 152, 156,
162 | redivcld 10732 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ) |
164 | 163 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈
ℝ*) |
165 | 150, 164 | xaddcld 12003 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈
ℝ*) |
166 | 127, 7 | ovncl 39457 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴‘𝑛)) ∈ (0[,]+∞)) |
167 | | xrge0ge0 38504 |
. . . . . . 7
⊢
(((voln*‘𝑋)‘(𝐴‘𝑛)) ∈ (0[,]+∞) → 0 ≤
((voln*‘𝑋)‘(𝐴‘𝑛))) |
168 | 166, 167 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
((voln*‘𝑋)‘(𝐴‘𝑛))) |
169 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ∈
ℝ) |
170 | 82 | rpgt0d 11751 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 < (𝐸 / (2↑𝑛))) |
171 | 169, 163,
170 | ltled 10064 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤ (𝐸 / (2↑𝑛))) |
172 | 163 | ltpnfd 11831 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) < +∞) |
173 | 164, 126,
172 | xrltled 38427 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ≤ +∞) |
174 | 124, 126,
164, 171, 173 | eliccxrd 38600 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ (0[,]+∞)) |
175 | 150, 174 | xadd0ge 38477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((voln*‘𝑋)‘(𝐴‘𝑛)) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))) |
176 | 124, 150,
165, 168, 175 | xrletrd 11869 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 0 ≤
(((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))) |
177 | | pnfge 11840 |
. . . . . 6
⊢
((((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ ℝ* →
(((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞) |
178 | 165, 177 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ≤ +∞) |
179 | 124, 126,
165, 176, 178 | eliccxrd 38600 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ∈ (0[,]+∞)) |
180 | 122, 14, 179 | sge0xrclmpt 39321 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) ∈
ℝ*) |
181 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐶 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)})) |
182 | | sseq1 3589 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → (𝑎 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ↔ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘))) |
183 | 182 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
184 | 183 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚)))) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
185 | 2 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ
↑𝑚 𝑋)) |
186 | 185, 27 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐴‘(1st ‘(𝐹‘𝑚))) ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
187 | 48 | rabex 4740 |
. . . . . . . . . . . . 13
⊢ {ℎ ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ∈ V |
188 | 187 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ∈ V) |
189 | 181, 184,
186, 188 | fvmptd 6197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
190 | | ssrab2 3650 |
. . . . . . . . . . . 12
⊢ {ℎ ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ) |
191 | 190 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘(1st ‘(𝐹‘𝑚))) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
192 | 189, 191 | eqsstrd 3602 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ⊆ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
193 | 55 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐷 = (𝑎 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))) |
194 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → (𝐶‘𝑎) = (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
195 | 194 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → (𝑖 ∈ (𝐶‘𝑎) ↔ 𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))))) |
196 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → ((voln*‘𝑋)‘𝑎) = ((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
197 | 196 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)) |
198 | 197 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒))) |
199 | 195, 198 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → ((𝑖 ∈ (𝐶‘𝑎) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)) ↔ (𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)))) |
200 | 199 | rabbidva2 3162 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)}) |
201 | 200 | mpteq2dv 4673 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)})) |
202 | 201 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑎 = (𝐴‘(1st ‘(𝐹‘𝑚)))) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘𝑎) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)})) |
203 | 66 | mptex 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ ℝ+
↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)}) ∈ V |
204 | 203 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)}) ∈ V) |
205 | 193, 202,
186, 204 | fvmptd 6197 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚)))) = (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)})) |
206 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))) → (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒) = (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))) |
207 | 206 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))) →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚))))))) |
208 | 207 | rabbidv 3164 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))}) |
209 | 208 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑒 = (𝐸 / (2↑(1st ‘(𝐹‘𝑚))))) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 𝑒)} = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))}) |
210 | 17, 74 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐸 ∈
ℝ+) |
211 | | 2rp 11713 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
212 | 211 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 2 ∈
ℝ+) |
213 | 27 | nnzd 11357 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1st
‘(𝐹‘𝑚)) ∈
ℤ) |
214 | 212, 213 | rpexpcld 12894 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(2↑(1st ‘(𝐹‘𝑚))) ∈
ℝ+) |
215 | 210, 214 | rpdivcld 11765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))) ∈
ℝ+) |
216 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∈ V |
217 | 216 | rabex 4740 |
. . . . . . . . . . . . . 14
⊢ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))} ∈ V |
218 | 217 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))} ∈ V) |
219 | 205, 209,
215, 218 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚))))) = {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))}) |
220 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) |
221 | 220 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑖 ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚)))) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘(1st ‘(𝐹‘𝑚)))) +𝑒 (𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))} ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
222 | 219, 221 | eqsstrd 3602 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚))))) ⊆ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
223 | 37 | anbi2d 736 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → ((𝜑 ∧ 𝑛 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ))) |
224 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (𝐴‘𝑛) = (𝐴‘(1st ‘(𝐹‘𝑚)))) |
225 | 224 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (𝐷‘(𝐴‘𝑛)) = (𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
226 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (2↑𝑛) = (2↑(1st ‘(𝐹‘𝑚)))) |
227 | 226 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (𝐸 / (2↑𝑛)) = (𝐸 / (2↑(1st ‘(𝐹‘𝑚))))) |
228 | 225, 227 | fveq12d 6109 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛))) = ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))) |
229 | 39, 228 | eleq12d 2682 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → ((𝐼‘𝑛) ∈ ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛))) ↔ (𝐼‘(1st ‘(𝐹‘𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚))))))) |
230 | 223, 229 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (1st ‘(𝐹‘𝑚)) → (((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ ((𝐷‘(𝐴‘𝑛))‘(𝐸 / (2↑𝑛)))) ↔ ((𝜑 ∧ (1st ‘(𝐹‘𝑚)) ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))))) |
231 | 36, 230, 90 | vtocl 3232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (1st
‘(𝐹‘𝑚)) ∈ ℕ) → (𝐼‘(1st
‘(𝐹‘𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))) |
232 | 17, 27, 231 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))) ∈ ((𝐷‘(𝐴‘(1st ‘(𝐹‘𝑚))))‘(𝐸 / (2↑(1st ‘(𝐹‘𝑚)))))) |
233 | 222, 232 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))) ∈ (𝐶‘(𝐴‘(1st ‘(𝐹‘𝑚))))) |
234 | 192, 233 | sseldd 3569 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚
ℕ)) |
235 | | elmapfn 7766 |
. . . . . . . . 9
⊢ ((𝐼‘(1st
‘(𝐹‘𝑚))) ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝐼‘(1st
‘(𝐹‘𝑚))) Fn ℕ) |
236 | 234, 235 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))) Fn ℕ) |
237 | | elmapi 7765 |
. . . . . . . . . . 11
⊢ ((𝐼‘(1st
‘(𝐹‘𝑚))) ∈ (((ℝ ×
ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) →
(𝐼‘(1st
‘(𝐹‘𝑚))):ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋)) |
238 | 234, 237 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
239 | 238 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
240 | 239 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ∀𝑗 ∈ ℕ ((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
241 | 236, 240 | jca 553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋))) |
242 | | ffnfv 6295 |
. . . . . . 7
⊢ ((𝐼‘(1st
‘(𝐹‘𝑚))):ℕ⟶((ℝ
× ℝ) ↑𝑚 𝑋) ↔ ((𝐼‘(1st ‘(𝐹‘𝑚))) Fn ℕ ∧ ∀𝑗 ∈ ℕ ((𝐼‘(1st
‘(𝐹‘𝑚)))‘𝑗) ∈ ((ℝ × ℝ)
↑𝑚 𝑋))) |
243 | 241, 242 | sylibr 223 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐼‘(1st ‘(𝐹‘𝑚))):ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
244 | 243, 29 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))) ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
245 | 244, 113 | fmptd 6292 |
. . . 4
⊢ (𝜑 → 𝐺:ℕ⟶((ℝ × ℝ)
↑𝑚 𝑋)) |
246 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝜑) |
247 | 90, 86 | eleqtrd 2690 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))}) |
248 | 87, 247 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) |
249 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) → (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) |
250 | 51 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) → (𝐶‘(𝐴‘𝑛)) = {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
251 | 249, 250 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) → (𝐼‘𝑛) ∈ {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)}) |
252 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (ℎ = (𝐼‘𝑛) → (ℎ‘𝑗) = ((𝐼‘𝑛)‘𝑗)) |
253 | 252 | coeq2d 5206 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = (𝐼‘𝑛) → ([,) ∘ (ℎ‘𝑗)) = ([,) ∘ ((𝐼‘𝑛)‘𝑗))) |
254 | 253 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ (ℎ = (𝐼‘𝑛) → (([,) ∘ (ℎ‘𝑗))‘𝑘) = (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘)) |
255 | 254 | ixpeq2dv 7810 |
. . . . . . . . . . . . . 14
⊢ (ℎ = (𝐼‘𝑛) → X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘)) |
256 | 255 | iuneq2d 4483 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝐼‘𝑛) → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘)) |
257 | 256 | sseq2d 3596 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝐼‘𝑛) → ((𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘) ↔ (𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘))) |
258 | 257 | elrab 3331 |
. . . . . . . . . . 11
⊢ ((𝐼‘𝑛) ∈ {ℎ ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)
∣ (𝐴‘𝑛) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (ℎ‘𝑗))‘𝑘)} ↔ ((𝐼‘𝑛) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘))) |
259 | 251, 258 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) → ((𝐼‘𝑛) ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ) ∧
(𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘))) |
260 | 259 | simprd 478 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ (𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛))) → (𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘)) |
261 | 246, 4, 248, 260 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘)) |
262 | | f1ofo 6057 |
. . . . . . . . . . . . . 14
⊢ (𝐹:ℕ–1-1-onto→(ℕ × ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ)) |
263 | 20, 262 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ–onto→(ℕ × ℕ)) |
264 | 263 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝐹:ℕ–onto→(ℕ × ℕ)) |
265 | | opelxpi 5072 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) →
〈𝑛, 𝑗〉 ∈ (ℕ ×
ℕ)) |
266 | 4, 265 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 〈𝑛, 𝑗〉 ∈ (ℕ ×
ℕ)) |
267 | | foelrni 6154 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℕ–onto→(ℕ × ℕ) ∧ 〈𝑛, 𝑗〉 ∈ (ℕ × ℕ))
→ ∃𝑚 ∈
ℕ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) |
268 | 264, 266,
267 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ ℕ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) |
269 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) |
270 | | nfre1 2988 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑚∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) |
271 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → 𝑚 ∈ ℕ) |
272 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → (1st ‘(𝐹‘𝑚)) = (1st ‘〈𝑛, 𝑗〉)) |
273 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
274 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑗 ∈ V |
275 | | op1stg 7071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑛 ∈ V ∧ 𝑗 ∈ V) →
(1st ‘〈𝑛, 𝑗〉) = 𝑛) |
276 | 273, 274,
275 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1st ‘〈𝑛, 𝑗〉) = 𝑛 |
277 | 276 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → (1st
‘〈𝑛, 𝑗〉) = 𝑛) |
278 | 272, 277 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → (1st ‘(𝐹‘𝑚)) = 𝑛) |
279 | 278 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → (1st ‘(𝐹‘𝑚)) = 𝑛) |
280 | 271, 279 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → (𝑚 ∈ ℕ ∧ (1st
‘(𝐹‘𝑚)) = 𝑛)) |
281 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑚 → (𝐹‘𝑖) = (𝐹‘𝑚)) |
282 | 281 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑚 → (1st ‘(𝐹‘𝑖)) = (1st ‘(𝐹‘𝑚))) |
283 | 282 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑚 → ((1st ‘(𝐹‘𝑖)) = 𝑛 ↔ (1st ‘(𝐹‘𝑚)) = 𝑛)) |
284 | 283 | elrab 3331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛} ↔ (𝑚 ∈ ℕ ∧ (1st
‘(𝐹‘𝑚)) = 𝑛)) |
285 | 280, 284 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}) |
286 | 285 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}) |
287 | 271, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → (𝐺‘𝑚) = ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))) |
288 | 278 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → (𝐼‘(1st ‘(𝐹‘𝑚))) = (𝐼‘𝑛)) |
289 | 273, 274 | op2ndd 7070 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → (2nd ‘(𝐹‘𝑚)) = 𝑗) |
290 | 288, 289 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))) = ((𝐼‘𝑛)‘𝑗)) |
291 | 290 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → ((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))) = ((𝐼‘𝑛)‘𝑗)) |
292 | 287, 291 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → ((𝐼‘𝑛)‘𝑗) = (𝐺‘𝑚)) |
293 | 292 | coeq2d 5206 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → ([,) ∘ ((𝐼‘𝑛)‘𝑗)) = ([,) ∘ (𝐺‘𝑚))) |
294 | 293 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) = (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
295 | 294 | ixpeq2dv 7810 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
296 | | eqimss 3620 |
. . . . . . . . . . . . . . . 16
⊢ (X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) → X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
297 | 295, 296 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
298 | 297 | 3adant1 1072 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
299 | | rspe 2986 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛} ∧ X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
300 | 286, 298,
299 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑚 ∈ ℕ ∧ (𝐹‘𝑚) = 〈𝑛, 𝑗〉) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
301 | 300 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝑚 ∈ ℕ → ((𝐹‘𝑚) = 〈𝑛, 𝑗〉 → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)))) |
302 | 269, 270,
301 | rexlimd 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (∃𝑚 ∈ ℕ (𝐹‘𝑚) = 〈𝑛, 𝑗〉 → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘))) |
303 | 268, 302 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
304 | 303 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∀𝑗 ∈ ℕ ∃𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
305 | | iunss2 4501 |
. . . . . . . . 9
⊢
(∀𝑗 ∈
ℕ ∃𝑚 ∈
{𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ ∪
𝑚 ∈ {𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
306 | 304, 305 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ ((𝐼‘𝑛)‘𝑗))‘𝑘) ⊆ ∪
𝑚 ∈ {𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
307 | 261, 306 | sstrd 3578 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ {𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
308 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛} ⊆ ℕ |
309 | | iunss1 4468 |
. . . . . . . . 9
⊢ ({𝑖 ∈ ℕ ∣
(1st ‘(𝐹‘𝑖)) = 𝑛} ⊆ ℕ → ∪ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
310 | 308, 309 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) |
311 | 310 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∪ 𝑚 ∈ {𝑖 ∈ ℕ ∣ (1st
‘(𝐹‘𝑖)) = 𝑛}X𝑘 ∈ 𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
312 | 307, 311 | sstrd 3578 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
313 | 312 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
314 | | iunss 4497 |
. . . . 5
⊢ (∪ 𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘) ↔ ∀𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
315 | 313, 314 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐴‘𝑛) ⊆ ∪
𝑚 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝐺‘𝑚))‘𝑘)) |
316 | 1, 130, 19, 245, 315 | ovnlecvr 39448 |
. . 3
⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚))))) |
317 | 116 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐿‘(𝐺‘𝑚)) = (𝐿‘((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))))) |
318 | 317 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚))) = (𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚)))))) |
319 | 318 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚)))) =
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))))))) |
320 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑝𝜑 |
321 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑝 = (𝐹‘𝑚) → (1st ‘𝑝) = (1st
‘(𝐹‘𝑚))) |
322 | 321 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑝 = (𝐹‘𝑚) → (𝐼‘(1st ‘𝑝)) = (𝐼‘(1st ‘(𝐹‘𝑚)))) |
323 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑝 = (𝐹‘𝑚) → (2nd ‘𝑝) = (2nd
‘(𝐹‘𝑚))) |
324 | 322, 323 | fveq12d 6109 |
. . . . . . 7
⊢ (𝑝 = (𝐹‘𝑚) → ((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝)) = ((𝐼‘(1st
‘(𝐹‘𝑚)))‘(2nd
‘(𝐹‘𝑚)))) |
325 | 324 | fveq2d 6107 |
. . . . . 6
⊢ (𝑝 = (𝐹‘𝑚) → (𝐿‘((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝))) = (𝐿‘((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))))) |
326 | | eqidd 2611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) = (𝐹‘𝑚)) |
327 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ 𝑝 ∈ (ℕ ×
ℕ)) |
328 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
𝑋 ∈
Fin) |
329 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
𝜑) |
330 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (ℕ ×
ℕ) → (1st ‘𝑝) ∈ ℕ) |
331 | 330 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
(1st ‘𝑝)
∈ ℕ) |
332 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (ℕ ×
ℕ) → (2nd ‘𝑝) ∈ ℕ) |
333 | 332 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
(2nd ‘𝑝)
∈ ℕ) |
334 | | fvex 6113 |
. . . . . . . . . 10
⊢
(2nd ‘𝑝) ∈ V |
335 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑗 = (2nd ‘𝑝) → (𝑗 ∈ ℕ ↔ (2nd
‘𝑝) ∈
ℕ)) |
336 | 335 | 3anbi3d 1397 |
. . . . . . . . . . 11
⊢ (𝑗 = (2nd ‘𝑝) → ((𝜑 ∧ (1st ‘𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st
‘𝑝) ∈ ℕ
∧ (2nd ‘𝑝) ∈ ℕ))) |
337 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = (2nd ‘𝑝) → ((𝐼‘(1st ‘𝑝))‘𝑗) = ((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝))) |
338 | 337 | feq1d 5943 |
. . . . . . . . . . 11
⊢ (𝑗 = (2nd ‘𝑝) → (((𝐼‘(1st ‘𝑝))‘𝑗):𝑋⟶(ℝ × ℝ) ↔
((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝)):𝑋⟶(ℝ ×
ℝ))) |
339 | 336, 338 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑗 = (2nd ‘𝑝) → (((𝜑 ∧ (1st ‘𝑝) ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘(1st
‘𝑝))‘𝑗):𝑋⟶(ℝ × ℝ)) ↔
((𝜑 ∧ (1st
‘𝑝) ∈ ℕ
∧ (2nd ‘𝑝) ∈ ℕ) → ((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝)):𝑋⟶(ℝ ×
ℝ)))) |
340 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(1st ‘𝑝) ∈ V |
341 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (1st ‘𝑝) → (𝑛 ∈ ℕ ↔ (1st
‘𝑝) ∈
ℕ)) |
342 | 341 | 3anbi2d 1396 |
. . . . . . . . . . . 12
⊢ (𝑛 = (1st ‘𝑝) → ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) ↔ (𝜑 ∧ (1st ‘𝑝) ∈ ℕ ∧ 𝑗 ∈
ℕ))) |
343 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (1st ‘𝑝) → (𝐼‘𝑛) = (𝐼‘(1st ‘𝑝))) |
344 | 343 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (1st ‘𝑝) → ((𝐼‘𝑛)‘𝑗) = ((𝐼‘(1st ‘𝑝))‘𝑗)) |
345 | 344 | feq1d 5943 |
. . . . . . . . . . . 12
⊢ (𝑛 = (1st ‘𝑝) → (((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ × ℝ) ↔
((𝐼‘(1st
‘𝑝))‘𝑗):𝑋⟶(ℝ ×
ℝ))) |
346 | 342, 345 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑛 = (1st ‘𝑝) → (((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ × ℝ)) ↔
((𝜑 ∧ (1st
‘𝑝) ∈ ℕ
∧ 𝑗 ∈ ℕ)
→ ((𝐼‘(1st ‘𝑝))‘𝑗):𝑋⟶(ℝ ×
ℝ)))) |
347 | 340, 346,
106 | vtocl 3232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (1st
‘𝑝) ∈ ℕ
∧ 𝑗 ∈ ℕ)
→ ((𝐼‘(1st ‘𝑝))‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
348 | 334, 339,
347 | vtocl 3232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (1st
‘𝑝) ∈ ℕ
∧ (2nd ‘𝑝) ∈ ℕ) → ((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝)):𝑋⟶(ℝ ×
ℝ)) |
349 | 329, 331,
333, 348 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝)):𝑋⟶(ℝ ×
ℝ)) |
350 | 327, 328,
19, 349 | hoiprodcl2 39445 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝))) ∈
(0[,)+∞)) |
351 | 15, 350 | sseldi 3566 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (ℕ × ℕ)) →
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝))) ∈
(0[,]+∞)) |
352 | 320, 12, 325, 14, 20, 326, 351 | sge0f1o 39275 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝))))) =
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘((𝐼‘(1st ‘(𝐹‘𝑚)))‘(2nd ‘(𝐹‘𝑚))))))) |
353 | 319, 352 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚)))) =
(Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝)))))) |
354 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑗𝜑 |
355 | 273, 274 | op1std 7069 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑛, 𝑗〉 → (1st ‘𝑝) = 𝑛) |
356 | 355 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑛, 𝑗〉 → (𝐼‘(1st ‘𝑝)) = (𝐼‘𝑛)) |
357 | 273, 274 | op2ndd 7070 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑛, 𝑗〉 → (2nd ‘𝑝) = 𝑗) |
358 | 356, 357 | fveq12d 6109 |
. . . . . . . 8
⊢ (𝑝 = 〈𝑛, 𝑗〉 → ((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝)) = ((𝐼‘𝑛)‘𝑗)) |
359 | 358 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑝 = 〈𝑛, 𝑗〉 → (𝐿‘((𝐼‘(1st ‘𝑝))‘(2nd
‘𝑝))) = (𝐿‘((𝐼‘𝑛)‘𝑗))) |
360 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑘((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) |
361 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 𝑋 ∈ Fin) |
362 | 97, 105 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → ((𝐼‘𝑛)‘𝑗):𝑋⟶(ℝ ×
ℝ)) |
363 | 360, 361,
19, 362 | hoiprodcl2 39445 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼‘𝑛)‘𝑗)) ∈ (0[,)+∞)) |
364 | 15, 363 | sseldi 3566 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼‘𝑛)‘𝑗)) ∈ (0[,]+∞)) |
365 | 364 | 3impa 1251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑗 ∈ ℕ) → (𝐿‘((𝐼‘𝑛)‘𝑗)) ∈ (0[,]+∞)) |
366 | 354, 359,
14, 14, 365 | sge0xp 39322 |
. . . . . 6
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))))) =
(Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝)))))) |
367 | 366 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝))))) =
(Σ^‘(𝑛 ∈ ℕ ↦
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗))))))) |
368 | 13 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ ∈
V) |
369 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗))) |
370 | 364, 369 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗))):ℕ⟶(0[,]+∞)) |
371 | 368, 370 | sge0cl 39274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) ∈ (0[,]+∞)) |
372 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐼‘𝑛) → (𝑖‘𝑗) = ((𝐼‘𝑛)‘𝑗)) |
373 | 372 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼‘𝑛) → (𝐿‘(𝑖‘𝑗)) = (𝐿‘((𝐼‘𝑛)‘𝑗))) |
374 | 373 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝐼‘𝑛) → (𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗))) = (𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) |
375 | 374 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑖 = (𝐼‘𝑛) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) =
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗))))) |
376 | 375 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑖 = (𝐼‘𝑛) →
((Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))) ↔
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) |
377 | 376 | elrab 3331 |
. . . . . . . 8
⊢ ((𝐼‘𝑛) ∈ {𝑖 ∈ (𝐶‘(𝐴‘𝑛)) ∣
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))} ↔ ((𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) |
378 | 247, 377 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐼‘𝑛) ∈ (𝐶‘(𝐴‘𝑛)) ∧
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) |
379 | 378 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))) ≤ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))) |
380 | 122, 14, 371, 179, 379 | sge0lempt 39303 |
. . . . 5
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦
(Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘((𝐼‘𝑛)‘𝑗)))))) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))) |
381 | 367, 380 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑝 ∈ (ℕ × ℕ) ↦
(𝐿‘((𝐼‘(1st
‘𝑝))‘(2nd ‘𝑝))))) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))) |
382 | 353, 381 | eqbrtrd 4605 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑚 ∈ ℕ ↦ (𝐿‘(𝐺‘𝑚)))) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))) |
383 | 11, 121, 180, 316, 382 | xrletrd 11869 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛)))))) |
384 | 122, 14, 166, 174 | sge0xadd 39328 |
. . 3
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))))) |
385 | 123 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℝ*) |
386 | 125 | a1i 11 |
. . . . . 6
⊢ (𝜑 → +∞ ∈
ℝ*) |
387 | 151 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ*) |
388 | 74 | rpge0d 11752 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝐸) |
389 | 151 | ltpnfd 11831 |
. . . . . 6
⊢ (𝜑 → 𝐸 < +∞) |
390 | 385, 386,
387, 388, 389 | elicod 12095 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) |
391 | 390 | sge0ad2en 39324 |
. . . 4
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛)))) = 𝐸) |
392 | 391 | oveq2d 6565 |
. . 3
⊢ (𝜑 →
((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒
(Σ^‘(𝑛 ∈ ℕ ↦ (𝐸 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸)) |
393 | 384, 392 | eqtrd 2644 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑛 ∈ ℕ ↦ (((voln*‘𝑋)‘(𝐴‘𝑛)) +𝑒 (𝐸 / (2↑𝑛))))) =
((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸)) |
394 | 383, 393 | breqtrd 4609 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘∪ 𝑛 ∈ ℕ (𝐴‘𝑛)) ≤
((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴‘𝑛)))) +𝑒 𝐸)) |