omeiunltfirp

Description: If the outer measure of a countable union is not +oo , then it can be arbitrarily approximated by finite sums of outer measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	omeiunltfirp.o	$⊢ φ \to O \in OutMeas$
	omeiunltfirp.x	$⊢ X = ⋃ dom O$
	omeiunltfirp.z	$⊢ Z = ℤ_{\geq N}$
	omeiunltfirp.e	$⊢ φ \to E : Z ⟶ 𝒫 X$
	omeiunltfirp.re	$⊢ φ \to O (⋃_{n \in Z} E (n)) \in ℝ$
	omeiunltfirp.y	$⊢ φ \to Y \in ℝ^{+}$
Assertion	omeiunltfirp	$⊢ φ \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$

Proof

Step	Hyp	Ref	Expression
1		omeiunltfirp.o	$⊢ φ \to O \in OutMeas$
2		omeiunltfirp.x	$⊢ X = ⋃ dom O$
3		omeiunltfirp.z	$⊢ Z = ℤ_{\geq N}$
4		omeiunltfirp.e	$⊢ φ \to E : Z ⟶ 𝒫 X$
5		omeiunltfirp.re	$⊢ φ \to O (⋃_{n \in Z} E (n)) \in ℝ$
6		omeiunltfirp.y	$⊢ φ \to Y \in ℝ^{+}$
7	3	fvexi	$⊢ Z \in V$
8	7	a1i	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to Z \in V$
9	1	adantr	$⊢ (φ \land n \in Z) \to O \in OutMeas$
10	4	ffvelcdmda	$⊢ (φ \land n \in Z) \to E (n) \in 𝒫 X$
11		fvex	$⊢ E (n) \in V$
12	11	elpw	$⊢ E (n) \in 𝒫 X \leftrightarrow E (n) \subseteq X$
13	10 12	sylib	$⊢ (φ \land n \in Z) \to E (n) \subseteq X$
14	9 2 13	omecl	$⊢ (φ \land n \in Z) \to O (E (n)) \in [0, +∞]$
15		eqid	$⊢ (n \in Z ⟼ O (E (n))) = (n \in Z ⟼ O (E (n)))$
16	14 15	fmptd	$⊢ φ \to (n \in Z ⟼ O (E (n))) : Z ⟶ [0, +∞]$
17	16	adantr	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to (n \in Z ⟼ O (E (n))) : Z ⟶ [0, +∞]$
18		simpr	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to sum^((n \in Z ⟼ O (E (n)))) = +∞$
19	5	adantr	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to O (⋃_{n \in Z} E (n)) \in ℝ$
20	8 17 18 19	sge0pnffigt	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})$
21		simpl	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to (φ \land z \in (𝒫 Z \cap Fin))$
22		simpr	$⊢ (z \in (𝒫 Z \cap Fin) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})$
23		elpwinss	$⊢ z \in (𝒫 Z \cap Fin) \to z \subseteq Z$
24	23	resmptd	$⊢ z \in (𝒫 Z \cap Fin) \to {(n \in Z ⟼ O (E (n))) ↾}_{z} = (n \in z ⟼ O (E (n)))$
25	24	fveq2d	$⊢ z \in (𝒫 Z \cap Fin) \to sum^({(n \in Z ⟼ O (E (n))) ↾}_{z}) = sum^((n \in z ⟼ O (E (n))))$
26	25	adantr	$⊢ (z \in (𝒫 Z \cap Fin) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to sum^({(n \in Z ⟼ O (E (n))) ↾}_{z}) = sum^((n \in z ⟼ O (E (n))))$
27	22 26	breqtrd	$⊢ (z \in (𝒫 Z \cap Fin) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))$
28	27	adantll	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))$
29	5	rexrd	$⊢ φ \to O (⋃_{n \in Z} E (n)) \in ℝ^{*}$
30	29	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to O (⋃_{n \in Z} E (n)) \in ℝ^{*}$
31		simpr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to z \in (𝒫 Z \cap Fin)$
32	1	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O \in OutMeas$
33	4	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to E : Z ⟶ 𝒫 X$
34	23	adantr	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to z \subseteq Z$
35		simpr	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to n \in z$
36	34 35	sseldd	$⊢ (z \in (𝒫 Z \cap Fin) \land n \in z) \to n \in Z$
37	36	adantll	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to n \in Z$
38	33 37	ffvelcdmd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to E (n) \in 𝒫 X$
39	38 12	sylib	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to E (n) \subseteq X$
40	32 2 39	omecl	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \in [0, +∞]$
41		eqid	$⊢ (n \in z ⟼ O (E (n))) = (n \in z ⟼ O (E (n)))$
42	40 41	fmptd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to (n \in z ⟼ O (E (n))) : z ⟶ [0, +∞]$
43	31 42	sge0xrcl	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) \in ℝ^{*}$
44	43	adantr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to sum^((n \in z ⟼ O (E (n)))) \in ℝ^{*}$
45		elinel2	$⊢ z \in (𝒫 Z \cap Fin) \to z \in Fin$
46	45	adantl	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to z \in Fin$
47		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
48		0xr	$⊢ 0 \in ℝ^{*}$
49	48	a1i	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to 0 \in ℝ^{*}$
50		pnfxr	$⊢ +∞ \in ℝ^{*}$
51	50	a1i	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to +∞ \in ℝ^{*}$
52	32 2 39	omexrcl	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \in ℝ^{*}$
53		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land O (E (n)) \in [0, +∞]) \to 0 \leq O (E (n))$
54	49 51 40 53	syl3anc	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to 0 \leq O (E (n))$
55	13	ralrimiva	$⊢ φ \to \forall n \in Z E (n) \subseteq X$
56		iunss	$⊢ ⋃_{n \in Z} E (n) \subseteq X \leftrightarrow \forall n \in Z E (n) \subseteq X$
57	55 56	sylibr	$⊢ φ \to ⋃_{n \in Z} E (n) \subseteq X$
58	57	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to ⋃_{n \in Z} E (n) \subseteq X$
59	32 2 58	omexrcl	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (⋃_{n \in Z} E (n)) \in ℝ^{*}$
60		ssiun2	$⊢ n \in Z \to E (n) \subseteq ⋃_{n \in Z} E (n)$
61	37 60	syl	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to E (n) \subseteq ⋃_{n \in Z} E (n)$
62	32 2 58 61	omessle	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \leq O (⋃_{n \in Z} E (n))$
63	5	ltpnfd	$⊢ φ \to O (⋃_{n \in Z} E (n)) < +∞$
64	63	ad2antrr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (⋃_{n \in Z} E (n)) < +∞$
65	52 59 51 62 64	xrlelttrd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) < +∞$
66	49 51 52 54 65	elicod	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \in [0, +∞)$
67	47 66	sselid	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \in ℝ$
68	46 67	fsumrecl	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O (E (n)) \in ℝ$
69	6	rpred	$⊢ φ \to Y \in ℝ$
70	69	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to Y \in ℝ$
71	68 70	readdcld	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O (E (n)) + Y \in ℝ$
72	71	rexrd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O (E (n)) + Y \in ℝ^{*}$
73	72	adantr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to \sum_{n \in z} O (E (n)) + Y \in ℝ^{*}$
74		simpr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))$
75	66 41	fmptd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to (n \in z ⟼ O (E (n))) : z ⟶ [0, +∞)$
76	46 75	sge0fsum	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) = \sum_{k \in z} (n \in z ⟼ O (E (n))) (k)$
77		eqidd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land k \in z) \to (n \in z ⟼ O (E (n))) = (n \in z ⟼ O (E (n)))$
78		2fveq3	$⊢ n = k \to O (E (n)) = O (E (k))$
79	78	adantl	$⊢ (((φ \land z \in (𝒫 Z \cap Fin)) \land k \in z) \land n = k) \to O (E (n)) = O (E (k))$
80		simpr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land k \in z) \to k \in z$
81		fvexd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land k \in z) \to O (E (k)) \in V$
82	77 79 80 81	fvmptd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land k \in z) \to (n \in z ⟼ O (E (n))) (k) = O (E (k))$
83	82	sumeq2dv	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{k \in z} (n \in z ⟼ O (E (n))) (k) = \sum_{k \in z} O (E (k))$
84		2fveq3	$⊢ k = n \to O (E (k)) = O (E (n))$
85	84	cbvsumv	$⊢ \sum_{k \in z} O (E (k)) = \sum_{n \in z} O (E (n))$
86	85	a1i	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{k \in z} O (E (k)) = \sum_{n \in z} O (E (n))$
87	76 83 86	3eqtrd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) = \sum_{n \in z} O (E (n))$
88	6	adantr	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to Y \in ℝ^{+}$
89	68 88	ltaddrpd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to \sum_{n \in z} O (E (n)) < \sum_{n \in z} O (E (n)) + Y$
90	87 89	eqbrtrd	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) < \sum_{n \in z} O (E (n)) + Y$
91	90	adantr	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to sum^((n \in z ⟼ O (E (n)))) < \sum_{n \in z} O (E (n)) + Y$
92	30 44 73 74 91	xrlttrd	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^((n \in z ⟼ O (E (n))))) \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
93	21 28 92	syl2anc	$⊢ ((φ \land z \in (𝒫 Z \cap Fin)) \land O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z})) \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
94	93	ex	$⊢ (φ \land z \in (𝒫 Z \cap Fin)) \to (O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z}) \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y)$
95	94	adantlr	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \land z \in (𝒫 Z \cap Fin)) \to (O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z}) \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y)$
96	95	reximdva	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to (\exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < sum^({(n \in Z ⟼ O (E (n))) ↾}_{z}) \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y)$
97	20 96	mpd	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) = +∞) \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
98		simpl	$⊢ (φ \land \neg sum^((n \in Z ⟼ O (E (n)))) = +∞) \to φ$
99		simpr	$⊢ (φ \land \neg sum^((n \in Z ⟼ O (E (n)))) = +∞) \to \neg sum^((n \in Z ⟼ O (E (n)))) = +∞$
100	7	a1i	$⊢ φ \to Z \in V$
101	100 16	sge0repnf	$⊢ φ \to (sum^((n \in Z ⟼ O (E (n)))) \in ℝ \leftrightarrow \neg sum^((n \in Z ⟼ O (E (n)))) = +∞)$
102	101	adantr	$⊢ (φ \land \neg sum^((n \in Z ⟼ O (E (n)))) = +∞) \to (sum^((n \in Z ⟼ O (E (n)))) \in ℝ \leftrightarrow \neg sum^((n \in Z ⟼ O (E (n)))) = +∞)$
103	99 102	mpbird	$⊢ (φ \land \neg sum^((n \in Z ⟼ O (E (n)))) = +∞) \to sum^((n \in Z ⟼ O (E (n)))) \in ℝ$
104		nfv	$⊢ Ⅎ n φ$
105		nfcv	$⊢ \underline{Ⅎ} n sum^$
106		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ O (E (n)))$
107	105 106	nffv	$⊢ \underline{Ⅎ} n sum^((n \in Z ⟼ O (E (n))))$
108		nfcv	$⊢ \underline{Ⅎ} n ℝ$
109	107 108	nfel	$⊢ Ⅎ n sum^((n \in Z ⟼ O (E (n)))) \in ℝ$
110	104 109	nfan	$⊢ Ⅎ n (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ)$
111	7	a1i	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to Z \in V$
112	14	adantlr	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land n \in Z) \to O (E (n)) \in [0, +∞]$
113	6	adantr	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to Y \in ℝ^{+}$
114		simpr	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to sum^((n \in Z ⟼ O (E (n)))) \in ℝ$
115	110 111 112 113 114	sge0ltfirpmpt	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to \exists z \in (𝒫 Z \cap Fin) sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y$
116	5	ad3antrrr	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to O (⋃_{n \in Z} E (n)) \in ℝ$
117	114	ad2antrr	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to sum^((n \in Z ⟼ O (E (n)))) \in ℝ$
118	71	ad4ant13	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to \sum_{n \in z} O (E (n)) + Y \in ℝ$
119		nfcv	$⊢ \underline{Ⅎ} n E$
120	104 119 1 2 3 4	omeiunle	$⊢ φ \to O (⋃_{n \in Z} E (n)) \leq sum^((n \in Z ⟼ O (E (n))))$
121	120	ad3antrrr	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to O (⋃_{n \in Z} E (n)) \leq sum^((n \in Z ⟼ O (E (n))))$
122		simpr	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y$
123		simpll	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to φ$
124		2fveq3	$⊢ n = m \to O (E (n)) = O (E (m))$
125	124	cbvmptv	$⊢ (n \in Z ⟼ O (E (n))) = (m \in Z ⟼ O (E (m)))$
126	125	fveq2i	$⊢ sum^((n \in Z ⟼ O (E (n)))) = sum^((m \in Z ⟼ O (E (m))))$
127	126	eleq1i	$⊢ sum^((n \in Z ⟼ O (E (n)))) \in ℝ \leftrightarrow sum^((m \in Z ⟼ O (E (m)))) \in ℝ$
128	127	biimpi	$⊢ sum^((n \in Z ⟼ O (E (n)))) \in ℝ \to sum^((m \in Z ⟼ O (E (m)))) \in ℝ$
129	128	ad2antlr	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to sum^((m \in Z ⟼ O (E (m)))) \in ℝ$
130		simpr	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to z \in (𝒫 Z \cap Fin)$
131	45	adantl	$⊢ ((φ \land sum^((m \in Z ⟼ O (E (m)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to z \in Fin$
132	66	adantllr	$⊢ (((φ \land sum^((m \in Z ⟼ O (E (m)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land n \in z) \to O (E (n)) \in [0, +∞)$
133	131 132	sge0fsummpt	$⊢ ((φ \land sum^((m \in Z ⟼ O (E (m)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) = \sum_{n \in z} O (E (n))$
134	123 129 130 133	syl21anc	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) = \sum_{n \in z} O (E (n))$
135	134	oveq1d	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to sum^((n \in z ⟼ O (E (n)))) + Y = \sum_{n \in z} O (E (n)) + Y$
136	135	adantr	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to sum^((n \in z ⟼ O (E (n)))) + Y = \sum_{n \in z} O (E (n)) + Y$
137	122 136	breqtrd	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to sum^((n \in Z ⟼ O (E (n)))) < \sum_{n \in z} O (E (n)) + Y$
138	116 117 118 121 137	lelttrd	$⊢ (((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \land sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y) \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
139	138	ex	$⊢ ((φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \land z \in (𝒫 Z \cap Fin)) \to (sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y \to O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y)$
140	139	reximdva	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to (\exists z \in (𝒫 Z \cap Fin) sum^((n \in Z ⟼ O (E (n)))) < sum^((n \in z ⟼ O (E (n)))) + Y \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y)$
141	115 140	mpd	$⊢ (φ \land sum^((n \in Z ⟼ O (E (n)))) \in ℝ) \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
142	98 103 141	syl2anc	$⊢ (φ \land \neg sum^((n \in Z ⟼ O (E (n)))) = +∞) \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$
143	97 142	pm2.61dan	$⊢ φ \to \exists z \in (𝒫 Z \cap Fin) O (⋃_{n \in Z} E (n)) < \sum_{n \in z} O (E (n)) + Y$

Metamath Proof Explorer

Theorem omeiunltfirp

Proof