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

Theorem omeiunltfirp 44446
Description: If the outer measure of a countable union is not +∞, then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
omeiunltfirp.o (𝜑𝑂 ∈ OutMeas)
omeiunltfirp.x 𝑋 = dom 𝑂
omeiunltfirp.z 𝑍 = (ℤ𝑁)
omeiunltfirp.e (𝜑𝐸:𝑍⟶𝒫 𝑋)
omeiunltfirp.re (𝜑 → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ)
omeiunltfirp.y (𝜑𝑌 ∈ ℝ+)
Assertion
Ref Expression
omeiunltfirp (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
Distinct variable groups:   𝑛,𝐸,𝑧   𝑛,𝑂,𝑧   𝑛,𝑋   𝑧,𝑌   𝑛,𝑍,𝑧   𝜑,𝑛,𝑧
Allowed substitution hints:   𝑁(𝑧,𝑛)   𝑋(𝑧)   𝑌(𝑛)

Proof of Theorem omeiunltfirp
Dummy variables 𝑘 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omeiunltfirp.z . . . . . 6 𝑍 = (ℤ𝑁)
21fvexi 6848 . . . . 5 𝑍 ∈ V
32a1i 11 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → 𝑍 ∈ V)
4 omeiunltfirp.o . . . . . . . 8 (𝜑𝑂 ∈ OutMeas)
54adantr 482 . . . . . . 7 ((𝜑𝑛𝑍) → 𝑂 ∈ OutMeas)
6 omeiunltfirp.x . . . . . . 7 𝑋 = dom 𝑂
7 omeiunltfirp.e . . . . . . . . 9 (𝜑𝐸:𝑍⟶𝒫 𝑋)
87ffvelcdmda 7026 . . . . . . . 8 ((𝜑𝑛𝑍) → (𝐸𝑛) ∈ 𝒫 𝑋)
9 fvex 6847 . . . . . . . . 9 (𝐸𝑛) ∈ V
109elpw 4559 . . . . . . . 8 ((𝐸𝑛) ∈ 𝒫 𝑋 ↔ (𝐸𝑛) ⊆ 𝑋)
118, 10sylib 217 . . . . . . 7 ((𝜑𝑛𝑍) → (𝐸𝑛) ⊆ 𝑋)
125, 6, 11omecl 44430 . . . . . 6 ((𝜑𝑛𝑍) → (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞))
13 eqid 2737 . . . . . 6 (𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) = (𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))
1412, 13fmptd 7053 . . . . 5 (𝜑 → (𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))):𝑍⟶(0[,]+∞))
1514adantr 482 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → (𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))):𝑍⟶(0[,]+∞))
16 simpr 486 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞)
17 omeiunltfirp.re . . . . 5 (𝜑 → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ)
1817adantr 482 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ)
193, 15, 16, 18sge0pnffigt 44323 . . 3 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)))
20 simpl 484 . . . . . . 7 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)))
21 simpr 486 . . . . . . . . 9 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)))
22 elpwinss 42969 . . . . . . . . . . . 12 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧𝑍)
2322resmptd 5987 . . . . . . . . . . 11 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → ((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧) = (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))
2423fveq2d 6838 . . . . . . . . . 10 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)) = (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))))
2524adantr 482 . . . . . . . . 9 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)) = (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))))
2621, 25breqtrd 5126 . . . . . . . 8 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))))
2726adantll 712 . . . . . . 7 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))))
2817rexrd 11135 . . . . . . . . 9 (𝜑 → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ*)
2928ad2antrr 724 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ*)
30 simpr 486 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ (𝒫 𝑍 ∩ Fin))
314ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 𝑂 ∈ OutMeas)
327ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 𝐸:𝑍⟶𝒫 𝑋)
3322adantr 482 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑧𝑍)
34 simpr 486 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑛𝑧)
3533, 34sseldd 3940 . . . . . . . . . . . . . . 15 ((𝑧 ∈ (𝒫 𝑍 ∩ Fin) ∧ 𝑛𝑧) → 𝑛𝑍)
3635adantll 712 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 𝑛𝑍)
3732, 36ffvelcdmd 7027 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝐸𝑛) ∈ 𝒫 𝑋)
3837, 10sylib 217 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝐸𝑛) ⊆ 𝑋)
3931, 6, 38omecl 44430 . . . . . . . . . . 11 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞))
40 eqid 2737 . . . . . . . . . . 11 (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))) = (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))
4139, 40fmptd 7053 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))):𝑧⟶(0[,]+∞))
4230, 41sge0xrcl 44312 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ*)
4342adantr 482 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ*)
44 elinel2 4151 . . . . . . . . . . . . 13 (𝑧 ∈ (𝒫 𝑍 ∩ Fin) → 𝑧 ∈ Fin)
4544adantl 483 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ Fin)
46 rge0ssre 13298 . . . . . . . . . . . . 13 (0[,)+∞) ⊆ ℝ
47 0xr 11132 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
4847a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 0 ∈ ℝ*)
49 pnfxr 11139 . . . . . . . . . . . . . . 15 +∞ ∈ ℝ*
5049a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → +∞ ∈ ℝ*)
5131, 6, 38omexrcl 44434 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ∈ ℝ*)
52 iccgelb 13245 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞)) → 0 ≤ (𝑂‘(𝐸𝑛)))
5348, 50, 39, 52syl3anc 1371 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 0 ≤ (𝑂‘(𝐸𝑛)))
5411ralrimiva 3141 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑛𝑍 (𝐸𝑛) ⊆ 𝑋)
55 iunss 5000 . . . . . . . . . . . . . . . . . 18 ( 𝑛𝑍 (𝐸𝑛) ⊆ 𝑋 ↔ ∀𝑛𝑍 (𝐸𝑛) ⊆ 𝑋)
5654, 55sylibr 233 . . . . . . . . . . . . . . . . 17 (𝜑 𝑛𝑍 (𝐸𝑛) ⊆ 𝑋)
5756ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → 𝑛𝑍 (𝐸𝑛) ⊆ 𝑋)
5831, 6, 57omexrcl 44434 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ*)
59 ssiun2 5002 . . . . . . . . . . . . . . . . 17 (𝑛𝑍 → (𝐸𝑛) ⊆ 𝑛𝑍 (𝐸𝑛))
6036, 59syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝐸𝑛) ⊆ 𝑛𝑍 (𝐸𝑛))
6131, 6, 57, 60omessle 44425 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ≤ (𝑂 𝑛𝑍 (𝐸𝑛)))
6217ltpnfd 12967 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑂 𝑛𝑍 (𝐸𝑛)) < +∞)
6362ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂 𝑛𝑍 (𝐸𝑛)) < +∞)
6451, 58, 50, 61, 63xrlelttrd 13004 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) < +∞)
6548, 50, 51, 53, 64elicod 13239 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ∈ (0[,)+∞))
6646, 65sselid 3937 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ∈ ℝ)
6745, 66fsumrecl 15550 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) ∈ ℝ)
68 omeiunltfirp.y . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℝ+)
6968rpred 12882 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7069adantr 482 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑌 ∈ ℝ)
7167, 70readdcld 11114 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌) ∈ ℝ)
7271rexrd 11135 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌) ∈ ℝ*)
7372adantr 482 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌) ∈ ℝ*)
74 simpr 486 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))))
7565, 40fmptd 7053 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))):𝑧⟶(0[,)+∞))
7645, 75sge0fsum 44314 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) = Σ𝑘𝑧 ((𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))‘𝑘))
77 eqidd 2738 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑧) → (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))) = (𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))
78 2fveq3 6839 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝑂‘(𝐸𝑛)) = (𝑂‘(𝐸𝑘)))
7978adantl 483 . . . . . . . . . . . . 13 ((((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑧) ∧ 𝑛 = 𝑘) → (𝑂‘(𝐸𝑛)) = (𝑂‘(𝐸𝑘)))
80 simpr 486 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑧) → 𝑘𝑧)
81 fvexd 6849 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑧) → (𝑂‘(𝐸𝑘)) ∈ V)
8277, 79, 80, 81fvmptd 6947 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑘𝑧) → ((𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))‘𝑘) = (𝑂‘(𝐸𝑘)))
8382sumeq2dv 15519 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘𝑧 ((𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))‘𝑘) = Σ𝑘𝑧 (𝑂‘(𝐸𝑘)))
84 2fveq3 6839 . . . . . . . . . . . . 13 (𝑘 = 𝑛 → (𝑂‘(𝐸𝑘)) = (𝑂‘(𝐸𝑛)))
8584cbvsumv 15512 . . . . . . . . . . . 12 Σ𝑘𝑧 (𝑂‘(𝐸𝑘)) = Σ𝑛𝑧 (𝑂‘(𝐸𝑛))
8685a1i 11 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑘𝑧 (𝑂‘(𝐸𝑘)) = Σ𝑛𝑧 (𝑂‘(𝐸𝑛)))
8776, 83, 863eqtrd 2781 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) = Σ𝑛𝑧 (𝑂‘(𝐸𝑛)))
8868adantr 482 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑌 ∈ ℝ+)
8967, 88ltaddrpd 12915 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
9087, 89eqbrtrd 5122 . . . . . . . . 9 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
9190adantr 482 . . . . . . . 8 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
9229, 43, 73, 74, 91xrlttrd 13003 . . . . . . 7 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛))))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
9320, 27, 92syl2anc 585 . . . . . 6 (((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧))) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
9493ex 414 . . . . 5 ((𝜑𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌)))
9594adantlr 713 . . . 4 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌)))
9695reximdva 3163 . . 3 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ^‘((𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) ↾ 𝑧)) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌)))
9719, 96mpd 15 . 2 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
98 simpl 484 . . 3 ((𝜑 ∧ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → 𝜑)
99 simpr 486 . . . 4 ((𝜑 ∧ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞)
1002a1i 11 . . . . . 6 (𝜑𝑍 ∈ V)
101100, 14sge0repnf 44313 . . . . 5 (𝜑 → ((Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ ↔ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞))
102101adantr 482 . . . 4 ((𝜑 ∧ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → ((Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ ↔ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞))
10399, 102mpbird 257 . . 3 ((𝜑 ∧ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ)
104 nfv 1917 . . . . . 6 𝑛𝜑
105 nfcv 2905 . . . . . . . 8 𝑛Σ^
106 nfmpt1 5208 . . . . . . . 8 𝑛(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))
107105, 106nffv 6844 . . . . . . 7 𝑛^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))))
108 nfcv 2905 . . . . . . 7 𝑛
109107, 108nfel 2919 . . . . . 6 𝑛^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ
110104, 109nfan 1902 . . . . 5 𝑛(𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ)
1112a1i 11 . . . . 5 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → 𝑍 ∈ V)
11212adantlr 713 . . . . 5 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑛𝑍) → (𝑂‘(𝐸𝑛)) ∈ (0[,]+∞))
11368adantr 482 . . . . 5 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → 𝑌 ∈ ℝ+)
114 simpr 486 . . . . 5 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ)
115110, 111, 112, 113, 114sge0ltfirpmpt 44335 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌))
11617ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (𝑂 𝑛𝑍 (𝐸𝑛)) ∈ ℝ)
117114ad2antrr 724 . . . . . . 7 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ)
11871ad4ant13 749 . . . . . . 7 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌) ∈ ℝ)
119 nfcv 2905 . . . . . . . . 9 𝑛𝐸
120104, 119, 4, 6, 1, 7omeiunle 44444 . . . . . . . 8 (𝜑 → (𝑂 𝑛𝑍 (𝐸𝑛)) ≤ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))))
121120ad3antrrr 728 . . . . . . 7 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (𝑂 𝑛𝑍 (𝐸𝑛)) ≤ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))))
122 simpr 486 . . . . . . . 8 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌))
123 simpll 765 . . . . . . . . . . 11 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝜑)
124 2fveq3 6839 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → (𝑂‘(𝐸𝑛)) = (𝑂‘(𝐸𝑚)))
125124cbvmptv 5213 . . . . . . . . . . . . . . 15 (𝑛𝑍 ↦ (𝑂‘(𝐸𝑛))) = (𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))
126125fveq2i 6837 . . . . . . . . . . . . . 14 ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚))))
127126eleq1i 2828 . . . . . . . . . . . . 13 ((Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ ↔ (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ)
128127biimpi 215 . . . . . . . . . . . 12 ((Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ → (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ)
129128ad2antlr 725 . . . . . . . . . . 11 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ)
130 simpr 486 . . . . . . . . . . 11 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ (𝒫 𝑍 ∩ Fin))
13144adantl 483 . . . . . . . . . . . 12 (((𝜑 ∧ (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → 𝑧 ∈ Fin)
13265adantllr 717 . . . . . . . . . . . 12 ((((𝜑 ∧ (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ 𝑛𝑧) → (𝑂‘(𝐸𝑛)) ∈ (0[,)+∞))
133131, 132sge0fsummpt 44317 . . . . . . . . . . 11 (((𝜑 ∧ (Σ^‘(𝑚𝑍 ↦ (𝑂‘(𝐸𝑚)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) = Σ𝑛𝑧 (𝑂‘(𝐸𝑛)))
134123, 129, 130, 133syl21anc 836 . . . . . . . . . 10 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → (Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) = Σ𝑛𝑧 (𝑂‘(𝐸𝑛)))
135134oveq1d 7361 . . . . . . . . 9 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌) = (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
136135adantr 482 . . . . . . . 8 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌) = (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
137122, 136breqtrd 5126 . . . . . . 7 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
138116, 117, 118, 121, 137lelttrd 11243 . . . . . 6 ((((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌)) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
139138ex 414 . . . . 5 (((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) ∧ 𝑧 ∈ (𝒫 𝑍 ∩ Fin)) → ((Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌) → (𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌)))
140139reximdva 3163 . . . 4 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → (∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) < ((Σ^‘(𝑛𝑧 ↦ (𝑂‘(𝐸𝑛)))) + 𝑌) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌)))
141115, 140mpd 15 . . 3 ((𝜑 ∧ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
14298, 103, 141syl2anc 585 . 2 ((𝜑 ∧ ¬ (Σ^‘(𝑛𝑍 ↦ (𝑂‘(𝐸𝑛)))) = +∞) → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
14397, 142pm2.61dan 811 1 (𝜑 → ∃𝑧 ∈ (𝒫 𝑍 ∩ Fin)(𝑂 𝑛𝑍 (𝐸𝑛)) < (Σ𝑛𝑧 (𝑂‘(𝐸𝑛)) + 𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wral 3062  wrex 3071  Vcvv 3443  cin 3904  wss 3905  𝒫 cpw 4555   cuni 4860   ciun 4949   class class class wbr 5100  cmpt 5183  dom cdm 5627  cres 5629  wf 6484  cfv 6488  (class class class)co 7346  Fincfn 8813  cr 10980  0cc0 10981   + caddc 10984  +∞cpnf 11116  *cxr 11118   < clt 11119  cle 11120  cuz 12692  +crp 12840  [,)cico 13191  [,]cicc 13192  Σcsu 15501  Σ^csumge0 44289  OutMeascome 44416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5237  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-inf2 9507  ax-ac2 10329  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058  ax-pre-sup 11059
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-se 5583  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7790  df-1st 7908  df-2nd 7909  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-1o 8376  df-oadd 8380  df-omul 8381  df-er 8578  df-map 8697  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-sup 9308  df-oi 9376  df-card 9805  df-acn 9808  df-ac 9982  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-div 11743  df-nn 12084  df-2 12146  df-3 12147  df-n0 12344  df-z 12430  df-uz 12693  df-rp 12841  df-ico 13195  df-icc 13196  df-fz 13350  df-fzo 13493  df-seq 13832  df-exp 13893  df-hash 14155  df-cj 14914  df-re 14915  df-im 14916  df-sqrt 15050  df-abs 15051  df-clim 15301  df-sum 15502  df-sumge0 44290  df-ome 44417
This theorem is referenced by:  carageniuncllem2  44449
  Copyright terms: Public domain W3C validator