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

Theorem ovnsubadd2lem 39335
Description: (voln*‘𝑋) is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . The special case of the union of 2 sets. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
Hypotheses
Ref Expression
ovnsubadd2lem.x (𝜑𝑋 ∈ Fin)
ovnsubadd2lem.a (𝜑𝐴 ⊆ (ℝ ↑𝑚 𝑋))
ovnsubadd2lem.b (𝜑𝐵 ⊆ (ℝ ↑𝑚 𝑋))
ovnsubadd2lem.c 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
Assertion
Ref Expression
ovnsubadd2lem (𝜑 → ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝐶,𝑛   𝑛,𝑋   𝜑,𝑛

Proof of Theorem ovnsubadd2lem
StepHypRef Expression
1 ovnsubadd2lem.x . . 3 (𝜑𝑋 ∈ Fin)
2 iftrue 4037 . . . . . . . 8 (𝑛 = 1 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐴)
32adantl 480 . . . . . . 7 ((𝜑𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐴)
4 ovex 6551 . . . . . . . . . . 11 (ℝ ↑𝑚 𝑋) ∈ V
54a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ ↑𝑚 𝑋) ∈ V)
6 ovnsubadd2lem.a . . . . . . . . . 10 (𝜑𝐴 ⊆ (ℝ ↑𝑚 𝑋))
75, 6ssexd 4724 . . . . . . . . 9 (𝜑𝐴 ∈ V)
87, 6elpwd 38063 . . . . . . . 8 (𝜑𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
98adantr 479 . . . . . . 7 ((𝜑𝑛 = 1) → 𝐴 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
103, 9eqeltrd 2683 . . . . . 6 ((𝜑𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
1110adantlr 746 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ 𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
12 simpl 471 . . . . . . . . . . 11 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → ¬ 𝑛 = 1)
1312iffalsed 4042 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
14 simpr 475 . . . . . . . . . . 11 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → 𝑛 = 2)
1514iftrued 4039 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 2, 𝐵, ∅) = 𝐵)
1613, 15eqtrd 2639 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
1716adantll 745 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
18 ovnsubadd2lem.b . . . . . . . . . . 11 (𝜑𝐵 ⊆ (ℝ ↑𝑚 𝑋))
195, 18ssexd 4724 . . . . . . . . . 10 (𝜑𝐵 ∈ V)
2019, 18elpwd 38063 . . . . . . . . 9 (𝜑𝐵 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
2120ad2antrr 757 . . . . . . . 8 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → 𝐵 ∈ 𝒫 (ℝ ↑𝑚 𝑋))
2217, 21eqeltrd 2683 . . . . . . 7 (((𝜑 ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
2322adantllr 750 . . . . . 6 ((((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) ∧ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
24 simpl 471 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ¬ 𝑛 = 1)
2524iffalsed 4042 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
26 simpr 475 . . . . . . . . . 10 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ¬ 𝑛 = 2)
2726iffalsed 4042 . . . . . . . . 9 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 2, 𝐵, ∅) = ∅)
2825, 27eqtrd 2639 . . . . . . . 8 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
29 0elpw 4751 . . . . . . . . 9 ∅ ∈ 𝒫 (ℝ ↑𝑚 𝑋)
3029a1i 11 . . . . . . . 8 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → ∅ ∈ 𝒫 (ℝ ↑𝑚 𝑋))
3128, 30eqeltrd 2683 . . . . . . 7 ((¬ 𝑛 = 1 ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
3231adantll 745 . . . . . 6 ((((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) ∧ ¬ 𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
3323, 32pm2.61dan 827 . . . . 5 (((𝜑𝑛 ∈ ℕ) ∧ ¬ 𝑛 = 1) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
3411, 33pm2.61dan 827 . . . 4 ((𝜑𝑛 ∈ ℕ) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
35 ovnsubadd2lem.c . . . 4 𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
3634, 35fmptd 6273 . . 3 (𝜑𝐶:ℕ⟶𝒫 (ℝ ↑𝑚 𝑋))
371, 36ovnsubadd 39262 . 2 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
38 eldifi 3689 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ {1, 2}) → 𝑛 ∈ ℕ)
3938adantl 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → 𝑛 ∈ ℕ)
40 eldifn 3690 . . . . . . . . . . . . . 14 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 ∈ {1, 2})
41 vex 3171 . . . . . . . . . . . . . . . . 17 𝑛 ∈ V
4241a1i 11 . . . . . . . . . . . . . . . 16 𝑛 ∈ {1, 2} → 𝑛 ∈ V)
43 id 22 . . . . . . . . . . . . . . . 16 𝑛 ∈ {1, 2} → ¬ 𝑛 ∈ {1, 2})
4442, 43nelpr1 38088 . . . . . . . . . . . . . . 15 𝑛 ∈ {1, 2} → 𝑛 ≠ 1)
4544neneqd 2782 . . . . . . . . . . . . . 14 𝑛 ∈ {1, 2} → ¬ 𝑛 = 1)
4640, 45syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 = 1)
4742, 43nelpr2 38087 . . . . . . . . . . . . . . 15 𝑛 ∈ {1, 2} → 𝑛 ≠ 2)
4847neneqd 2782 . . . . . . . . . . . . . 14 𝑛 ∈ {1, 2} → ¬ 𝑛 = 2)
4940, 48syl 17 . . . . . . . . . . . . 13 (𝑛 ∈ (ℕ ∖ {1, 2}) → ¬ 𝑛 = 2)
5046, 49, 28syl2anc 690 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ {1, 2}) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
51 0ex 4709 . . . . . . . . . . . . 13 ∅ ∈ V
5251a1i 11 . . . . . . . . . . . 12 (𝑛 ∈ (ℕ ∖ {1, 2}) → ∅ ∈ V)
5350, 52eqeltrd 2683 . . . . . . . . . . 11 (𝑛 ∈ (ℕ ∖ {1, 2}) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V)
5453adantl 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V)
5535fvmpt2 6181 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) ∈ V) → (𝐶𝑛) = if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
5639, 54, 55syl2anc 690 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → (𝐶𝑛) = if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)))
5750adantl 480 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = ∅)
5856, 57eqtrd 2639 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → (𝐶𝑛) = ∅)
5958ralrimiva 2944 . . . . . . 7 (𝜑 → ∀𝑛 ∈ (ℕ ∖ {1, 2})(𝐶𝑛) = ∅)
60 nfcv 2746 . . . . . . . 8 𝑛(ℕ ∖ {1, 2})
6160iunxdif3 4532 . . . . . . 7 (∀𝑛 ∈ (ℕ ∖ {1, 2})(𝐶𝑛) = ∅ → 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ ℕ (𝐶𝑛))
6259, 61syl 17 . . . . . 6 (𝜑 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ ℕ (𝐶𝑛))
6362eqcomd 2611 . . . . 5 (𝜑 𝑛 ∈ ℕ (𝐶𝑛) = 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛))
64 1nn 10874 . . . . . . . . . 10 1 ∈ ℕ
65 2nn 11028 . . . . . . . . . 10 2 ∈ ℕ
6664, 65pm3.2i 469 . . . . . . . . 9 (1 ∈ ℕ ∧ 2 ∈ ℕ)
67 prssi 4288 . . . . . . . . 9 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → {1, 2} ⊆ ℕ)
6866, 67ax-mp 5 . . . . . . . 8 {1, 2} ⊆ ℕ
69 dfss4 3815 . . . . . . . 8 ({1, 2} ⊆ ℕ ↔ (ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2})
7068, 69mpbi 218 . . . . . . 7 (ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2}
71 iuneq1 4460 . . . . . . 7 ((ℕ ∖ (ℕ ∖ {1, 2})) = {1, 2} → 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛))
7270, 71ax-mp 5 . . . . . 6 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛)
7372a1i 11 . . . . 5 (𝜑 𝑛 ∈ (ℕ ∖ (ℕ ∖ {1, 2}))(𝐶𝑛) = 𝑛 ∈ {1, 2} (𝐶𝑛))
74 fveq2 6084 . . . . . . . . 9 (𝑛 = 1 → (𝐶𝑛) = (𝐶‘1))
75 fveq2 6084 . . . . . . . . 9 (𝑛 = 2 → (𝐶𝑛) = (𝐶‘2))
7674, 75iunxprg 4533 . . . . . . . 8 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2)))
7764, 65, 76mp2an 703 . . . . . . 7 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2))
7877a1i 11 . . . . . 6 (𝜑 𝑛 ∈ {1, 2} (𝐶𝑛) = ((𝐶‘1) ∪ (𝐶‘2)))
7935a1i 11 . . . . . . . 8 (𝜑𝐶 = (𝑛 ∈ ℕ ↦ if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅))))
8064a1i 11 . . . . . . . 8 (𝜑 → 1 ∈ ℕ)
8179, 3, 80, 7fvmptd 6178 . . . . . . 7 (𝜑 → (𝐶‘1) = 𝐴)
82 id 22 . . . . . . . . . . . . 13 (𝑛 = 2 → 𝑛 = 2)
83 1ne2 11083 . . . . . . . . . . . . . . 15 1 ≠ 2
8483necomi 2831 . . . . . . . . . . . . . 14 2 ≠ 1
8584a1i 11 . . . . . . . . . . . . 13 (𝑛 = 2 → 2 ≠ 1)
8682, 85eqnetrd 2844 . . . . . . . . . . . 12 (𝑛 = 2 → 𝑛 ≠ 1)
8786neneqd 2782 . . . . . . . . . . 11 (𝑛 = 2 → ¬ 𝑛 = 1)
8887iffalsed 4042 . . . . . . . . . 10 (𝑛 = 2 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = if(𝑛 = 2, 𝐵, ∅))
89 iftrue 4037 . . . . . . . . . 10 (𝑛 = 2 → if(𝑛 = 2, 𝐵, ∅) = 𝐵)
9088, 89eqtrd 2639 . . . . . . . . 9 (𝑛 = 2 → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
9190adantl 480 . . . . . . . 8 ((𝜑𝑛 = 2) → if(𝑛 = 1, 𝐴, if(𝑛 = 2, 𝐵, ∅)) = 𝐵)
9265a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℕ)
9379, 91, 92, 19fvmptd 6178 . . . . . . 7 (𝜑 → (𝐶‘2) = 𝐵)
9481, 93uneq12d 3725 . . . . . 6 (𝜑 → ((𝐶‘1) ∪ (𝐶‘2)) = (𝐴𝐵))
95 eqidd 2606 . . . . . 6 (𝜑 → (𝐴𝐵) = (𝐴𝐵))
9678, 94, 953eqtrd 2643 . . . . 5 (𝜑 𝑛 ∈ {1, 2} (𝐶𝑛) = (𝐴𝐵))
9763, 73, 963eqtrd 2643 . . . 4 (𝜑 𝑛 ∈ ℕ (𝐶𝑛) = (𝐴𝐵))
9897fveq2d 6088 . . 3 (𝜑 → ((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) = ((voln*‘𝑋)‘(𝐴𝐵)))
99 nfv 1828 . . . . . 6 𝑛𝜑
100 nnex 10869 . . . . . . 7 ℕ ∈ V
101100a1i 11 . . . . . 6 (𝜑 → ℕ ∈ V)
10268a1i 11 . . . . . 6 (𝜑 → {1, 2} ⊆ ℕ)
1031adantr 479 . . . . . . 7 ((𝜑𝑛 ∈ {1, 2}) → 𝑋 ∈ Fin)
104 simpl 471 . . . . . . . 8 ((𝜑𝑛 ∈ {1, 2}) → 𝜑)
105102sselda 3563 . . . . . . . 8 ((𝜑𝑛 ∈ {1, 2}) → 𝑛 ∈ ℕ)
10636ffvelrnda 6248 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋))
107 elpwi 4112 . . . . . . . . 9 ((𝐶𝑛) ∈ 𝒫 (ℝ ↑𝑚 𝑋) → (𝐶𝑛) ⊆ (ℝ ↑𝑚 𝑋))
108106, 107syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐶𝑛) ⊆ (ℝ ↑𝑚 𝑋))
109104, 105, 108syl2anc 690 . . . . . . 7 ((𝜑𝑛 ∈ {1, 2}) → (𝐶𝑛) ⊆ (ℝ ↑𝑚 𝑋))
110103, 109ovncl 39257 . . . . . 6 ((𝜑𝑛 ∈ {1, 2}) → ((voln*‘𝑋)‘(𝐶𝑛)) ∈ (0[,]+∞))
11158fveq2d 6088 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘∅))
1121adantr 479 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → 𝑋 ∈ Fin)
113112ovn0 39256 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘∅) = 0)
114111, 113eqtrd 2639 . . . . . 6 ((𝜑𝑛 ∈ (ℕ ∖ {1, 2})) → ((voln*‘𝑋)‘(𝐶𝑛)) = 0)
11599, 101, 102, 110, 114sge0ss 39105 . . . . 5 (𝜑 → (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
116115eqcomd 2611 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))))
11781, 6eqsstrd 3597 . . . . . 6 (𝜑 → (𝐶‘1) ⊆ (ℝ ↑𝑚 𝑋))
1181, 117ovncl 39257 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘1)) ∈ (0[,]+∞))
11993, 18eqsstrd 3597 . . . . . 6 (𝜑 → (𝐶‘2) ⊆ (ℝ ↑𝑚 𝑋))
1201, 119ovncl 39257 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘2)) ∈ (0[,]+∞))
12174fveq2d 6088 . . . . 5 (𝑛 = 1 → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘(𝐶‘1)))
12275fveq2d 6088 . . . . 5 (𝑛 = 2 → ((voln*‘𝑋)‘(𝐶𝑛)) = ((voln*‘𝑋)‘(𝐶‘2)))
12383a1i 11 . . . . 5 (𝜑 → 1 ≠ 2)
12480, 92, 118, 120, 121, 122, 123sge0pr 39087 . . . 4 (𝜑 → (Σ^‘(𝑛 ∈ {1, 2} ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (((voln*‘𝑋)‘(𝐶‘1)) +𝑒 ((voln*‘𝑋)‘(𝐶‘2))))
12581fveq2d 6088 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘1)) = ((voln*‘𝑋)‘𝐴))
12693fveq2d 6088 . . . . 5 (𝜑 → ((voln*‘𝑋)‘(𝐶‘2)) = ((voln*‘𝑋)‘𝐵))
127125, 126oveq12d 6541 . . . 4 (𝜑 → (((voln*‘𝑋)‘(𝐶‘1)) +𝑒 ((voln*‘𝑋)‘(𝐶‘2))) = (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
128116, 124, 1273eqtrd 2643 . . 3 (𝜑 → (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) = (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
12998, 128breq12d 4586 . 2 (𝜑 → (((voln*‘𝑋)‘ 𝑛 ∈ ℕ (𝐶𝑛)) ≤ (Σ^‘(𝑛 ∈ ℕ ↦ ((voln*‘𝑋)‘(𝐶𝑛)))) ↔ ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵))))
13037, 129mpbid 220 1 (𝜑 → ((voln*‘𝑋)‘(𝐴𝐵)) ≤ (((voln*‘𝑋)‘𝐴) +𝑒 ((voln*‘𝑋)‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1474  wcel 1975  wne 2775  wral 2891  Vcvv 3168  cdif 3532  cun 3533  wss 3535  c0 3869  ifcif 4031  𝒫 cpw 4103  {cpr 4122   ciun 4445   class class class wbr 4573  cmpt 4633  cfv 5786  (class class class)co 6523  𝑚 cmap 7717  Fincfn 7814  cr 9787  0cc0 9788  1c1 9789  cle 9927  cn 10863  2c2 10913   +𝑒 cxad 11772  Σ^csumge0 39055  voln*covoln 39226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cc 9113  ax-ac2 9141  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866  ax-addf 9867  ax-mulf 9868
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 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-disj 4544  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-om 6931  df-1st 7032  df-2nd 7033  df-tpos 7212  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-ixp 7768  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-fi 8173  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-acn 8624  df-ac 8795  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-4 10924  df-5 10925  df-6 10926  df-7 10927  df-8 10928  df-9 10929  df-n0 11136  df-z 11207  df-dec 11322  df-uz 11516  df-q 11617  df-rp 11661  df-xneg 11774  df-xadd 11775  df-xmul 11776  df-ioo 12002  df-ico 12004  df-icc 12005  df-fz 12149  df-fzo 12286  df-fl 12406  df-seq 12615  df-exp 12674  df-hash 12931  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-clim 14009  df-rlim 14010  df-sum 14207  df-prod 14417  df-struct 15639  df-ndx 15640  df-slot 15641  df-base 15642  df-sets 15643  df-ress 15644  df-plusg 15723  df-mulr 15724  df-starv 15725  df-tset 15729  df-ple 15730  df-ds 15733  df-unif 15734  df-rest 15848  df-0g 15867  df-topgen 15869  df-mgm 17007  df-sgrp 17049  df-mnd 17060  df-grp 17190  df-minusg 17191  df-subg 17356  df-cmn 17960  df-abl 17961  df-mgp 18255  df-ur 18267  df-ring 18314  df-cring 18315  df-oppr 18388  df-dvdsr 18406  df-unit 18407  df-invr 18437  df-dvr 18448  df-drng 18514  df-psmet 19501  df-xmet 19502  df-met 19503  df-bl 19504  df-mopn 19505  df-cnfld 19510  df-top 20459  df-bases 20460  df-topon 20461  df-cmp 20938  df-ovol 22953  df-vol 22954  df-sumge0 39056  df-ovoln 39227
This theorem is referenced by:  ovnsubadd2  39336
  Copyright terms: Public domain W3C validator