Metamath Proof Explorer


Theorem ovnsubaddlem2

Description: ( voln*X ) is subadditive. Proposition 115D (a)(iv) of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsubaddlem2.x ( 𝜑𝑋 ∈ Fin )
ovnsubaddlem2.n0 ( 𝜑𝑋 ≠ ∅ )
ovnsubaddlem2.a ( 𝜑𝐴 : ℕ ⟶ 𝒫 ( ℝ ↑m 𝑋 ) )
ovnsubaddlem2.e ( 𝜑𝐸 ∈ ℝ+ )
ovnsubaddlem2.z 𝑍 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑧 ∈ ℝ* ∣ ∃ 𝑖 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ( 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ∧ 𝑧 = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ( 𝑖𝑗 ) ) ‘ 𝑘 ) ) ) ) ) } )
ovnsubaddlem2.c 𝐶 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ { 𝑙 ∈ ( ( ( ℝ × ℝ ) ↑m 𝑋 ) ↑m ℕ ) ∣ 𝑎 𝑗 ∈ ℕ X 𝑘𝑋 ( ( [,) ∘ ( 𝑙𝑗 ) ) ‘ 𝑘 ) } )
ovnsubaddlem2.l 𝐿 = ( ∈ ( ( ℝ × ℝ ) ↑m 𝑋 ) ↦ ∏ 𝑘𝑋 ( vol ‘ ( ( [,) ∘ ) ‘ 𝑘 ) ) )
ovnsubaddlem2.d 𝐷 = ( 𝑎 ∈ 𝒫 ( ℝ ↑m 𝑋 ) ↦ ( 𝑒 ∈ ℝ+ ↦ { 𝑖 ∈ ( 𝐶𝑎 ) ∣ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝐿 ‘ ( 𝑖𝑗 ) ) ) ) ≤ ( ( ( voln* ‘ 𝑋 ) ‘ 𝑎 ) +𝑒 𝑒 ) } ) )
Assertion ovnsubaddlem2 ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝑛 ∈ ℕ ( 𝐴𝑛 ) ) ≤ ( ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( ( voln* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) +𝑒 𝐸 ) )

Proof

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* ‘ 𝑋 ) ‘ ( 𝐴𝑛 ) ) ) ) +𝑒 𝐸 ) )