rpnnen2lem7

		Ref	Expression
	Hypothesis	rpnnen2.1	$⊢ F = (x \in 𝒫 ℕ ⟼ (n \in ℕ ⟼ if (n \in x, {(\frac{1}{3})}^{n}, 0)))$
	Assertion	rpnnen2lem7	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to \sum_{k \in ℤ_{\geq M}} F (A) (k) \leq \sum_{k \in ℤ_{\geq M}} F (B) (k)$

Proof

Step	Hyp	Ref	Expression
1		rpnnen2.1	$⊢ F = (x \in 𝒫 ℕ ⟼ (n \in ℕ ⟼ if (n \in x, {(\frac{1}{3})}^{n}, 0)))$
2		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
3		simp3	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to M \in ℕ$
4	3	nnzd	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to M \in ℤ$
5		eqidd	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) (k) = F (A) (k)$
6		eluznn	$⊢ (M \in ℕ \land k \in ℤ_{\geq M}) \to k \in ℕ$
7	3 6	sylan	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to k \in ℕ$
8		sstr	$⊢ (A \subseteq B \land B \subseteq ℕ) \to A \subseteq ℕ$
9	8	3adant3	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to A \subseteq ℕ$
10	1	rpnnen2lem2	$⊢ A \subseteq ℕ \to F (A) : ℕ ⟶ ℝ$
11	9 10	syl	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to F (A) : ℕ ⟶ ℝ$
12	11	ffvelcdmda	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℕ) \to F (A) (k) \in ℝ$
13	7 12	syldan	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) (k) \in ℝ$
14		eqidd	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (B) (k) = F (B) (k)$
15	1	rpnnen2lem2	$⊢ B \subseteq ℕ \to F (B) : ℕ ⟶ ℝ$
16	15	3ad2ant2	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to F (B) : ℕ ⟶ ℝ$
17	16	ffvelcdmda	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℕ) \to F (B) (k) \in ℝ$
18	7 17	syldan	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (B) (k) \in ℝ$
19	1	rpnnen2lem4	$⊢ (A \subseteq B \land B \subseteq ℕ \land k \in ℕ) \to (0 \leq F (A) (k) \land F (A) (k) \leq F (B) (k))$
20	19	simprd	$⊢ (A \subseteq B \land B \subseteq ℕ \land k \in ℕ) \to F (A) (k) \leq F (B) (k)$
21	20	3expa	$⊢ ((A \subseteq B \land B \subseteq ℕ) \land k \in ℕ) \to F (A) (k) \leq F (B) (k)$
22	21	3adantl3	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℕ) \to F (A) (k) \leq F (B) (k)$
23	7 22	syldan	$⊢ ((A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \land k \in ℤ_{\geq M}) \to F (A) (k) \leq F (B) (k)$
24	1	rpnnen2lem5	$⊢ (A \subseteq ℕ \land M \in ℕ) \to seq M (+ F (A)) \in dom ⇝$
25	8 24	stoic3	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to seq M (+ F (A)) \in dom ⇝$
26	1	rpnnen2lem5	$⊢ (B \subseteq ℕ \land M \in ℕ) \to seq M (+ F (B)) \in dom ⇝$
27	26	3adant1	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to seq M (+ F (B)) \in dom ⇝$
28	2 4 5 13 14 18 23 25 27	isumle	$⊢ (A \subseteq B \land B \subseteq ℕ \land M \in ℕ) \to \sum_{k \in ℤ_{\geq M}} F (A) (k) \leq \sum_{k \in ℤ_{\geq M}} F (B) (k)$

Metamath Proof Explorer

Theorem rpnnen2lem7

Proof