Step |
Hyp |
Ref |
Expression |
1 |
|
ovnsubaddlem2.x |
⊢ ( 𝜑 → 𝑋 ∈ Fin ) |
2 |
|
ovnsubaddlem2.n0 |
⊢ ( 𝜑 → 𝑋 ≠ ∅ ) |
3 |
|
ovnsubaddlem2.a |
⊢ ( 𝜑 → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) |
4 |
|
ovnsubaddlem2.e |
⊢ ( 𝜑 → 𝐸 ∈ ℝ+ ) |
5 |
|
ovnsubaddlem2.z |
⊢ 𝑍 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖 ‘ 𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } ) |
6 |
|
ovnsubaddlem2.c |
⊢ 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 ⊆ ∪ 𝑗 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( [,) ∘ ( 𝑙 ‘ 𝑗 ) ) ‘ 𝑘 ) } ) |
7 |
|
ovnsubaddlem2.l |
⊢ 𝐿 = ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) |
8 |
|
ovnsubaddlem2.d |
⊢ 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶 ‘ 𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖 ‘ 𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) ) |
9 |
|
fvex |
⊢ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∈ V |
10 |
|
nnenom |
⊢ ℕ ≈ ω |
11 |
9 10
|
axcc3 |
⊢ ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
12 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → 𝑔 Fn ℕ ) |
13 |
|
nfv |
⊢ Ⅎ 𝑛 𝜑 |
14 |
|
nfra1 |
⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
15 |
13 14
|
nfan |
⊢ Ⅎ 𝑛 ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
16 |
|
rspa |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
17 |
16
|
adantll |
⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
18 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ Fin ) |
19 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑋 ≠ ∅ ) |
20 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) |
21 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
22 |
20 21
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) ) |
23 |
|
elpwi |
⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ 𝒫 ( ℝ ↑m 𝑋 ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
24 |
22 23
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ⊆ ( ℝ ↑m 𝑋 ) ) |
25 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ+ ) |
26 |
|
nnnn0 |
⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 ) |
27 |
|
2nn |
⊢ 2 ∈ ℕ |
28 |
27
|
a1i |
⊢ ( 𝑛 ∈ ℕ0 → 2 ∈ ℕ ) |
29 |
|
id |
⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 ) |
30 |
|
nnexpcl |
⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ ) |
31 |
28 29 30
|
syl2anc |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℕ ) |
32 |
|
nnrp |
⊢ ( ( 2 ↑ 𝑛 ) ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ ) |
33 |
31 32
|
syl |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 ↑ 𝑛 ) ∈ ℝ+ ) |
34 |
26 33
|
syl |
⊢ ( 𝑛 ∈ ℕ → ( 2 ↑ 𝑛 ) ∈ ℝ+ ) |
35 |
34
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 2 ↑ 𝑛 ) ∈ ℝ+ ) |
36 |
25 35
|
rpdivcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐸 / ( 2 ↑ 𝑛 ) ) ∈ ℝ+ ) |
37 |
18 19 24 36 6 7 8
|
ovncvrrp |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
38 |
|
n0 |
⊢ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ ↔ ∃ 𝑖 𝑖 ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
39 |
37 38
|
sylibr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ ) |
40 |
39
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ ) |
41 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
42 |
40 41
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
43 |
42
|
ex |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
44 |
43
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
45 |
17 44
|
mpd |
⊢ ( ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
46 |
45
|
ex |
⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ℕ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
47 |
15 46
|
ralrimi |
⊢ ( ( 𝜑 ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
48 |
47
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
49 |
12 48
|
jca |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) → ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
50 |
49
|
ex |
⊢ ( 𝜑 → ( ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) |
51 |
50
|
eximdv |
⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ≠ ∅ → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) ) |
52 |
11 51
|
mpi |
⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
53 |
|
simpl |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝜑 ) |
54 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → 𝑔 Fn ℕ ) |
55 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
56 |
|
nnf1oxpnn |
⊢ ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) |
57 |
|
simpl1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝜑 ) |
58 |
|
simpl2 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑔 Fn ℕ ) |
59 |
|
fveq2 |
⊢ ( 𝑞 = 𝑛 → ( 𝑔 ‘ 𝑞 ) = ( 𝑔 ‘ 𝑛 ) ) |
60 |
|
2fveq3 |
⊢ ( 𝑞 = 𝑛 → ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) = ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ) |
61 |
|
oveq2 |
⊢ ( 𝑞 = 𝑛 → ( 2 ↑ 𝑞 ) = ( 2 ↑ 𝑛 ) ) |
62 |
61
|
oveq2d |
⊢ ( 𝑞 = 𝑛 → ( 𝐸 / ( 2 ↑ 𝑞 ) ) = ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) |
63 |
60 62
|
fveq12d |
⊢ ( 𝑞 = 𝑛 → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) = ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
64 |
59 63
|
eleq12d |
⊢ ( 𝑞 = 𝑛 → ( ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ↔ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) |
65 |
64
|
cbvralvw |
⊢ ( ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ↔ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
66 |
65
|
biimpri |
⊢ ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) |
67 |
66
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) |
68 |
67
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) |
69 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) |
70 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ∈ Fin ) |
71 |
70
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ∈ Fin ) |
72 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ≠ ∅ ) |
73 |
72
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑋 ≠ ∅ ) |
74 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) |
75 |
74
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) ) |
76 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐸 ∈ ℝ+ ) |
77 |
76
|
3ad2antl1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝐸 ∈ ℝ+ ) |
78 |
|
coeq2 |
⊢ ( ℎ = 𝑖 → ( [,) ∘ ℎ ) = ( [,) ∘ 𝑖 ) ) |
79 |
78
|
fveq1d |
⊢ ( ℎ = 𝑖 → ( ( [,) ∘ ℎ ) ‘ 𝑘 ) = ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) |
80 |
79
|
fveq2d |
⊢ ( ℎ = 𝑖 → ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) ) |
81 |
80
|
prodeq2ad |
⊢ ( ℎ = 𝑖 → ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) ) |
82 |
81
|
cbvmptv |
⊢ ( ℎ ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ ℎ ) ‘ 𝑘 ) ) ) = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) ) |
83 |
7 82
|
eqtri |
⊢ 𝐿 = ( 𝑖 ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( [,) ∘ 𝑖 ) ‘ 𝑘 ) ) ) |
84 |
65
|
biimpi |
⊢ ( ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
85 |
84
|
3ad2ant3 |
⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
86 |
85
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
87 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ ) |
88 |
|
rspa |
⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
89 |
86 87 88
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) |
90 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) |
91 |
|
2fveq3 |
⊢ ( 𝑞 = 𝑚 → ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) = ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) |
92 |
91
|
fveq2d |
⊢ ( 𝑞 = 𝑚 → ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) = ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) |
93 |
|
2fveq3 |
⊢ ( 𝑞 = 𝑚 → ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) |
94 |
92 93
|
fveq12d |
⊢ ( 𝑞 = 𝑚 → ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) ) = ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) |
95 |
94
|
cbvmptv |
⊢ ( 𝑞 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑞 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑞 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑔 ‘ ( 1st ‘ ( 𝑓 ‘ 𝑚 ) ) ) ‘ ( 2nd ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) |
96 |
71 73 75 77 5 6 83 8 89 90 95
|
ovnsubaddlem1 |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑞 ∈ ℕ ( 𝑔 ‘ 𝑞 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑞 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑞 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) |
97 |
57 58 68 69 96
|
syl31anc |
⊢ ( ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ∧ 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) |
98 |
97
|
ex |
⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) ) |
99 |
98
|
exlimdv |
⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ∃ 𝑓 𝑓 : ℕ –1-1-onto→ ( ℕ × ℕ ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) ) |
100 |
56 99
|
mpi |
⊢ ( ( 𝜑 ∧ 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) |
101 |
53 54 55 100
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) |
102 |
101
|
ex |
⊢ ( 𝜑 → ( ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) ) |
103 |
102
|
exlimdv |
⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝑛 ) ) ‘ ( 𝐸 / ( 2 ↑ 𝑛 ) ) ) ) → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) ) |
104 |
52 103
|
mpd |
⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ ∪ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴 ‘ 𝑛 ) ) ) ) +𝑒 𝐸 ) ) |