sge0rpcpnf

Description: The sum of an infinite number of a positive constant, is +oo (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0rpcpnf.a	$⊢ φ \to A \in V$
	sge0rpcpnf.nfi	$⊢ φ \to \neg A \in Fin$
	sge0rpcpnf.b	$⊢ φ \to B \in ℝ^{+}$
Assertion	sge0rpcpnf	$⊢ φ \to sum^((x \in A ⟼ B)) = +∞$

Proof

Step	Hyp	Ref	Expression
1		sge0rpcpnf.a	$⊢ φ \to A \in V$
2		sge0rpcpnf.nfi	$⊢ φ \to \neg A \in Fin$
3		sge0rpcpnf.b	$⊢ φ \to B \in ℝ^{+}$
4	1	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to A \in V$
5		0xr	$⊢ 0 \in ℝ^{*}$
6	5	a1i	$⊢ φ \to 0 \in ℝ^{*}$
7		pnfxr	$⊢ +∞ \in ℝ^{*}$
8	7	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
9	3	rpxrd	$⊢ φ \to B \in ℝ^{*}$
10	3	rpge0d	$⊢ φ \to 0 \leq B$
11	3	rpred	$⊢ φ \to B \in ℝ$
12		ltpnf	$⊢ B \in ℝ \to B < +∞$
13	11 12	syl	$⊢ φ \to B < +∞$
14	9 8 13	xrltled	$⊢ φ \to B \leq +∞$
15	6 8 9 10 14	eliccxrd	$⊢ φ \to B \in [0, +∞]$
16	15	adantr	$⊢ (φ \land x \in A) \to B \in [0, +∞]$
17		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
18	16 17	fmptd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ [0, +∞]$
19	18	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to (x \in A ⟼ B) : A ⟶ [0, +∞]$
20	4 19	sge0xrcl	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to sum^((x \in A ⟼ B)) \in ℝ^{*}$
21	7	a1i	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to +∞ \in ℝ^{*}$
22		simpr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to sum^((x \in A ⟼ B)) < +∞$
23	20 21 22	xrgtned	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to +∞ \neq sum^((x \in A ⟼ B))$
24	23	necomd	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to sum^((x \in A ⟼ B)) \neq +∞$
25	24	neneqd	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to \neg sum^((x \in A ⟼ B)) = +∞$
26	4 19	sge0repnf	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to (sum^((x \in A ⟼ B)) \in ℝ \leftrightarrow \neg sum^((x \in A ⟼ B)) = +∞)$
27	25 26	mpbird	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to sum^((x \in A ⟼ B)) \in ℝ$
28	11	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to B \in ℝ$
29	3	rpne0d	$⊢ φ \to B \neq 0$
30	29	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to B \neq 0$
31	27 28 30	redivcld	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to \frac{sum^((x \in A ⟼ B))}{B} \in ℝ$
32		arch	$⊢ \frac{sum^((x \in A ⟼ B))}{B} \in ℝ \to \exists n \in ℕ \frac{sum^((x \in A ⟼ B))}{B} < n$
33	31 32	syl	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to \exists n \in ℕ \frac{sum^((x \in A ⟼ B))}{B} < n$
34		ishashinf	$⊢ \neg A \in Fin \to \forall n \in ℕ \exists y \in 𝒫 A \|y\| = n$
35	2 34	syl	$⊢ φ \to \forall n \in ℕ \exists y \in 𝒫 A \|y\| = n$
36	35	r19.21bi	$⊢ (φ \land n \in ℕ) \to \exists y \in 𝒫 A \|y\| = n$
37		df-rex	$⊢ \exists y \in 𝒫 A \|y\| = n \leftrightarrow \exists y (y \in 𝒫 A \land \|y\| = n)$
38	36 37	sylib	$⊢ (φ \land n \in ℕ) \to \exists y (y \in 𝒫 A \land \|y\| = n)$
39	38	adantlr	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ) \to \exists y (y \in 𝒫 A \land \|y\| = n)$
40	39	3adant3	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to \exists y (y \in 𝒫 A \land \|y\| = n)$
41		nfv	$⊢ Ⅎ y ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n)$
42		simprl	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to y \in 𝒫 A$
43		simpr	$⊢ (n \in ℕ \land \|y\| = n) \to \|y\| = n$
44		simpl	$⊢ (n \in ℕ \land \|y\| = n) \to n \in ℕ$
45	43 44	eqeltrd	$⊢ (n \in ℕ \land \|y\| = n) \to \|y\| \in ℕ$
46		nnnn0	$⊢ \|y\| \in ℕ \to \|y\| \in ℕ_{0}$
47		vex	$⊢ y \in V$
48	47	a1i	$⊢ \|y\| \in ℕ \to y \in V$
49		hashclb	$⊢ y \in V \to (y \in Fin \leftrightarrow \|y\| \in ℕ_{0})$
50	48 49	syl	$⊢ \|y\| \in ℕ \to (y \in Fin \leftrightarrow \|y\| \in ℕ_{0})$
51	46 50	mpbird	$⊢ \|y\| \in ℕ \to y \in Fin$
52	45 51	syl	$⊢ (n \in ℕ \land \|y\| = n) \to y \in Fin$
53	52	adantrl	$⊢ (n \in ℕ \land (y \in 𝒫 A \land \|y\| = n)) \to y \in Fin$
54	53	3ad2antl2	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to y \in Fin$
55	42 54	elind	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to y \in (𝒫 A \cap Fin)$
56		simp3	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to \frac{sum^((x \in A ⟼ B))}{B} < n$
57	27	3ad2ant1	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to sum^((x \in A ⟼ B)) \in ℝ$
58		nnre	$⊢ n \in ℕ \to n \in ℝ$
59	58	3ad2ant2	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to n \in ℝ$
60	3	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to B \in ℝ^{+}$
61	60	3ad2ant1	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to B \in ℝ^{+}$
62	57 59 61	ltdivmul2d	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to (\frac{sum^((x \in A ⟼ B))}{B} < n \leftrightarrow sum^((x \in A ⟼ B)) < n B)$
63	56 62	mpbid	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to sum^((x \in A ⟼ B)) < n B$
64	63	adantr	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to sum^((x \in A ⟼ B)) < n B$
65	53	adantll	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to y \in Fin$
66	5	a1i	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to 0 \in ℝ^{*}$
67	7	a1i	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to +∞ \in ℝ^{*}$
68	9	ad3antrrr	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to B \in ℝ^{*}$
69	10	ad3antrrr	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to 0 \leq B$
70	13	ad3antrrr	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to B < +∞$
71	66 67 68 69 70	elicod	$⊢ (((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \land x \in y) \to B \in [0, +∞)$
72	65 71	sge0fsummpt	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to sum^((x \in y ⟼ B)) = \sum_{x \in y} B$
73	11	recnd	$⊢ φ \to B \in ℂ$
74	73	ad2antrr	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to B \in ℂ$
75		fsumconst	$⊢ (y \in Fin \land B \in ℂ) \to \sum_{x \in y} B = \|y\| B$
76	65 74 75	syl2anc	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to \sum_{x \in y} B = \|y\| B$
77		oveq1	$⊢ \|y\| = n \to \|y\| B = n B$
78	77	adantl	$⊢ (y \in 𝒫 A \land \|y\| = n) \to \|y\| B = n B$
79	78	adantl	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to \|y\| B = n B$
80	72 76 79	3eqtrrd	$⊢ ((φ \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to n B = sum^((x \in y ⟼ B))$
81	80	adantllr	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ) \land (y \in 𝒫 A \land \|y\| = n)) \to n B = sum^((x \in y ⟼ B))$
82	81	3adantl3	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to n B = sum^((x \in y ⟼ B))$
83	64 82	breqtrd	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
84	55 83	jca	$⊢ (((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \land (y \in 𝒫 A \land \|y\| = n)) \to (y \in (𝒫 A \cap Fin) \land sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)))$
85	84	ex	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to ((y \in 𝒫 A \land \|y\| = n) \to (y \in (𝒫 A \cap Fin) \land sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))))$
86	41 85	eximd	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to (\exists y (y \in 𝒫 A \land \|y\| = n) \to \exists y (y \in (𝒫 A \cap Fin) \land sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))))$
87	40 86	mpd	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to \exists y (y \in (𝒫 A \cap Fin) \land sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)))$
88		df-rex	$⊢ \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)) \leftrightarrow \exists y (y \in (𝒫 A \cap Fin) \land sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)))$
89	87 88	sylibr	$⊢ ((φ \land sum^((x \in A ⟼ B)) < +∞) \land n \in ℕ \land \frac{sum^((x \in A ⟼ B))}{B} < n) \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
90	89	3exp	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to (n \in ℕ \to (\frac{sum^((x \in A ⟼ B))}{B} < n \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))))$
91	90	rexlimdv	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to (\exists n \in ℕ \frac{sum^((x \in A ⟼ B))}{B} < n \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)))$
92	33 91	mpd	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
93	1	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to A \in V$
94	16	adantlr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in A) \to B \in [0, +∞]$
95		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
96	95	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
97	93 94 96	sge0lessmpt	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in y ⟼ B)) \leq sum^((x \in A ⟼ B))$
98		simpr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in (𝒫 A \cap Fin)$
99	15	adantr	$⊢ (φ \land x \in y) \to B \in [0, +∞]$
100		eqid	$⊢ (x \in y ⟼ B) = (x \in y ⟼ B)$
101	99 100	fmptd	$⊢ φ \to (x \in y ⟼ B) : y ⟶ [0, +∞]$
102	101	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (x \in y ⟼ B) : y ⟶ [0, +∞]$
103	98 102	sge0xrcl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in y ⟼ B)) \in ℝ^{*}$
104	1 18	sge0xrcl	$⊢ φ \to sum^((x \in A ⟼ B)) \in ℝ^{*}$
105	104	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in A ⟼ B)) \in ℝ^{*}$
106	103 105	xrlenltd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (sum^((x \in y ⟼ B)) \leq sum^((x \in A ⟼ B)) \leftrightarrow \neg sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)))$
107	97 106	mpbid	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \neg sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
108	107	ralrimiva	$⊢ φ \to \forall y \in (𝒫 A \cap Fin) \neg sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
109		ralnex	$⊢ \forall y \in (𝒫 A \cap Fin) \neg sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B)) \leftrightarrow \neg \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
110	108 109	sylib	$⊢ φ \to \neg \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
111	110	adantr	$⊢ (φ \land sum^((x \in A ⟼ B)) < +∞) \to \neg \exists y \in (𝒫 A \cap Fin) sum^((x \in A ⟼ B)) < sum^((x \in y ⟼ B))$
112	92 111	pm2.65da	$⊢ φ \to \neg sum^((x \in A ⟼ B)) < +∞$
113		nltpnft	$⊢ sum^((x \in A ⟼ B)) \in ℝ^{*} \to (sum^((x \in A ⟼ B)) = +∞ \leftrightarrow \neg sum^((x \in A ⟼ B)) < +∞)$
114	104 113	syl	$⊢ φ \to (sum^((x \in A ⟼ B)) = +∞ \leftrightarrow \neg sum^((x \in A ⟼ B)) < +∞)$
115	112 114	mpbird	$⊢ φ \to sum^((x \in A ⟼ B)) = +∞$

Metamath Proof Explorer

Theorem sge0rpcpnf

Proof