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	ffvelrni	$⊢ 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	mulid2d	$⊢ 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	19 20	syl	$⊢ A \in (T \cap R) \to G (A) : ℕ ⟶ \{0, 1\}$
50		ffn	$⊢ G (A) : ℕ ⟶ \{0, 1\} \to G (A) Fn ℕ$
51		elpreima	$⊢ G (A) Fn ℕ \to (k \in {G (A)}^{-1} [ℕ] \leftrightarrow (k \in ℕ \land G (A) (k) \in ℕ))$
52	49 50 51	3syl	$⊢ A \in (T \cap R) \to (k \in {G (A)}^{-1} [ℕ] \leftrightarrow (k \in ℕ \land G (A) (k) \in ℕ))$
53	52	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 ℕ))$
54	42 48 53	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} [ℕ]$
55	54	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} [ℕ])$
56	55	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} [ℕ]$
57		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$
58	41 56 57	syl2anc	$⊢ A \in (T \cap R) \to \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \in Fin$
59		cnvexg	$⊢ A \in (T \cap R) \to A^{-1} \in V$
60		imaexg	$⊢ A^{-1} \in V \to A^{-1} [ℕ] \in V$
61		inex1g	$⊢ A^{-1} [ℕ] \in V \to A^{-1} [ℕ] \cap J \in V$
62	59 60 61	3syl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J \in V$
63		snex	$⊢ \{t\} \in V$
64		fvex	$⊢ bits (A (t)) \in V$
65	63 64	xpex	$⊢ \{t\} \times bits (A (t)) \in V$
66	65	rgenw	$⊢ \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \in V$
67		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$
68	62 66 67	sylancl	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in V$
69		eqid	$⊢ ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) = ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t)))$
70	1 2 3 4 5 6 7 8 9 10 69	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\}$
71		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\}$
72	68 70 71	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\}$
73		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$
74	58 72 73	syl2anc	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \in Fin$
75		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)$
76	75	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)$
77		inss2	$⊢ A^{-1} [ℕ] \cap J \subseteq J$
78		simpr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in (A^{-1} [ℕ] \cap J)$
79	77 78	sselid	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in J$
80	79	snssd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \{t\} \subseteq J$
81		bitsss	$⊢ bits (A (t)) \subseteq ℕ_{0}$
82		xpss12	$⊢ (\{t\} \subseteq J \land bits (A (t)) \subseteq ℕ_{0}) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
83	80 81 82	sylancl	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
84	83	ralrimiva	$⊢ A \in (T \cap R) \to \forall t \in (A^{-1} [ℕ] \cap J) \{t\} \times bits (A (t)) \subseteq J \times ℕ_{0}$
85		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}$
86	84 85	sylibr	$⊢ A \in (T \cap R) \to ⋃_{t \in A^{-1} [ℕ] \cap J} (\{t\} \times bits (A (t))) \subseteq J \times ℕ_{0}$
87	86	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})$
88	4 5	oddpwdcv	$⊢ w \in (J \times ℕ_{0}) \to F (w) = 2^{2^{nd} (w)} 1^{st} (w)$
89	87 88	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)$
90	76 89	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)$
91	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 ℂ$
92	40 74 70 90 91	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)$
93	39 92	syl5eq	$⊢ 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)$
94		ax-1cn	$⊢ 1 \in ℂ$
95		0cn	$⊢ 0 \in ℂ$
96	94 95	ifcli	$⊢ if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = k, 1, 0) \in ℂ$
97	96	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 ℂ$
98		ssrab2	$⊢ \{m \in ℕ \| \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = m\} \subseteq ℕ$
99		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\}$
100	98 99	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 ℕ$
101	100	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 ℂ$
102	97 101	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 ℂ$
103		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\})$
104	103	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\}$
105	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 ℕ$
106	105	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 ℕ$
107	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)$
108		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)$
109	107 108	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)$
110	104 106 109	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$
111	110	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$
112	111	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$
113		nnsscn	$⊢ ℕ \subseteq ℂ$
114	105 113	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 ℂ$
115	114	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 ℂ$
116	115	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$
117	112 116	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$
118	56 102 117 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$
119	93 118	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$
120	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)$
121	120	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
122		elmapi	$⊢ A \in ({ℕ_{0}}^{ℕ}) \to A : ℕ ⟶ ℕ_{0}$
123	121 122	syl	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
124	123	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A : ℕ ⟶ ℕ_{0}$
125		cnvimass	$⊢ A^{-1} [ℕ] \subseteq dom A$
126	125 123	fssdm	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq ℕ$
127	126	adantr	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A^{-1} [ℕ] \subseteq ℕ$
128		inss1	$⊢ A^{-1} [ℕ] \cap J \subseteq A^{-1} [ℕ]$
129	128 78	sselid	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in A^{-1} [ℕ]$
130	127 129	sseldd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in ℕ$
131	124 130	ffvelrnd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to A (t) \in ℕ_{0}$
132		bitsfi	$⊢ A (t) \in ℕ_{0} \to bits (A (t)) \in Fin$
133	131 132	syl	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to bits (A (t)) \in Fin$
134	130	nncnd	$⊢ (A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \to t \in ℂ$
135		2cnd	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2 \in ℂ$
136		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))$
137	81 136	sselid	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to n \in ℕ_{0}$
138	135 137	expcld	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2^{n} \in ℂ$
139	138	anassrs	$⊢ ((A \in (T \cap R) \land t \in (A^{-1} [ℕ] \cap J)) \land n \in bits (A (t))) \to 2^{n} \in ℂ$
140	133 134 139	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$
141	140	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$
142		bitsinv1	$⊢ A (t) \in ℕ_{0} \to \sum_{n \in bits (A (t))} 2^{n} = A (t)$
143	142	oveq1d	$⊢ A (t) \in ℕ_{0} \to \sum_{n \in bits (A (t))} 2^{n} t = A (t) t$
144	131 143	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$
145	144	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$
146		vex	$⊢ t \in V$
147		vex	$⊢ n \in V$
148	146 147	op2ndd	$⊢ w = ⟨t, n⟩ \to 2^{nd} (w) = n$
149	148	oveq2d	$⊢ w = ⟨t, n⟩ \to 2^{2^{nd} (w)} = 2^{n}$
150	146 147	op1std	$⊢ w = ⟨t, n⟩ \to 1^{st} (w) = t$
151	149 150	oveq12d	$⊢ w = ⟨t, n⟩ \to 2^{2^{nd} (w)} 1^{st} (w) = 2^{n} t$
152		inss2	$⊢ T \cap R \subseteq R$
153	152	sseli	$⊢ A \in (T \cap R) \to A \in R$
154		cnveq	$⊢ f = A \to f^{-1} = A^{-1}$
155	154	imaeq1d	$⊢ f = A \to f^{-1} [ℕ] = A^{-1} [ℕ]$
156	155	eleq1d	$⊢ f = A \to (f^{-1} [ℕ] \in Fin \leftrightarrow A^{-1} [ℕ] \in Fin)$
157	156 8	elab2g	$⊢ A \in (T \cap R) \to (A \in R \leftrightarrow A^{-1} [ℕ] \in Fin)$
158	153 157	mpbid	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \in Fin$
159		ssfi	$⊢ (A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \cap J \subseteq A^{-1} [ℕ]) \to A^{-1} [ℕ] \cap J \in Fin$
160	158 128 159	sylancl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J \in Fin$
161	134	adantrr	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to t \in ℂ$
162	138 161	mulcld	$⊢ (A \in (T \cap R) \land (t \in (A^{-1} [ℕ] \cap J) \land n \in bits (A (t)))) \to 2^{n} t \in ℂ$
163	151 160 133 162	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)$
164	141 145 163	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)$
165		inss1	$⊢ T \cap R \subseteq T$
166	165	sseli	$⊢ A \in (T \cap R) \to A \in T$
167	155	sseq1d	$⊢ f = A \to (f^{-1} [ℕ] \subseteq J \leftrightarrow A^{-1} [ℕ] \subseteq J)$
168	167 9	elrab2	$⊢ A \in T \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \subseteq J)$
169	168	simprbi	$⊢ A \in T \to A^{-1} [ℕ] \subseteq J$
170	166 169	syl	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq J$
171		df-ss	$⊢ A^{-1} [ℕ] \subseteq J \leftrightarrow A^{-1} [ℕ] \cap J = A^{-1} [ℕ]$
172	170 171	sylib	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \cap J = A^{-1} [ℕ]$
173	172	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$
174	164 173	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$
175	28 119 174	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$
176		fveq2	$⊢ k = t \to A (k) = A (t)$
177		id	$⊢ k = t \to k = t$
178	176 177	oveq12d	$⊢ k = t \to A (k) k = A (t) t$
179	178	cbvsumv	$⊢ \sum_{k \in A^{-1} [ℕ]} A (k) k = \sum_{t \in A^{-1} [ℕ]} A (t) t$
180	175 179	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$
181		0nn0	$⊢ 0 \in ℕ_{0}$
182		1nn0	$⊢ 1 \in ℕ_{0}$
183		prssi	$⊢ (0 \in ℕ_{0} \land 1 \in ℕ_{0}) \to \{0, 1\} \subseteq ℕ_{0}$
184	181 182 183	mp2an	$⊢ \{0, 1\} \subseteq ℕ_{0}$
185		fss	$⊢ (G (A) : ℕ ⟶ \{0, 1\} \land \{0, 1\} \subseteq ℕ_{0}) \to G (A) : ℕ ⟶ ℕ_{0}$
186	184 185	mpan2	$⊢ G (A) : ℕ ⟶ \{0, 1\} \to G (A) : ℕ ⟶ ℕ_{0}$
187		nn0ex	$⊢ ℕ_{0} \in V$
188		nnex	$⊢ ℕ \in V$
189	187 188	elmap	$⊢ G (A) \in ({ℕ_{0}}^{ℕ}) \leftrightarrow G (A) : ℕ ⟶ ℕ_{0}$
190	189	biimpri	$⊢ G (A) : ℕ ⟶ ℕ_{0} \to G (A) \in ({ℕ_{0}}^{ℕ})$
191	20 186 190	3syl	$⊢ G (A) \in ({\{0, 1\}}^{ℕ}) \to G (A) \in ({ℕ_{0}}^{ℕ})$
192	191	anim1i	$⊢ (G (A) \in ({\{0, 1\}}^{ℕ}) \land G (A) \in R) \to (G (A) \in ({ℕ_{0}}^{ℕ}) \land G (A) \in R)$
193		elin	$⊢ G (A) \in (({ℕ_{0}}^{ℕ}) \cap R) \leftrightarrow (G (A) \in ({ℕ_{0}}^{ℕ}) \land G (A) \in R)$
194	192 17 193	3imtr4i	$⊢ G (A) \in (({\{0, 1\}}^{ℕ}) \cap R) \to G (A) \in (({ℕ_{0}}^{ℕ}) \cap R)$
195	8 11	eulerpartlemsv2	$⊢ G (A) \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (G (A)) = \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k$
196	16 194 195	3syl	$⊢ A \in (T \cap R) \to S (G (A)) = \sum_{k \in {G (A)}^{-1} [ℕ]} G (A) (k) k$
197	121 153	elind	$⊢ A \in (T \cap R) \to A \in (({ℕ_{0}}^{ℕ}) \cap R)$
198	8 11	eulerpartlemsv2	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) = \sum_{k \in A^{-1} [ℕ]} A (k) k$
199	197 198	syl	$⊢ A \in (T \cap R) \to S (A) = \sum_{k \in A^{-1} [ℕ]} A (k) k$
200	180 196 199	3eqtr4d	$⊢ A \in (T \cap R) \to S (G (A)) = S (A)$

Metamath Proof Explorer

Theorem eulerpartlemgs2

Proof