Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovnsubaddlem2 Structured version   Visualization version   GIF version

Theorem ovnsubaddlem2 39258
Description: (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
ovnsubaddlem2.x (𝜑𝑋 ∈ Fin)
ovnsubaddlem2.n0 (𝜑𝑋 ≠ ∅)
ovnsubaddlem2.a (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
ovnsubaddlem2.e (𝜑𝐸 ∈ ℝ+)
ovnsubaddlem2.z 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
ovnsubaddlem2.c 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
ovnsubaddlem2.l 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)))
ovnsubaddlem2.d 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
Assertion
Ref Expression
ovnsubaddlem2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Distinct variable groups:   𝐴,𝑎,𝑒,𝑖,𝑗,𝑛   𝐴,𝑘,𝑙,𝑎,𝑖,𝑗,𝑛   𝑧,𝐴,𝑎,𝑖,𝑗,𝑘,𝑛   𝐶,𝑎,𝑒,𝑖   𝐷,𝑎,𝑒,𝑖,𝑗,𝑛   𝐷,𝑘   𝐸,𝑎,𝑒,𝑖,𝑗,𝑛   𝑘,𝐸   𝐿,𝑎,𝑒,𝑖,𝑗,𝑛   𝑋,𝑎,𝑒,𝑖,𝑗,𝑛   ,𝑋,𝑘,𝑖,𝑗   𝑋,𝑙   𝑧,𝑋   𝜑,𝑎,𝑒,𝑖,𝑗,𝑛   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑧,,𝑙)   𝐴()   𝐶(𝑧,,𝑗,𝑘,𝑛,𝑙)   𝐷(𝑧,,𝑙)   𝐸(𝑧,,𝑙)   𝐿(𝑧,,𝑘,𝑙)   𝑍(𝑧,𝑒,,𝑖,𝑗,𝑘,𝑛,𝑎,𝑙)

Proof of Theorem ovnsubaddlem2
Dummy variables 𝑓 𝑔 𝑚 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6098 . . . 4 ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ∈ V
2 nnenom 12596 . . . 4 ℕ ≈ ω
31, 2axcc3 9120 . . 3 𝑔(𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
4 simprl 789 . . . . . 6 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))) → 𝑔 Fn ℕ)
5 nfv 1829 . . . . . . . . 9 𝑛𝜑
6 nfra1 2924 . . . . . . . . 9 𝑛𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
75, 6nfan 1815 . . . . . . . 8 𝑛(𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
8 rspa 2913 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑛 ∈ ℕ) → (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
98adantll 745 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) ∧ 𝑛 ∈ ℕ) → (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
10 ovnsubaddlem2.x . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ∈ Fin)
1110adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝑋 ∈ Fin)
12 ovnsubaddlem2.n0 . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ≠ ∅)
1312adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝑋 ≠ ∅)
14 ovnsubaddlem2.a . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
1514adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
16 simpr 475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
1715, 16ffvelrnd 6253 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
18 elpwi 4116 . . . . . . . . . . . . . . . . 17 ((𝐴𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
1917, 18syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ (ℝ ↑𝑚 𝑋))
20 ovnsubaddlem2.e . . . . . . . . . . . . . . . . . 18 (𝜑𝐸 ∈ ℝ+)
2120adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
22 nnnn0 11146 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
23 2nn 11032 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ
2423a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ0 → 2 ∈ ℕ)
25 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ ℕ0𝑛 ∈ ℕ0)
26 nnexpcl 12690 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
2724, 25, 26syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℕ)
28 nnrp 11674 . . . . . . . . . . . . . . . . . . . 20 ((2↑𝑛) ∈ ℕ → (2↑𝑛) ∈ ℝ+)
2927, 28syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ0 → (2↑𝑛) ∈ ℝ+)
3022, 29syl 17 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℝ+)
3130adantl 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
3221, 31rpdivcld 11721 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐸 / (2↑𝑛)) ∈ ℝ+)
33 ovnsubaddlem2.c . . . . . . . . . . . . . . . 16 𝐶 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑙 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ) ∣ 𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑙𝑗))‘𝑘)})
34 ovnsubaddlem2.l . . . . . . . . . . . . . . . 16 𝐿 = ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)))
35 ovnsubaddlem2.d . . . . . . . . . . . . . . . 16 𝐷 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ (𝑒 ∈ ℝ+ ↦ {𝑖 ∈ (𝐶𝑎) ∣ (Σ^‘(𝑗 ∈ ℕ ↦ (𝐿‘(𝑖𝑗)))) ≤ (((voln*‘𝑋)‘𝑎) +𝑒 𝑒)}))
3611, 13, 19, 32, 33, 34, 35ovncvrrp 39251 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑖 𝑖 ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
37 n0 3889 . . . . . . . . . . . . . . 15 (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ ↔ ∃𝑖 𝑖 ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
3836, 37sylibr 222 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅)
3938adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅)
40 simpr 475 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
4139, 40mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
4241ex 448 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
4342adantlr 746 . . . . . . . . . 10 (((𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) ∧ 𝑛 ∈ ℕ) → ((((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
449, 43mpd 15 . . . . . . . . 9 (((𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) ∧ 𝑛 ∈ ℕ) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
4544ex 448 . . . . . . . 8 ((𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → (𝑛 ∈ ℕ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
467, 45ralrimi 2939 . . . . . . 7 ((𝜑 ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
4746adantrl 747 . . . . . 6 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
484, 47jca 552 . . . . 5 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))) → (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
4948ex 448 . . . 4 (𝜑 → ((𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))))
5049eximdv 1832 . . 3 (𝜑 → (∃𝑔(𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ≠ ∅ → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → ∃𝑔(𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))))
513, 50mpi 20 . 2 (𝜑 → ∃𝑔(𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
52 simpl 471 . . . . 5 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → 𝜑)
53 simprl 789 . . . . 5 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → 𝑔 Fn ℕ)
54 simprr 791 . . . . 5 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
55 nnf1oxpnn 38175 . . . . . 6 𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ)
56 simpl1 1056 . . . . . . . . 9 (((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝜑)
57 simpl2 1057 . . . . . . . . 9 (((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑔 Fn ℕ)
58 fveq2 6088 . . . . . . . . . . . . . 14 (𝑞 = 𝑛 → (𝑔𝑞) = (𝑔𝑛))
59 fveq2 6088 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑛 → (𝐴𝑞) = (𝐴𝑛))
6059fveq2d 6092 . . . . . . . . . . . . . . 15 (𝑞 = 𝑛 → (𝐷‘(𝐴𝑞)) = (𝐷‘(𝐴𝑛)))
61 oveq2 6535 . . . . . . . . . . . . . . . 16 (𝑞 = 𝑛 → (2↑𝑞) = (2↑𝑛))
6261oveq2d 6543 . . . . . . . . . . . . . . 15 (𝑞 = 𝑛 → (𝐸 / (2↑𝑞)) = (𝐸 / (2↑𝑛)))
6360, 62fveq12d 6094 . . . . . . . . . . . . . 14 (𝑞 = 𝑛 → ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))) = ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
6458, 63eleq12d 2681 . . . . . . . . . . . . 13 (𝑞 = 𝑛 → ((𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))) ↔ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))))
6564cbvralv 3146 . . . . . . . . . . . 12 (∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))) ↔ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
6665biimpri 216 . . . . . . . . . . 11 (∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) → ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))))
67663ad2ant3 1076 . . . . . . . . . 10 ((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))))
6867adantr 479 . . . . . . . . 9 (((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))))
69 simpr 475 . . . . . . . . 9 (((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑓:ℕ–1-1-onto→(ℕ × ℕ))
7010adantr 479 . . . . . . . . . . 11 ((𝜑𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑋 ∈ Fin)
71703ad2antl1 1215 . . . . . . . . . 10 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑋 ∈ Fin)
7212adantr 479 . . . . . . . . . . 11 ((𝜑𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑋 ≠ ∅)
73723ad2antl1 1215 . . . . . . . . . 10 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑋 ≠ ∅)
7414adantr 479 . . . . . . . . . . 11 ((𝜑𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
75743ad2antl1 1215 . . . . . . . . . 10 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝐴:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
7620adantr 479 . . . . . . . . . . 11 ((𝜑𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝐸 ∈ ℝ+)
77763ad2antl1 1215 . . . . . . . . . 10 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝐸 ∈ ℝ+)
78 ovnsubaddlem2.z . . . . . . . . . 10 𝑍 = (𝑎 ∈ 𝒫 (ℝ ↑𝑚 𝑋) ↦ {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑎 𝑗 ∈ ℕ X𝑘𝑋 (([,) ∘ (𝑖𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘𝑋 (vol‘(([,) ∘ (𝑖𝑗))‘𝑘)))))})
79 coeq2 5190 . . . . . . . . . . . . . . 15 ( = 𝑖 → ([,) ∘ ) = ([,) ∘ 𝑖))
8079fveq1d 6090 . . . . . . . . . . . . . 14 ( = 𝑖 → (([,) ∘ )‘𝑘) = (([,) ∘ 𝑖)‘𝑘))
8180fveq2d 6092 . . . . . . . . . . . . 13 ( = 𝑖 → (vol‘(([,) ∘ )‘𝑘)) = (vol‘(([,) ∘ 𝑖)‘𝑘)))
8281prodeq2ad 38456 . . . . . . . . . . . 12 ( = 𝑖 → ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘)) = ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
8382cbvmptv 4672 . . . . . . . . . . 11 ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ )‘𝑘))) = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
8434, 83eqtri 2631 . . . . . . . . . 10 𝐿 = (𝑖 ∈ ((ℝ × ℝ) ↑𝑚 𝑋) ↦ ∏𝑘𝑋 (vol‘(([,) ∘ 𝑖)‘𝑘)))
8565biimpi 204 . . . . . . . . . . . . 13 (∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
86853ad2ant3 1076 . . . . . . . . . . . 12 ((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
8786ad2antrr 757 . . . . . . . . . . 11 ((((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) ∧ 𝑛 ∈ ℕ) → ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
88 simpr 475 . . . . . . . . . . 11 ((((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
89 rspa 2913 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))) ∧ 𝑛 ∈ ℕ) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
9087, 88, 89syl2anc 690 . . . . . . . . . 10 ((((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) ∧ 𝑛 ∈ ℕ) → (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))
91 simpr 475 . . . . . . . . . 10 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → 𝑓:ℕ–1-1-onto→(ℕ × ℕ))
92 fveq2 6088 . . . . . . . . . . . . . 14 (𝑞 = 𝑚 → (𝑓𝑞) = (𝑓𝑚))
9392fveq2d 6092 . . . . . . . . . . . . 13 (𝑞 = 𝑚 → (1st ‘(𝑓𝑞)) = (1st ‘(𝑓𝑚)))
9493fveq2d 6092 . . . . . . . . . . . 12 (𝑞 = 𝑚 → (𝑔‘(1st ‘(𝑓𝑞))) = (𝑔‘(1st ‘(𝑓𝑚))))
9592fveq2d 6092 . . . . . . . . . . . 12 (𝑞 = 𝑚 → (2nd ‘(𝑓𝑞)) = (2nd ‘(𝑓𝑚)))
9694, 95fveq12d 6094 . . . . . . . . . . 11 (𝑞 = 𝑚 → ((𝑔‘(1st ‘(𝑓𝑞)))‘(2nd ‘(𝑓𝑞))) = ((𝑔‘(1st ‘(𝑓𝑚)))‘(2nd ‘(𝑓𝑚))))
9796cbvmptv 4672 . . . . . . . . . 10 (𝑞 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑓𝑞)))‘(2nd ‘(𝑓𝑞)))) = (𝑚 ∈ ℕ ↦ ((𝑔‘(1st ‘(𝑓𝑚)))‘(2nd ‘(𝑓𝑚))))
9871, 73, 75, 77, 78, 33, 84, 35, 90, 91, 97ovnsubaddlem1 39257 . . . . . . . . 9 (((𝜑𝑔 Fn ℕ ∧ ∀𝑞 ∈ ℕ (𝑔𝑞) ∈ ((𝐷‘(𝐴𝑞))‘(𝐸 / (2↑𝑞)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
9956, 57, 68, 69, 98syl31anc 1320 . . . . . . . 8 (((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) ∧ 𝑓:ℕ–1-1-onto→(ℕ × ℕ)) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
10099ex 448 . . . . . . 7 ((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → (𝑓:ℕ–1-1-onto→(ℕ × ℕ) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸)))
101100exlimdv 1847 . . . . . 6 ((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → (∃𝑓 𝑓:ℕ–1-1-onto→(ℕ × ℕ) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸)))
10255, 101mpi 20 . . . . 5 ((𝜑𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
10352, 53, 54, 102syl3anc 1317 . . . 4 ((𝜑 ∧ (𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛))))) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
104103ex 448 . . 3 (𝜑 → ((𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸)))
105104exlimdv 1847 . 2 (𝜑 → (∃𝑔(𝑔 Fn ℕ ∧ ∀𝑛 ∈ ℕ (𝑔𝑛) ∈ ((𝐷‘(𝐴𝑛))‘(𝐸 / (2↑𝑛)))) → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸)))
10651, 105mpd 15 1 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐴𝑛)) ≤ ((Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐴𝑛)))) +𝑒 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  wss 3539  c0 3873  𝒫 cpw 4107   ciun 4449   class class class wbr 4577  cmpt 4637   × cxp 5026  ccom 5032   Fn wfn 5785  wf 5786  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  1st c1st 7034  2nd c2nd 7035  𝑚 cmap 7721  Xcixp 7771  Fincfn 7818  cr 9791  *cxr 9929  cle 9931   / cdiv 10533  cn 10867  2c2 10917  0cn0 11139  +crp 11664   +𝑒 cxad 11776  [,)cico 12004  cexp 12677  cprod 14420  volcvol 22956  Σ^csumge0 39052  voln*covoln 39223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cc 9117  ax-ac2 9145  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-tpos 7216  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-acn 8628  df-ac 8799  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-seq 12619  df-exp 12678  df-hash 12935  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-clim 14013  df-rlim 14014  df-sum 14211  df-prod 14421  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-rest 15852  df-0g 15871  df-topgen 15873  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-grp 17194  df-minusg 17195  df-subg 17360  df-cmn 17964  df-abl 17965  df-mgp 18259  df-ur 18271  df-ring 18318  df-cring 18319  df-oppr 18392  df-dvdsr 18410  df-unit 18411  df-invr 18441  df-dvr 18452  df-drng 18518  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-cmp 20942  df-ovol 22957  df-vol 22958  df-sumge0 39053  df-ovoln 39224
This theorem is referenced by:  ovnsubadd  39259
  Copyright terms: Public domain W3C validator