rpnnen2lem10

	Ref	Expression
Hypotheses	rpnnen2.1	$⊢ F = (x \in 𝒫 ℕ ⟼ (n \in ℕ ⟼ if (n \in x, {(\frac{1}{3})}^{n}, 0)))$
	rpnnen2.2	$⊢ φ \to A \subseteq ℕ$
	rpnnen2.3	$⊢ φ \to B \subseteq ℕ$
	rpnnen2.4	$⊢ φ \to m \in (A ∖ B)$
	rpnnen2.5	$⊢ φ \to \forall n \in ℕ (n < m \to (n \in A \leftrightarrow n \in B))$
	rpnnen2.6	$⊢ ψ \leftrightarrow \sum_{k \in ℕ} F (A) (k) = \sum_{k \in ℕ} F (B) (k)$
Assertion	rpnnen2lem10	$⊢ (φ \land ψ) \to \sum_{k \in ℤ_{\geq m}} F (A) (k) = \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		rpnnen2.2	$⊢ φ \to A \subseteq ℕ$
3		rpnnen2.3	$⊢ φ \to B \subseteq ℕ$
4		rpnnen2.4	$⊢ φ \to m \in (A ∖ B)$
5		rpnnen2.5	$⊢ φ \to \forall n \in ℕ (n < m \to (n \in A \leftrightarrow n \in B))$
6		rpnnen2.6	$⊢ ψ \leftrightarrow \sum_{k \in ℕ} F (A) (k) = \sum_{k \in ℕ} F (B) (k)$
7		simpr	$⊢ (φ \land ψ) \to ψ$
8	7 6	sylib	$⊢ (φ \land ψ) \to \sum_{k \in ℕ} F (A) (k) = \sum_{k \in ℕ} F (B) (k)$
9		eldifi	$⊢ m \in (A ∖ B) \to m \in A$
10		ssel2	$⊢ (A \subseteq ℕ \land m \in A) \to m \in ℕ$
11	9 10	sylan2	$⊢ (A \subseteq ℕ \land m \in (A ∖ B)) \to m \in ℕ$
12	2 4 11	syl2anc	$⊢ φ \to m \in ℕ$
13	1	rpnnen2lem8	$⊢ (A \subseteq ℕ \land m \in ℕ) \to \sum_{k \in ℕ} F (A) (k) = \sum_{k = 1}^{m - 1} F (A) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k)$
14	2 12 13	syl2anc	$⊢ φ \to \sum_{k \in ℕ} F (A) (k) = \sum_{k = 1}^{m - 1} F (A) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k)$
15		1z	$⊢ 1 \in ℤ$
16		nnz	$⊢ m \in ℕ \to m \in ℤ$
17		elfzm11	$⊢ (1 \in ℤ \land m \in ℤ) \to (k \in (1 \dots m - 1) \leftrightarrow (k \in ℤ \land 1 \leq k \land k < m))$
18	15 16 17	sylancr	$⊢ m \in ℕ \to (k \in (1 \dots m - 1) \leftrightarrow (k \in ℤ \land 1 \leq k \land k < m))$
19	18	biimpa	$⊢ (m \in ℕ \land k \in (1 \dots m - 1)) \to (k \in ℤ \land 1 \leq k \land k < m)$
20	12 19	sylan	$⊢ (φ \land k \in (1 \dots m - 1)) \to (k \in ℤ \land 1 \leq k \land k < m)$
21	20	simp3d	$⊢ (φ \land k \in (1 \dots m - 1)) \to k < m$
22		elfznn	$⊢ k \in (1 \dots m - 1) \to k \in ℕ$
23		breq1	$⊢ n = k \to (n < m \leftrightarrow k < m)$
24		eleq1w	$⊢ n = k \to (n \in A \leftrightarrow k \in A)$
25		eleq1w	$⊢ n = k \to (n \in B \leftrightarrow k \in B)$
26	24 25	bibi12d	$⊢ n = k \to ((n \in A \leftrightarrow n \in B) \leftrightarrow (k \in A \leftrightarrow k \in B))$
27	23 26	imbi12d	$⊢ n = k \to ((n < m \to (n \in A \leftrightarrow n \in B)) \leftrightarrow (k < m \to (k \in A \leftrightarrow k \in B)))$
28	27	rspccva	$⊢ (\forall n \in ℕ (n < m \to (n \in A \leftrightarrow n \in B)) \land k \in ℕ) \to (k < m \to (k \in A \leftrightarrow k \in B))$
29	5 22 28	syl2an	$⊢ (φ \land k \in (1 \dots m - 1)) \to (k < m \to (k \in A \leftrightarrow k \in B))$
30	21 29	mpd	$⊢ (φ \land k \in (1 \dots m - 1)) \to (k \in A \leftrightarrow k \in B)$
31	30	ifbid	$⊢ (φ \land k \in (1 \dots m - 1)) \to if (k \in A, {(\frac{1}{3})}^{k}, 0) = if (k \in B, {(\frac{1}{3})}^{k}, 0)$
32	1	rpnnen2lem1	$⊢ (A \subseteq ℕ \land k \in ℕ) \to F (A) (k) = if (k \in A, {(\frac{1}{3})}^{k}, 0)$
33	2 22 32	syl2an	$⊢ (φ \land k \in (1 \dots m - 1)) \to F (A) (k) = if (k \in A, {(\frac{1}{3})}^{k}, 0)$
34	1	rpnnen2lem1	$⊢ (B \subseteq ℕ \land k \in ℕ) \to F (B) (k) = if (k \in B, {(\frac{1}{3})}^{k}, 0)$
35	3 22 34	syl2an	$⊢ (φ \land k \in (1 \dots m - 1)) \to F (B) (k) = if (k \in B, {(\frac{1}{3})}^{k}, 0)$
36	31 33 35	3eqtr4d	$⊢ (φ \land k \in (1 \dots m - 1)) \to F (A) (k) = F (B) (k)$
37	36	sumeq2dv	$⊢ φ \to \sum_{k = 1}^{m - 1} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k)$
38	37	oveq1d	$⊢ φ \to \sum_{k = 1}^{m - 1} F (A) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k)$
39	14 38	eqtrd	$⊢ φ \to \sum_{k \in ℕ} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k)$
40	39	adantr	$⊢ (φ \land ψ) \to \sum_{k \in ℕ} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k)$
41	1	rpnnen2lem8	$⊢ (B \subseteq ℕ \land m \in ℕ) \to \sum_{k \in ℕ} F (B) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k)$
42	3 12 41	syl2anc	$⊢ φ \to \sum_{k \in ℕ} F (B) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k)$
43	42	adantr	$⊢ (φ \land ψ) \to \sum_{k \in ℕ} F (B) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k)$
44	8 40 43	3eqtr3d	$⊢ (φ \land ψ) \to \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k)$
45	1	rpnnen2lem6	$⊢ (A \subseteq ℕ \land m \in ℕ) \to \sum_{k \in ℤ_{\geq m}} F (A) (k) \in ℝ$
46	2 12 45	syl2anc	$⊢ φ \to \sum_{k \in ℤ_{\geq m}} F (A) (k) \in ℝ$
47	1	rpnnen2lem6	$⊢ (B \subseteq ℕ \land m \in ℕ) \to \sum_{k \in ℤ_{\geq m}} F (B) (k) \in ℝ$
48	3 12 47	syl2anc	$⊢ φ \to \sum_{k \in ℤ_{\geq m}} F (B) (k) \in ℝ$
49		fzfid	$⊢ φ \to (1 \dots m - 1) \in Fin$
50	1	rpnnen2lem2	$⊢ B \subseteq ℕ \to F (B) : ℕ ⟶ ℝ$
51	3 50	syl	$⊢ φ \to F (B) : ℕ ⟶ ℝ$
52		ffvelcdm	$⊢ (F (B) : ℕ ⟶ ℝ \land k \in ℕ) \to F (B) (k) \in ℝ$
53	51 22 52	syl2an	$⊢ (φ \land k \in (1 \dots m - 1)) \to F (B) (k) \in ℝ$
54	49 53	fsumrecl	$⊢ φ \to \sum_{k = 1}^{m - 1} F (B) (k) \in ℝ$
55		readdcan	$⊢ (\sum_{k \in ℤ_{\geq m}} F (A) (k) \in ℝ \land \sum_{k \in ℤ_{\geq m}} F (B) (k) \in ℝ \land \sum_{k = 1}^{m - 1} F (B) (k) \in ℝ) \to (\sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k) \leftrightarrow \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k \in ℤ_{\geq m}} F (B) (k))$
56	46 48 54 55	syl3anc	$⊢ φ \to (\sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k) \leftrightarrow \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k \in ℤ_{\geq m}} F (B) (k))$
57	56	adantr	$⊢ (φ \land ψ) \to (\sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k = 1}^{m - 1} F (B) (k) + \sum_{k \in ℤ_{\geq m}} F (B) (k) \leftrightarrow \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k \in ℤ_{\geq m}} F (B) (k))$
58	44 57	mpbid	$⊢ (φ \land ψ) \to \sum_{k \in ℤ_{\geq m}} F (A) (k) = \sum_{k \in ℤ_{\geq m}} F (B) (k)$

Metamath Proof Explorer

Theorem rpnnen2lem10

Proof