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