Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  voliune Structured version   Visualization version   GIF version

Theorem voliune 29445
Description: The Lebesgue measure function is countably additive. This formulation on the extended reals, allows for +∞ for the measure of any set in the sum. Cf. ovoliun 22982 and voliun 23032. (Contributed by Thierry Arnoux, 16-Oct-2017.)
Assertion
Ref Expression
voliune ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))

Proof of Theorem voliune
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 r19.26 2950 . . . . 5 (∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ↔ (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ))
2 eqid 2514 . . . . . 6 seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))) = seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴)))
3 eqid 2514 . . . . . 6 (𝑛 ∈ ℕ ↦ (vol‘𝐴)) = (𝑛 ∈ ℕ ↦ (vol‘𝐴))
42, 3voliun 23032 . . . . 5 ((∀𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
51, 4sylanbr 488 . . . 4 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
65an32s 841 . . 3 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → (vol‘ 𝑛 ∈ ℕ 𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
7 nfra1 2829 . . . . . . 7 𝑛𝑛 ∈ ℕ 𝐴 ∈ dom vol
8 nfra1 2829 . . . . . . 7 𝑛𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ
97, 8nfan 2059 . . . . . 6 𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)
10 simpr 475 . . . . . . . . . 10 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
11 rspa 2818 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ dom vol)
12 volf 23007 . . . . . . . . . . . 12 vol:dom vol⟶(0[,]+∞)
1312ffvelrni 6149 . . . . . . . . . . 11 (𝐴 ∈ dom vol → (vol‘𝐴) ∈ (0[,]+∞))
1411, 13syl 17 . . . . . . . . . 10 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞))
153fvmpt2 6083 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (vol‘𝐴) ∈ (0[,]+∞)) → ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))
1610, 14, 15syl2anc 690 . . . . . . . . 9 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))
1716adantlr 746 . . . . . . . 8 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))
1817ex 448 . . . . . . 7 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → (𝑛 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴)))
199, 18ralrimi 2844 . . . . . 6 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = (vol‘𝐴))
209, 19esumeq2d 29252 . . . . 5 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
21 simpr 475 . . . . . . . . 9 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)
2221r19.21bi 2820 . . . . . . . 8 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) ∈ ℝ)
2314adantlr 746 . . . . . . . . 9 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞))
24 0xr 9839 . . . . . . . . . . 11 0 ∈ ℝ*
25 pnfxr 11687 . . . . . . . . . . 11 +∞ ∈ ℝ*
26 elicc1 11956 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((vol‘𝐴) ∈ (0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤ (vol‘𝐴) ∧ (vol‘𝐴) ≤ +∞)))
2724, 25, 26mp2an 703 . . . . . . . . . 10 ((vol‘𝐴) ∈ (0[,]+∞) ↔ ((vol‘𝐴) ∈ ℝ* ∧ 0 ≤ (vol‘𝐴) ∧ (vol‘𝐴) ≤ +∞))
2827simp2bi 1069 . . . . . . . . 9 ((vol‘𝐴) ∈ (0[,]+∞) → 0 ≤ (vol‘𝐴))
2923, 28syl 17 . . . . . . . 8 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → 0 ≤ (vol‘𝐴))
30 ltpnf 11697 . . . . . . . . 9 ((vol‘𝐴) ∈ ℝ → (vol‘𝐴) < +∞)
3122, 30syl 17 . . . . . . . 8 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) < +∞)
32 0re 9793 . . . . . . . . 9 0 ∈ ℝ
33 elico2 11974 . . . . . . . . 9 ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) → ((vol‘𝐴) ∈ (0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤ (vol‘𝐴) ∧ (vol‘𝐴) < +∞)))
3432, 25, 33mp2an 703 . . . . . . . 8 ((vol‘𝐴) ∈ (0[,)+∞) ↔ ((vol‘𝐴) ∈ ℝ ∧ 0 ≤ (vol‘𝐴) ∧ (vol‘𝐴) < +∞))
3522, 29, 31, 34syl3anbrc 1238 . . . . . . 7 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) ∈ (0[,)+∞))
369, 35, 3fmptdf 6177 . . . . . 6 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → (𝑛 ∈ ℕ ↦ (vol‘𝐴)):ℕ⟶(0[,)+∞))
37 nfmpt1 4573 . . . . . . 7 𝑛(𝑛 ∈ ℕ ↦ (vol‘𝐴))
3837esumfsupre 29286 . . . . . 6 ((𝑛 ∈ ℕ ↦ (vol‘𝐴)):ℕ⟶(0[,)+∞) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
3936, 38syl 17 . . . . 5 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → Σ*𝑛 ∈ ℕ((𝑛 ∈ ℕ ↦ (vol‘𝐴))‘𝑛) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
4020, 39eqtr3d 2550 . . . 4 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
4140adantlr 746 . . 3 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = sup(ran seq1( + , (𝑛 ∈ ℕ ↦ (vol‘𝐴))), ℝ*, < ))
426, 41eqtr4d 2551 . 2 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ) → (vol‘ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
43 simpr 475 . . . . . . . 8 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)
44 nfv 1796 . . . . . . . . 9 𝑘(vol‘𝐴) = +∞
45 nfcv 2655 . . . . . . . . . . 11 𝑛vol
46 nfcsb1v 3419 . . . . . . . . . . 11 𝑛𝑘 / 𝑛𝐴
4745, 46nffv 5993 . . . . . . . . . 10 𝑛(vol‘𝑘 / 𝑛𝐴)
4847nfeq1 2668 . . . . . . . . 9 𝑛(vol‘𝑘 / 𝑛𝐴) = +∞
49 csbeq1a 3412 . . . . . . . . . . 11 (𝑛 = 𝑘𝐴 = 𝑘 / 𝑛𝐴)
5049fveq2d 5990 . . . . . . . . . 10 (𝑛 = 𝑘 → (vol‘𝐴) = (vol‘𝑘 / 𝑛𝐴))
5150eqeq1d 2516 . . . . . . . . 9 (𝑛 = 𝑘 → ((vol‘𝐴) = +∞ ↔ (vol‘𝑘 / 𝑛𝐴) = +∞))
5244, 48, 51cbvrex 3048 . . . . . . . 8 (∃𝑛 ∈ ℕ (vol‘𝐴) = +∞ ↔ ∃𝑘 ∈ ℕ (vol‘𝑘 / 𝑛𝐴) = +∞)
5343, 52sylib 206 . . . . . . 7 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ∃𝑘 ∈ ℕ (vol‘𝑘 / 𝑛𝐴) = +∞)
5446nfel1 2669 . . . . . . . . . . . . 13 𝑛𝑘 / 𝑛𝐴 ∈ dom vol
5549eleq1d 2576 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝐴 ∈ dom vol ↔ 𝑘 / 𝑛𝐴 ∈ dom vol))
5654, 55rspc 3180 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → 𝑘 / 𝑛𝐴 ∈ dom vol))
5756impcom 444 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 ∈ dom vol)
58 iunmbl 23031 . . . . . . . . . . . 12 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → 𝑛 ∈ ℕ 𝐴 ∈ dom vol)
5958adantr 479 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ) → 𝑛 ∈ ℕ 𝐴 ∈ dom vol)
60 nfcv 2655 . . . . . . . . . . . . 13 𝑛
61 nfcv 2655 . . . . . . . . . . . . 13 𝑛𝑘
6260, 61, 46, 49ssiun2sf 28578 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 / 𝑛𝐴 𝑛 ∈ ℕ 𝐴)
6362adantl 480 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ) → 𝑘 / 𝑛𝐴 𝑛 ∈ ℕ 𝐴)
64 volss 23011 . . . . . . . . . . 11 ((𝑘 / 𝑛𝐴 ∈ dom vol ∧ 𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 / 𝑛𝐴 𝑛 ∈ ℕ 𝐴) → (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
6557, 59, 63, 64syl3anc 1317 . . . . . . . . . 10 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ 𝑘 ∈ ℕ) → (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
6665adantlr 746 . . . . . . . . 9 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ 𝑘 ∈ ℕ) → (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
6766adantlr 746 . . . . . . . 8 ((((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) ∧ 𝑘 ∈ ℕ) → (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
6867ralrimiva 2853 . . . . . . 7 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ∀𝑘 ∈ ℕ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
69 r19.29r 2959 . . . . . . 7 ((∃𝑘 ∈ ℕ (vol‘𝑘 / 𝑛𝐴) = +∞ ∧ ∀𝑘 ∈ ℕ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ ((vol‘𝑘 / 𝑛𝐴) = +∞ ∧ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)))
7053, 68, 69syl2anc 690 . . . . . 6 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ∃𝑘 ∈ ℕ ((vol‘𝑘 / 𝑛𝐴) = +∞ ∧ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)))
71 breq1 4484 . . . . . . . 8 ((vol‘𝑘 / 𝑛𝐴) = +∞ → ((vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴) ↔ +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)))
7271biimpa 499 . . . . . . 7 (((vol‘𝑘 / 𝑛𝐴) = +∞ ∧ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)) → +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
7372reximi 2898 . . . . . 6 (∃𝑘 ∈ ℕ ((vol‘𝑘 / 𝑛𝐴) = +∞ ∧ (vol‘𝑘 / 𝑛𝐴) ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)) → ∃𝑘 ∈ ℕ +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
7470, 73syl 17 . . . . 5 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ∃𝑘 ∈ ℕ +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
75 1nn 10784 . . . . . 6 1 ∈ ℕ
76 ne0i 3783 . . . . . 6 (1 ∈ ℕ → ℕ ≠ ∅)
77 r19.9rzv 3920 . . . . . 6 (ℕ ≠ ∅ → (+∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴)))
7875, 76, 77mp2b 10 . . . . 5 (+∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴) ↔ ∃𝑘 ∈ ℕ +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
7974, 78sylibr 222 . . . 4 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → +∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴))
80 iccssxr 11993 . . . . . . . 8 (0[,]+∞) ⊆ ℝ*
8112ffvelrni 6149 . . . . . . . 8 ( 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘ 𝑛 ∈ ℕ 𝐴) ∈ (0[,]+∞))
8280, 81sseldi 3470 . . . . . . 7 ( 𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ*)
8358, 82syl 17 . . . . . 6 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → (vol‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ*)
8483ad2antrr 757 . . . . 5 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → (vol‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ*)
85 xgepnf 28722 . . . . 5 ((vol‘ 𝑛 ∈ ℕ 𝐴) ∈ ℝ* → (+∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘ 𝑛 ∈ ℕ 𝐴) = +∞))
8684, 85syl 17 . . . 4 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → (+∞ ≤ (vol‘ 𝑛 ∈ ℕ 𝐴) ↔ (vol‘ 𝑛 ∈ ℕ 𝐴) = +∞))
8779, 86mpbid 220 . . 3 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → (vol‘ 𝑛 ∈ ℕ 𝐴) = +∞)
88 nfdisj1 4464 . . . . . 6 𝑛Disj 𝑛 ∈ ℕ 𝐴
897, 88nfan 2059 . . . . 5 𝑛(∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴)
90 nfre1 2892 . . . . 5 𝑛𝑛 ∈ ℕ (vol‘𝐴) = +∞
9189, 90nfan 2059 . . . 4 𝑛((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)
92 nnex 10779 . . . . 5 ℕ ∈ V
9392a1i 11 . . . 4 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → ℕ ∈ V)
94143ad2antr3 1220 . . . . 5 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ (Disj 𝑛 ∈ ℕ 𝐴 ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞ ∧ 𝑛 ∈ ℕ)) → (vol‘𝐴) ∈ (0[,]+∞))
95943anassrs 1281 . . . 4 ((((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) ∧ 𝑛 ∈ ℕ) → (vol‘𝐴) ∈ (0[,]+∞))
9691, 93, 95, 43esumpinfval 29288 . . 3 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → Σ*𝑛 ∈ ℕ(vol‘𝐴) = +∞)
9787, 96eqtr4d 2551 . 2 (((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) ∧ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞) → (vol‘ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
98 exmid 429 . . . . 5 (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)
99 rexnal 2882 . . . . . 6 (∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ ↔ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ)
10099orbi2i 539 . . . . 5 ((∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) ↔ (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ¬ ∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ))
10198, 100mpbir 219 . . . 4 (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ)
102 r19.29 2958 . . . . . . 7 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) → ∃𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈ ℝ))
103 xrge0nre 12014 . . . . . . . . 9 (((vol‘𝐴) ∈ (0[,]+∞) ∧ ¬ (vol‘𝐴) ∈ ℝ) → (vol‘𝐴) = +∞)
10413, 103sylan 486 . . . . . . . 8 ((𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈ ℝ) → (vol‘𝐴) = +∞)
105104reximi 2898 . . . . . . 7 (∃𝑛 ∈ ℕ (𝐴 ∈ dom vol ∧ ¬ (vol‘𝐴) ∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)
106102, 105syl 17 . . . . . 6 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)
107106ex 448 . . . . 5 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → (∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ → ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞))
108107orim2d 880 . . . 4 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → ((∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ ¬ (vol‘𝐴) ∈ ℝ) → (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞)))
109101, 108mpi 20 . . 3 (∀𝑛 ∈ ℕ 𝐴 ∈ dom vol → (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞))
110109adantr 479 . 2 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (∀𝑛 ∈ ℕ (vol‘𝐴) ∈ ℝ ∨ ∃𝑛 ∈ ℕ (vol‘𝐴) = +∞))
11142, 97, 110mpjaodan 822 1 ((∀𝑛 ∈ ℕ 𝐴 ∈ dom vol ∧ Disj 𝑛 ∈ ℕ 𝐴) → (vol‘ 𝑛 ∈ ℕ 𝐴) = Σ*𝑛 ∈ ℕ(vol‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684  wral 2800  wrex 2801  Vcvv 3077  csb 3403  wss 3444  c0 3777   ciun 4353  Disj wdisj 4451   class class class wbr 4481  cmpt 4541  dom cdm 4932  ran crn 4933  wf 5685  cfv 5689  (class class class)co 6425  supcsup 8103  cr 9688  0cc0 9689  1c1 9690   + caddc 9692  +∞cpnf 9824  *cxr 9826   < clt 9827  cle 9828  cn 10773  [,)cico 11914  [,]cicc 11915  seqcseq 12528  volcvol 22939  Σ*cesum 29242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721  ax-inf2 8295  ax-cc 9014  ax-cnex 9745  ax-resscn 9746  ax-1cn 9747  ax-icn 9748  ax-addcl 9749  ax-addrcl 9750  ax-mulcl 9751  ax-mulrcl 9752  ax-mulcom 9753  ax-addass 9754  ax-mulass 9755  ax-distr 9756  ax-i2m1 9757  ax-1ne0 9758  ax-1rid 9759  ax-rnegex 9760  ax-rrecex 9761  ax-cnre 9762  ax-pre-lttri 9763  ax-pre-lttrn 9764  ax-pre-ltadd 9765  ax-pre-mulgt0 9766  ax-pre-sup 9767  ax-addf 9768  ax-mulf 9769
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 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-disj 4452  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-of 6669  df-om 6832  df-1st 6932  df-2nd 6933  df-supp 7056  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-1o 7321  df-2o 7322  df-oadd 7325  df-er 7503  df-map 7620  df-pm 7621  df-ixp 7669  df-en 7716  df-dom 7717  df-sdom 7718  df-fin 7719  df-fsupp 8033  df-fi 8074  df-sup 8105  df-inf 8106  df-oi 8172  df-card 8522  df-cda 8747  df-pnf 9829  df-mnf 9830  df-xr 9831  df-ltxr 9832  df-le 9833  df-sub 10017  df-neg 10018  df-div 10432  df-nn 10774  df-2 10832  df-3 10833  df-4 10834  df-5 10835  df-6 10836  df-7 10837  df-8 10838  df-9 10839  df-10OLD 10840  df-n0 11046  df-z 11117  df-dec 11232  df-uz 11424  df-q 11527  df-rp 11571  df-xneg 11684  df-xadd 11685  df-xmul 11686  df-ioo 11916  df-ioc 11917  df-ico 11918  df-icc 11919  df-fz 12063  df-fzo 12200  df-fl 12320  df-mod 12396  df-seq 12529  df-exp 12588  df-fac 12788  df-bc 12817  df-hash 12845  df-shft 13510  df-cj 13542  df-re 13543  df-im 13544  df-sqrt 13678  df-abs 13679  df-limsup 13906  df-clim 13929  df-rlim 13930  df-sum 14130  df-ef 14503  df-sin 14505  df-cos 14506  df-pi 14508  df-struct 15602  df-ndx 15603  df-slot 15604  df-base 15605  df-sets 15606  df-ress 15607  df-plusg 15686  df-mulr 15687  df-starv 15688  df-sca 15689  df-vsca 15690  df-ip 15691  df-tset 15692  df-ple 15693  df-ds 15696  df-unif 15697  df-hom 15698  df-cco 15699  df-rest 15811  df-topn 15812  df-0g 15830  df-gsum 15831  df-topgen 15832  df-pt 15833  df-prds 15836  df-ordt 15889  df-xrs 15890  df-qtop 15896  df-imas 15897  df-xps 15900  df-mre 15982  df-mrc 15983  df-acs 15985  df-ps 16936  df-tsr 16937  df-plusf 16977  df-mgm 16978  df-sgrp 17020  df-mnd 17031  df-mhm 17071  df-submnd 17072  df-grp 17161  df-minusg 17162  df-sbg 17163  df-mulg 17277  df-subg 17327  df-cntz 17486  df-cmn 17947  df-abl 17948  df-mgp 18241  df-ur 18253  df-ring 18300  df-cring 18301  df-subrg 18529  df-abv 18568  df-lmod 18616  df-scaf 18617  df-sra 18918  df-rgmod 18919  df-psmet 19484  df-xmet 19485  df-met 19486  df-bl 19487  df-mopn 19488  df-fbas 19489  df-fg 19490  df-cnfld 19493  df-top 20445  df-bases 20446  df-topon 20447  df-topsp 20448  df-cld 20557  df-ntr 20558  df-cls 20559  df-nei 20636  df-lp 20674  df-perf 20675  df-cn 20765  df-cnp 20766  df-haus 20853  df-tx 21099  df-hmeo 21292  df-fil 21384  df-fm 21476  df-flim 21477  df-flf 21478  df-tmd 21610  df-tgp 21611  df-tsms 21664  df-trg 21697  df-xms 21858  df-ms 21859  df-tms 21860  df-nm 22120  df-ngp 22121  df-nrg 22123  df-nlm 22124  df-ii 22432  df-cncf 22433  df-ovol 22940  df-vol 22942  df-limc 23339  df-dv 23340  df-log 24024  df-esum 29243
This theorem is referenced by:  volmeas  29447
  Copyright terms: Public domain W3C validator