eulerpartlemgs2

Description: Lemma for eulerpart : The G function also preserves partition sums. (Contributed by Thierry Arnoux, 10-Sep-2017)

	Ref	Expression
Hypotheses	eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
	eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
	eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
	eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
	eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
	eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
	eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
	eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
	eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
	eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
	eulerpart.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
Assertion	eulerpartlemgs2	$⊢ A \in (T \cap R) \to S (G (A)) = S (A)$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
2		eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
3		eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
4		eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
5		eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
6		eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
7		eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
8		eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
9		eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
10		eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
11		eulerpart.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
12		cnvimass	$⊢ {G (A)}^{-1} [ℕ] \subseteq dom G (A)$
13	1 2 3 4 5 6 7 8 9 10	eulerpartgbij	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
14		f1of	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R \to G : T \cap R ⟶ ({\{0, 1\}}^{ℕ}) \cap R$
15	13 14	ax-mp	$⊢ G : T \cap R ⟶ ({\{0, 1\}}^{ℕ}) \cap R$
16	15	ffvelcdmi	$⊢ A \in (T \cap R) \to G (A) \in (({\{0, 1\}}^{ℕ}) \cap R)$
17		elin	$⊢ G (A) \in (({\{0, 1\}}^{ℕ}) \cap R) \leftrightarrow (G (A) \in ({\{0, 1\}}^{ℕ}) \land G (A) \in R)$
18	16 17	sylib	$⊢ A \in (T \cap R) \to (G (A) \in ({\{0, 1\}}^{ℕ}) \land G (A) \in R)$
19	18	simpld	$⊢ A \in (T \cap R) \to G (A) \in ({\{0, 1\}}^{ℕ})$
20		elmapi	$⊢ G (A) \in ({\{0, 1\}}^{ℕ}) \to G (A) : ℕ ⟶ \{0, 1\}$
21		fdm	$⊢ G (A) : ℕ ⟶ \{0, 1\} \to dom G (A) = ℕ$
22	19 20 21	3syl	$⊢ A \in (T \cap R) \to dom G (A) = ℕ$
23	12 22	sseqtrid	$⊢ A \in (T \cap R) \to {G (A)}^{-1} [ℕ] \subseteq ℕ$
24	23	sselda	$⊢ (A \in (T \cap R) \land k \in {G (A)}^{-1} [ℕ]) \to k \in ℕ$
25	1 2 3 4 5 6 7 8 9 10	eulerpartlemgvv	$⊢ (A \in (T \cap R) \land k \in ℕ) \to G (A) (k) = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0)$
26	25	oveq1d	$⊢ (A \in (T \cap R) \land k \in ℕ) \to G (A) (k) k = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k$
27	24 26	syldan	$⊢ (A \in (T \cap R) \land k \in {G (A)}^{-1} [ℕ]) \to G (A) (k) k = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k$
28	27	sumeq2dv	$⊢ A \in (T \cap R) \to \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k = \sum_{k \in {G (A)}^{-1} [ℕ]} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k$
29		eqeq2	$⊢ m = k \to (2^{n} t = m \leftrightarrow 2^{n} t = k)$
30	29	2rexbidv	$⊢ m = k \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m \leftrightarrow \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k)$
31	30	elrab	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \leftrightarrow (k \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k)$
32	31	simprbi	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k$
33	32	iftrued	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) = 1$
34	33	oveq1d	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = 1 k$
35		elrabi	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to k \in ℕ$
36	35	nncnd	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to k \in ℂ$
37	36	mullidd	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to 1 k = k$
38	34 37	eqtrd	$⊢ k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = k$
39	38	sumeq2i	$⊢ \sum_{k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = \sum_{k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}} k$
40		id	$⊢ k = 2^{2^{nd} (w)} 1^{st} (w) \to k = 2^{2^{nd} (w)} 1^{st} (w)$
41	1 2 3 4 5 6 7 8 9 10	eulerpartlemgf	$⊢ A \in (T \cap R) \to {G (A)}^{-1} [ℕ] \in Fin$
42	35	adantl	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in ℕ$
43	42 25	syldan	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to G (A) (k) = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0)$
44	32	adantl	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k$
45	44	iftrued	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) = 1$
46	43 45	eqtrd	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to G (A) (k) = 1$
47		1nn	$⊢ 1 \in ℕ$
48	46 47	eqeltrdi	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to G (A) (k) \in ℕ$
49		ffn	$⊢ G (A) : ℕ ⟶ \{0, 1\} \to G (A) Fn ℕ$
50		elpreima	$⊢ G (A) Fn ℕ \to (k \in {G (A)}^{-1} [ℕ] \leftrightarrow (k \in ℕ \land G (A) (k) \in ℕ))$
51	19 20 49 50	4syl	$⊢ A \in (T \cap R) \to (k \in {G (A)}^{-1} [ℕ] \leftrightarrow (k \in ℕ \land G (A) (k) \in ℕ))$
52	51	adantr	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to (k \in {G (A)}^{-1} [ℕ] \leftrightarrow (k \in ℕ \land G (A) (k) \in ℕ))$
53	42 48 52	mpbir2and	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in {G (A)}^{-1} [ℕ]$
54	53	ex	$⊢ A \in (T \cap R) \to (k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to k \in {G (A)}^{-1} [ℕ])$
55	54	ssrdv	$⊢ A \in (T \cap R) \to \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq {G (A)}^{-1} [ℕ]$
56		ssfi	$⊢ ({G (A)}^{-1} [ℕ] \in Fin \land \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq {G (A)}^{-1} [ℕ]) \to \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \in Fin$
57	41 55 56	syl2anc	$⊢ A \in (T \cap R) \to \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \in Fin$
58		cnvexg	$⊢ A \in (T \cap R) \to A^{-1} \in V$
59		imaexg	$⊢ A^{-1} \in V \to A^{-1} [ℕ] \in V$
60		inex1g	$⊢ A^{-1} [ℕ] \in V \to A^{-1} [ℕ] \cap J \in V$
61	58 59 60	3syl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J \in V$
62		vsnex	$⊢ \{t\} \in V$
63		fvex	$⊢ bits (A (t)) \in V$
64	62 63	xpex	$⊢ \{t\} \times bits (A (t)) \in V$
65	64	rgenw	$⊢ \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \in V$
66		iunexg	$⊢ (A^{-1} [ℕ] \cap J \in V \land \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \in V) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in V$
67	61 65 66	sylancl	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in V$
68		eqid	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
69	1 2 3 4 5 6 7 8 9 10 68	eulerpartlemgh	$⊢ A \in (T \cap R) \to ({F ↾}_{⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))}) : ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
70		f1oeng	$⊢ (⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in V \land ({F ↾}_{⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))}) : ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \underset{1-1 onto}{⟶} \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \approx \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
71	67 69 70	syl2anc	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \approx \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
72		enfii	$⊢ (\{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \in Fin \land ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \approx \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in Fin$
73	57 71 72	syl2anc	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in Fin$
74		fvres	$⊢ w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \to ({F ↾}_{⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))}) (w) = F (w)$
75	74	adantl	$⊢ (A \in (T \cap R) \land w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))) \to ({F ↾}_{⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))}) (w) = F (w)$
76		inss2	$⊢ A^{-1} [ℕ] \cap J \subseteq J$
77		simpr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in (A^{-1} [ℕ] \cap J)$
78	76 77	sselid	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in J$
79	78	snssd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \{t\} \subseteq J$
80		bitsss	$⊢ bits (A (t)) \subseteq ℕ_{0}$
81		xpss12	$⊢ (\{t\} \subseteq J \land bits (A (t)) \subseteq ℕ_{0}) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
82	79 80 81	sylancl	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
83	82	ralrimiva	$⊢ A \in (T \cap R) \to \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
84		iunss	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \subseteq J \times ℕ_{0} \leftrightarrow \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
85	83 84	sylibr	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \subseteq J \times ℕ_{0}$
86	85	sselda	$⊢ (A \in (T \cap R) \land w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))) \to w \in (J \times ℕ_{0})$
87	4 5	oddpwdcv	$⊢ w \in (J \times ℕ_{0}) \to F (w) = 2^{2^{nd} (w)} 1^{st} (w)$
88	86 87	syl	$⊢ (A \in (T \cap R) \land w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))) \to F (w) = 2^{2^{nd} (w)} 1^{st} (w)$
89	75 88	eqtrd	$⊢ (A \in (T \cap R) \land w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))) \to ({F ↾}_{⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))}) (w) = 2^{2^{nd} (w)} 1^{st} (w)$
90	42	nncnd	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in ℂ$
91	40 73 69 89 90	fsumf1o	$⊢ A \in (T \cap R) \to \sum_{k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}} k = \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w)$
92	39 91	eqtrid	$⊢ A \in (T \cap R) \to \sum_{k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w)$
93		ax-1cn	$⊢ 1 \in ℂ$
94		0cn	$⊢ 0 \in ℂ$
95	93 94	ifcli	$⊢ if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) \in ℂ$
96	95	a1i	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) \in ℂ$
97		ssrab2	$⊢ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq ℕ$
98		simpr	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
99	97 98	sselid	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in ℕ$
100	99	nncnd	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to k \in ℂ$
101	96 100	mulcld	$⊢ (A \in (T \cap R) \land k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k \in ℂ$
102		simpr	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})$
103	102	eldifbd	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to \neg k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}$
104	23	ssdifssd	$⊢ A \in (T \cap R) \to {G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq ℕ$
105	104	sselda	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to k \in ℕ$
106	31	notbii	$⊢ \neg k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \leftrightarrow \neg (k \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k)$
107		imnan	$⊢ (k \in ℕ \to \neg \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k) \leftrightarrow \neg (k \in ℕ \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k)$
108	106 107	sylbb2	$⊢ \neg k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \to (k \in ℕ \to \neg \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k)$
109	103 105 108	sylc	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to \neg \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k$
110	109	iffalsed	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) = 0$
111	110	oveq1d	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = 0 \cdot k$
112		nnsscn	$⊢ ℕ \subseteq ℂ$
113	104 112	sstrdi	$⊢ A \in (T \cap R) \to {G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq ℂ$
114	113	sselda	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to k \in ℂ$
115	114	mul02d	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to 0 \cdot k = 0$
116	111 115	eqtrd	$⊢ (A \in (T \cap R) \land k \in ({G (A)}^{-1} [ℕ] ∖ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\})) \to if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = 0$
117	55 101 116 41	fsumss	$⊢ A \in (T \cap R) \to \sum_{k \in \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\}} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k = \sum_{k \in {G (A)}^{-1} [ℕ]} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k$
118	92 117	eqtr3d	$⊢ A \in (T \cap R) \to \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w) = \sum_{k \in {G (A)}^{-1} [ℕ]} if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) k$
119	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ A \in (T \cap R) \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \subseteq J)$
120	119	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
121		elmapi	$⊢ A \in ({ℕ_{0}}^{ℕ}) \to A : ℕ ⟶ ℕ_{0}$
122	120 121	syl	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
123	122	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A : ℕ ⟶ ℕ_{0}$
124		cnvimass	$⊢ A^{-1} [ℕ] \subseteq dom A$
125	124 122	fssdm	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq ℕ$
126	125	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A^{-1} [ℕ] \subseteq ℕ$
127		inss1	$⊢ A^{-1} [ℕ] \cap J \subseteq A^{-1} [ℕ]$
128	127 77	sselid	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in A^{-1} [ℕ]$
129	126 128	sseldd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in ℕ$
130	123 129	ffvelcdmd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A (t) \in ℕ_{0}$
131		bitsfi	$⊢ A (t) \in ℕ_{0} \to bits (A (t)) \in Fin$
132	130 131	syl	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to bits (A (t)) \in Fin$
133	129	nncnd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in ℂ$
134		2cnd	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2 \in ℂ$
135		simprr	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to n \in bits (A (t))$
136	80 135	sselid	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to n \in ℕ_{0}$
137	134 136	expcld	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2^{n} \in ℂ$
138	137	anassrs	$⊢ ((A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \land n \in bits (A (t))) \to 2^{n} \in ℂ$
139	132 133 138	fsummulc1	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \sum_{n \in bits (A (t))} 2^{n} t = \sum_{n \in bits (A (t))} 2^{n} t$
140	139	sumeq2dv	$⊢ A \in (T \cap R) \to \sum_{t \in A^{-1} [ℕ] \cap J} \sum_{n \in bits (A (t))} 2^{n} t = \sum_{t \in A^{-1} [ℕ] \cap J} \sum_{n \in bits (A (t))} 2^{n} t$
141		bitsinv1	$⊢ A (t) \in ℕ_{0} \to \sum_{n \in bits (A (t))} 2^{n} = A (t)$
142	141	oveq1d	$⊢ A (t) \in ℕ_{0} \to \sum_{n \in bits (A (t))} 2^{n} t = A (t) t$
143	130 142	syl	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \sum_{n \in bits (A (t))} 2^{n} t = A (t) t$
144	143	sumeq2dv	$⊢ A \in (T \cap R) \to \sum_{t \in A^{-1} [ℕ] \cap J} \sum_{n \in bits (A (t))} 2^{n} t = \sum_{t \in A^{-1} [ℕ] \cap J} A (t) t$
145		vex	$⊢ t \in V$
146		vex	$⊢ n \in V$
147	145 146	op2ndd	$⊢ w = ⟨t, n⟩ \to 2^{nd} (w) = n$
148	147	oveq2d	$⊢ w = ⟨t, n⟩ \to 2^{2^{nd} (w)} = 2^{n}$
149	145 146	op1std	$⊢ w = ⟨t, n⟩ \to 1^{st} (w) = t$
150	148 149	oveq12d	$⊢ w = ⟨t, n⟩ \to 2^{2^{nd} (w)} 1^{st} (w) = 2^{n} t$
151		inss2	$⊢ T \cap R \subseteq R$
152	151	sseli	$⊢ A \in (T \cap R) \to A \in R$
153		cnveq	$⊢ f = A \to f^{-1} = A^{-1}$
154	153	imaeq1d	$⊢ f = A \to f^{-1} [ℕ] = A^{-1} [ℕ]$
155	154	eleq1d	$⊢ f = A \to (f^{-1} [ℕ] \in Fin \leftrightarrow A^{-1} [ℕ] \in Fin)$
156	155 8	elab2g	$⊢ A \in (T \cap R) \to (A \in R \leftrightarrow A^{-1} [ℕ] \in Fin)$
157	152 156	mpbid	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \in Fin$
158		ssfi	$⊢ (A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \cap J \subseteq A^{-1} [ℕ]) \to A^{-1} [ℕ] \cap J \in Fin$
159	157 127 158	sylancl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J \in Fin$
160	133	adantrr	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to t \in ℂ$
161	137 160	mulcld	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2^{n} t \in ℂ$
162	150 159 132 161	fsum2d	$⊢ A \in (T \cap R) \to \sum_{t \in A^{-1} [ℕ] \cap J} \sum_{n \in bits (A (t))} 2^{n} t = \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w)$
163	140 144 162	3eqtr3d	$⊢ A \in (T \cap R) \to \sum_{t \in A^{-1} [ℕ] \cap J} A (t) t = \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w)$
164		inss1	$⊢ T \cap R \subseteq T$
165	164	sseli	$⊢ A \in (T \cap R) \to A \in T$
166	154	sseq1d	$⊢ f = A \to (f^{-1} [ℕ] \subseteq J \leftrightarrow A^{-1} [ℕ] \subseteq J)$
167	166 9	elrab2	$⊢ A \in T \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \subseteq J)$
168	167	simprbi	$⊢ A \in T \to A^{-1} [ℕ] \subseteq J$
169	165 168	syl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq J$
170		dfss2	$⊢ A^{-1} [ℕ] \subseteq J \leftrightarrow A^{-1} [ℕ] \cap J = A^{-1} [ℕ]$
171	169 170	sylib	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J = A^{-1} [ℕ]$
172	171	sumeq1d	$⊢ A \in (T \cap R) \to \sum_{t \in A^{-1} [ℕ] \cap J} A (t) t = \sum_{t \in A^{-1} [ℕ]} A (t) t$
173	163 172	eqtr3d	$⊢ A \in (T \cap R) \to \sum_{w \in ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))} 2^{2^{nd} (w)} 1^{st} (w) = \sum_{t \in A^{-1} [ℕ]} A (t) t$
174	28 118 173	3eqtr2d	$⊢ A \in (T \cap R) \to \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k = \sum_{t \in A^{-1} [ℕ]} A (t) t$
175		fveq2	$⊢ k = t \to A (k) = A (t)$
176		id	$⊢ k = t \to k = t$
177	175 176	oveq12d	$⊢ k = t \to A (k) k = A (t) t$
178	177	cbvsumv	$⊢ \sum_{k \in A^{-1} [ℕ]} A (k) k = \sum_{t \in A^{-1} [ℕ]} A (t) t$
179	174 178	eqtr4di	$⊢ A \in (T \cap R) \to \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k = \sum_{k \in A^{-1} [ℕ]} A (k) k$
180		0nn0	$⊢ 0 \in ℕ_{0}$
181		1nn0	$⊢ 1 \in ℕ_{0}$
182		prssi	$⊢ (0 \in ℕ_{0} \land 1 \in ℕ_{0}) \to \{0, 1\} \subseteq ℕ_{0}$
183	180 181 182	mp2an	$⊢ \{0, 1\} \subseteq ℕ_{0}$
184		fss	$⊢ (G (A) : ℕ ⟶ \{0, 1\} \land \{0, 1\} \subseteq ℕ_{0}) \to G (A) : ℕ ⟶ ℕ_{0}$
185	183 184	mpan2	$⊢ G (A) : ℕ ⟶ \{0, 1\} \to G (A) : ℕ ⟶ ℕ_{0}$
186		nn0ex	$⊢ ℕ_{0} \in V$
187		nnex	$⊢ ℕ \in V$
188	186 187	elmap	$⊢ G (A) \in ({ℕ_{0}}^{ℕ}) \leftrightarrow G (A) : ℕ ⟶ ℕ_{0}$
189	188	biimpri	$⊢ G (A) : ℕ ⟶ ℕ_{0} \to G (A) \in ({ℕ_{0}}^{ℕ})$
190	20 185 189	3syl	$⊢ G (A) \in ({\{0, 1\}}^{ℕ}) \to G (A) \in ({ℕ_{0}}^{ℕ})$
191	190	anim1i	$⊢ (G (A) \in ({\{0, 1\}}^{ℕ}) \land G (A) \in R) \to (G (A) \in ({ℕ_{0}}^{ℕ}) \land G (A) \in R)$
192		elin	$⊢ G (A) \in (({ℕ_{0}}^{ℕ}) \cap R) \leftrightarrow (G (A) \in ({ℕ_{0}}^{ℕ}) \land G (A) \in R)$
193	191 17 192	3imtr4i	$⊢ G (A) \in (({\{0, 1\}}^{ℕ}) \cap R) \to G (A) \in (({ℕ_{0}}^{ℕ}) \cap R)$
194	8 11	eulerpartlemsv2	$⊢ G (A) \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (G (A)) = \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k$
195	16 193 194	3syl	$⊢ A \in (T \cap R) \to S (G (A)) = \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k$
196	120 152	elind	$⊢ A \in (T \cap R) \to A \in (({ℕ_{0}}^{ℕ}) \cap R)$
197	8 11	eulerpartlemsv2	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) = \sum_{k \in A^{-1} [ℕ]} A (k) k$
198	196 197	syl	$⊢ A \in (T \cap R) \to S (A) = \sum_{k \in A^{-1} [ℕ]} A (k) k$
199	179 195 198	3eqtr4d	$⊢ A \in (T \cap R) \to S (G (A)) = S (A)$

Metamath Proof Explorer

Theorem eulerpartlemgs2

Proof