eulerpartlemgvv

Description: Lemma for eulerpart : value of the function G evaluated. (Contributed by Thierry Arnoux, 10-Aug-2018)

	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}))]))$
Assertion	eulerpartlemgvv	$⊢ (A \in (T \cap R) \land B \in ℕ) \to G (A) (B) = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B, 1, 0)$

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	1 2 3 4 5 6 7 8 9 10	eulerpartlemgv	$⊢ A \in (T \cap R) \to G (A) = 𝟙_{ℕ} (F [M (bits \circ ({A ↾}_{J}))])$
12	11	fveq1d	$⊢ A \in (T \cap R) \to G (A) (B) = 𝟙_{ℕ} (F [M (bits \circ ({A ↾}_{J}))]) (B)$
13	12	adantr	$⊢ (A \in (T \cap R) \land B \in ℕ) \to G (A) (B) = 𝟙_{ℕ} (F [M (bits \circ ({A ↾}_{J}))]) (B)$
14		nnex	$⊢ ℕ \in V$
15		imassrn	$⊢ F [M (bits \circ ({A ↾}_{J}))] \subseteq ran F$
16	4 5	oddpwdc	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ$
17		f1of	$⊢ F : J \times ℕ_{0} \underset{1-1 onto}{⟶} ℕ \to F : J \times ℕ_{0} ⟶ ℕ$
18		frn	$⊢ F : J \times ℕ_{0} ⟶ ℕ \to ran F \subseteq ℕ$
19	16 17 18	mp2b	$⊢ ran F \subseteq ℕ$
20	15 19	sstri	$⊢ F [M (bits \circ ({A ↾}_{J}))] \subseteq ℕ$
21		simpr	$⊢ (A \in (T \cap R) \land B \in ℕ) \to B \in ℕ$
22		indfval	$⊢ (ℕ \in V \land F [M (bits \circ ({A ↾}_{J}))] \subseteq ℕ \land B \in ℕ) \to 𝟙_{ℕ} (F [M (bits \circ ({A ↾}_{J}))]) (B) = if (B \in F [M (bits \circ ({A ↾}_{J}))], 1, 0)$
23	14 20 21 22	mp3an12i	$⊢ (A \in (T \cap R) \land B \in ℕ) \to 𝟙_{ℕ} (F [M (bits \circ ({A ↾}_{J}))]) (B) = if (B \in F [M (bits \circ ({A ↾}_{J}))], 1, 0)$
24		ffn	$⊢ F : J \times ℕ_{0} ⟶ ℕ \to F Fn (J \times ℕ_{0})$
25	16 17 24	mp2b	$⊢ F Fn (J \times ℕ_{0})$
26	1 2 3 4 5 6 7 8 9 10	eulerpartlemmf	$⊢ A \in (T \cap R) \to bits \circ ({A ↾}_{J}) \in H$
27	1 2 3 4 5 6 7	eulerpartlem1	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin$
28		f1of	$⊢ M : H \underset{1-1 onto}{⟶} 𝒫 (J \times ℕ_{0}) \cap Fin \to M : H ⟶ 𝒫 (J \times ℕ_{0}) \cap Fin$
29	27 28	ax-mp	$⊢ M : H ⟶ 𝒫 (J \times ℕ_{0}) \cap Fin$
30	29	ffvelrni	$⊢ bits \circ ({A ↾}_{J}) \in H \to M (bits \circ ({A ↾}_{J})) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
31	26 30	syl	$⊢ A \in (T \cap R) \to M (bits \circ ({A ↾}_{J})) \in (𝒫 (J \times ℕ_{0}) \cap Fin)$
32	31	elin1d	$⊢ A \in (T \cap R) \to M (bits \circ ({A ↾}_{J})) \in 𝒫 (J \times ℕ_{0})$
33	32	adantr	$⊢ (A \in (T \cap R) \land B \in ℕ) \to M (bits \circ ({A ↾}_{J})) \in 𝒫 (J \times ℕ_{0})$
34	33	elpwid	$⊢ (A \in (T \cap R) \land B \in ℕ) \to M (bits \circ ({A ↾}_{J})) \subseteq J \times ℕ_{0}$
35		fvelimab	$⊢ (F Fn (J \times ℕ_{0}) \land M (bits \circ ({A ↾}_{J})) \subseteq J \times ℕ_{0}) \to (B \in F [M (bits \circ ({A ↾}_{J}))] \leftrightarrow \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B)$
36	25 34 35	sylancr	$⊢ (A \in (T \cap R) \land B \in ℕ) \to (B \in F [M (bits \circ ({A ↾}_{J}))] \leftrightarrow \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B)$
37	4	ssrab3	$⊢ J \subseteq ℕ$
38		fveq1	$⊢ r = bits \circ ({A ↾}_{J}) \to r (x) = (bits \circ ({A ↾}_{J})) (x)$
39	38	eleq2d	$⊢ r = bits \circ ({A ↾}_{J}) \to (y \in r (x) \leftrightarrow y \in (bits \circ ({A ↾}_{J})) (x))$
40	39	anbi2d	$⊢ r = bits \circ ({A ↾}_{J}) \to ((x \in J \land y \in r (x)) \leftrightarrow (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x)))$
41	40	opabbidv	$⊢ r = bits \circ ({A ↾}_{J}) \to \{⟨x, y⟩ \| (x \in J \land y \in r (x))\} = \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\}$
42	14 37	ssexi	$⊢ J \in V$
43		abid2	$⊢ \{y \| y \in (bits \circ ({A ↾}_{J})) (x)\} = (bits \circ ({A ↾}_{J})) (x)$
44	43	fvexi	$⊢ \{y \| y \in (bits \circ ({A ↾}_{J})) (x)\} \in V$
45	44	a1i	$⊢ x \in J \to \{y \| y \in (bits \circ ({A ↾}_{J})) (x)\} \in V$
46	42 45	opabex3	$⊢ \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\} \in V$
47	46	a1i	$⊢ A \in (T \cap R) \to \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\} \in V$
48	7 41 26 47	fvmptd3	$⊢ A \in (T \cap R) \to M (bits \circ ({A ↾}_{J})) = \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\}$
49		simpl	$⊢ (x = t \land y = n) \to x = t$
50	49	eleq1d	$⊢ (x = t \land y = n) \to (x \in J \leftrightarrow t \in J)$
51		simpr	$⊢ (x = t \land y = n) \to y = n$
52	49	fveq2d	$⊢ (x = t \land y = n) \to (bits \circ ({A ↾}_{J})) (x) = (bits \circ ({A ↾}_{J})) (t)$
53	51 52	eleq12d	$⊢ (x = t \land y = n) \to (y \in (bits \circ ({A ↾}_{J})) (x) \leftrightarrow n \in (bits \circ ({A ↾}_{J})) (t))$
54	50 53	anbi12d	$⊢ (x = t \land y = n) \to ((x \in J \land y \in (bits \circ ({A ↾}_{J})) (x)) \leftrightarrow (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t)))$
55	54	cbvopabv	$⊢ \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\} = \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\}$
56	48 55	eqtrdi	$⊢ A \in (T \cap R) \to M (bits \circ ({A ↾}_{J})) = \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\}$
57	56	eleq2d	$⊢ A \in (T \cap R) \to (w \in M (bits \circ ({A ↾}_{J})) \leftrightarrow w \in \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\})$
58	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)$
59	58	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
60		nn0ex	$⊢ ℕ_{0} \in V$
61	60 14	elmap	$⊢ A \in ({ℕ_{0}}^{ℕ}) \leftrightarrow A : ℕ ⟶ ℕ_{0}$
62	59 61	sylib	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
63		ffun	$⊢ A : ℕ ⟶ ℕ_{0} \to Fun A$
64		funres	$⊢ Fun A \to Fun ({A ↾}_{J})$
65	62 63 64	3syl	$⊢ A \in (T \cap R) \to Fun ({A ↾}_{J})$
66		fssres	$⊢ (A : ℕ ⟶ ℕ_{0} \land J \subseteq ℕ) \to ({A ↾}_{J}) : J ⟶ ℕ_{0}$
67	62 37 66	sylancl	$⊢ A \in (T \cap R) \to ({A ↾}_{J}) : J ⟶ ℕ_{0}$
68		fdm	$⊢ ({A ↾}_{J}) : J ⟶ ℕ_{0} \to dom ({A ↾}_{J}) = J$
69	68	eleq2d	$⊢ ({A ↾}_{J}) : J ⟶ ℕ_{0} \to (t \in dom ({A ↾}_{J}) \leftrightarrow t \in J)$
70	67 69	syl	$⊢ A \in (T \cap R) \to (t \in dom ({A ↾}_{J}) \leftrightarrow t \in J)$
71	70	biimpar	$⊢ (A \in (T \cap R) \land t \in J) \to t \in dom ({A ↾}_{J})$
72		fvco	$⊢ (Fun ({A ↾}_{J}) \land t \in dom ({A ↾}_{J})) \to (bits \circ ({A ↾}_{J})) (t) = bits (({A ↾}_{J}) (t))$
73	65 71 72	syl2an2r	$⊢ (A \in (T \cap R) \land t \in J) \to (bits \circ ({A ↾}_{J})) (t) = bits (({A ↾}_{J}) (t))$
74		fvres	$⊢ t \in J \to ({A ↾}_{J}) (t) = A (t)$
75	74	fveq2d	$⊢ t \in J \to bits (({A ↾}_{J}) (t)) = bits (A (t))$
76	75	adantl	$⊢ (A \in (T \cap R) \land t \in J) \to bits (({A ↾}_{J}) (t)) = bits (A (t))$
77	73 76	eqtrd	$⊢ (A \in (T \cap R) \land t \in J) \to (bits \circ ({A ↾}_{J})) (t) = bits (A (t))$
78	77	eleq2d	$⊢ (A \in (T \cap R) \land t \in J) \to (n \in (bits \circ ({A ↾}_{J})) (t) \leftrightarrow n \in bits (A (t)))$
79	78	pm5.32da	$⊢ A \in (T \cap R) \to ((t \in J \land n \in (bits \circ ({A ↾}_{J})) (t)) \leftrightarrow (t \in J \land n \in bits (A (t))))$
80	79	opabbidv	$⊢ A \in (T \cap R) \to \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\} = \{⟨t, n⟩ \| (t \in J \land n \in bits (A (t)))\}$
81	80	eleq2d	$⊢ A \in (T \cap R) \to (w \in \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\} \leftrightarrow w \in \{⟨t, n⟩ \| (t \in J \land n \in bits (A (t)))\})$
82		elopab	$⊢ w \in \{⟨t, n⟩ \| (t \in J \land n \in bits (A (t)))\} \leftrightarrow \exists t \exists n (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t))))$
83	81 82	bitrdi	$⊢ A \in (T \cap R) \to (w \in \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\} \leftrightarrow \exists t \exists n (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t)))))$
84		ancom	$⊢ (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t)))) \leftrightarrow ((t \in J \land n \in bits (A (t))) \land w = ⟨t, n⟩)$
85		anass	$⊢ ((t \in J \land n \in bits (A (t))) \land w = ⟨t, n⟩) \leftrightarrow (t \in J \land (n \in bits (A (t)) \land w = ⟨t, n⟩))$
86	84 85	bitri	$⊢ (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t)))) \leftrightarrow (t \in J \land (n \in bits (A (t)) \land w = ⟨t, n⟩))$
87	86	2exbii	$⊢ \exists t \exists n (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t)))) \leftrightarrow \exists t \exists n (t \in J \land (n \in bits (A (t)) \land w = ⟨t, n⟩))$
88		df-rex	$⊢ \exists n \in bits (A (t)) w = ⟨t, n⟩ \leftrightarrow \exists n (n \in bits (A (t)) \land w = ⟨t, n⟩)$
89	88	anbi2i	$⊢ (t \in J \land \exists n \in bits (A (t)) w = ⟨t, n⟩) \leftrightarrow (t \in J \land \exists n (n \in bits (A (t)) \land w = ⟨t, n⟩))$
90	89	exbii	$⊢ \exists t (t \in J \land \exists n \in bits (A (t)) w = ⟨t, n⟩) \leftrightarrow \exists t (t \in J \land \exists n (n \in bits (A (t)) \land w = ⟨t, n⟩))$
91		df-rex	$⊢ \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩ \leftrightarrow \exists t (t \in J \land \exists n \in bits (A (t)) w = ⟨t, n⟩)$
92		exdistr	$⊢ \exists t \exists n (t \in J \land (n \in bits (A (t)) \land w = ⟨t, n⟩)) \leftrightarrow \exists t (t \in J \land \exists n (n \in bits (A (t)) \land w = ⟨t, n⟩))$
93	90 91 92	3bitr4i	$⊢ \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩ \leftrightarrow \exists t \exists n (t \in J \land (n \in bits (A (t)) \land w = ⟨t, n⟩))$
94	87 93	bitr4i	$⊢ \exists t \exists n (w = ⟨t, n⟩ \land (t \in J \land n \in bits (A (t)))) \leftrightarrow \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩$
95	83 94	bitrdi	$⊢ A \in (T \cap R) \to (w \in \{⟨t, n⟩ \| (t \in J \land n \in (bits \circ ({A ↾}_{J})) (t))\} \leftrightarrow \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩)$
96	57 95	bitrd	$⊢ A \in (T \cap R) \to (w \in M (bits \circ ({A ↾}_{J})) \leftrightarrow \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩)$
97	96	biimpa	$⊢ (A \in (T \cap R) \land w \in M (bits \circ ({A ↾}_{J}))) \to \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩$
98	97	adantlr	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \to \exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩$
99		fveq2	$⊢ w = ⟨t, n⟩ \to F (w) = F (⟨t, n⟩)$
100	99	adantl	$⊢ ((((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land (t \in J \land n \in bits (A (t)))) \land w = ⟨t, n⟩) \to F (w) = F (⟨t, n⟩)$
101		bitsss	$⊢ bits (A (t)) \subseteq ℕ_{0}$
102	101	sseli	$⊢ n \in bits (A (t)) \to n \in ℕ_{0}$
103	102	anim2i	$⊢ (t \in J \land n \in bits (A (t))) \to (t \in J \land n \in ℕ_{0})$
104	103	ad2antlr	$⊢ ((((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land (t \in J \land n \in bits (A (t)))) \land w = ⟨t, n⟩) \to (t \in J \land n \in ℕ_{0})$
105		opelxp	$⊢ ⟨t, n⟩ \in (J \times ℕ_{0}) \leftrightarrow (t \in J \land n \in ℕ_{0})$
106	4 5	oddpwdcv	$⊢ ⟨t, n⟩ \in (J \times ℕ_{0}) \to F (⟨t, n⟩) = 2^{2^{nd} (⟨t, n⟩)} 1^{st} (⟨t, n⟩)$
107		vex	$⊢ t \in V$
108		vex	$⊢ n \in V$
109	107 108	op2nd	$⊢ 2^{nd} (⟨t, n⟩) = n$
110	109	oveq2i	$⊢ 2^{2^{nd} (⟨t, n⟩)} = 2^{n}$
111	107 108	op1st	$⊢ 1^{st} (⟨t, n⟩) = t$
112	110 111	oveq12i	$⊢ 2^{2^{nd} (⟨t, n⟩)} 1^{st} (⟨t, n⟩) = 2^{n} t$
113	106 112	eqtrdi	$⊢ ⟨t, n⟩ \in (J \times ℕ_{0}) \to F (⟨t, n⟩) = 2^{n} t$
114	105 113	sylbir	$⊢ (t \in J \land n \in ℕ_{0}) \to F (⟨t, n⟩) = 2^{n} t$
115	104 114	syl	$⊢ ((((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land (t \in J \land n \in bits (A (t)))) \land w = ⟨t, n⟩) \to F (⟨t, n⟩) = 2^{n} t$
116	100 115	eqtr2d	$⊢ ((((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land (t \in J \land n \in bits (A (t)))) \land w = ⟨t, n⟩) \to 2^{n} t = F (w)$
117	116	ex	$⊢ (((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land (t \in J \land n \in bits (A (t)))) \to (w = ⟨t, n⟩ \to 2^{n} t = F (w))$
118	117	reximdvva	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \to (\exists t \in J \exists n \in bits (A (t)) w = ⟨t, n⟩ \to \exists t \in J \exists n \in bits (A (t)) 2^{n} t = F (w))$
119	98 118	mpd	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \to \exists t \in J \exists n \in bits (A (t)) 2^{n} t = F (w)$
120		ssrexv	$⊢ J \subseteq ℕ \to (\exists t \in J \exists n \in bits (A (t)) 2^{n} t = F (w) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = F (w))$
121	37 119 120	mpsyl	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = F (w)$
122	121	adantr	$⊢ (((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land F (w) = B) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = F (w)$
123		eqeq2	$⊢ F (w) = B \to (2^{n} t = F (w) \leftrightarrow 2^{n} t = B)$
124	123	rexbidv	$⊢ F (w) = B \to (\exists n \in bits (A (t)) 2^{n} t = F (w) \leftrightarrow \exists n \in bits (A (t)) 2^{n} t = B)$
125	124	adantl	$⊢ (((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land F (w) = B) \to (\exists n \in bits (A (t)) 2^{n} t = F (w) \leftrightarrow \exists n \in bits (A (t)) 2^{n} t = B)$
126	125	rexbidv	$⊢ (((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land F (w) = B) \to (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = F (w) \leftrightarrow \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B)$
127	122 126	mpbid	$⊢ (((A \in (T \cap R) \land B \in ℕ) \land w \in M (bits \circ ({A ↾}_{J}))) \land F (w) = B) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B$
128	127	r19.29an	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B) \to \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B$
129		simp-5l	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to A \in (T \cap R)$
130		simpllr	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to x \in J$
131		simplr	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to y \in bits (A (x))$
132	68	eleq2d	$⊢ ({A ↾}_{J}) : J ⟶ ℕ_{0} \to (x \in dom ({A ↾}_{J}) \leftrightarrow x \in J)$
133	67 132	syl	$⊢ A \in (T \cap R) \to (x \in dom ({A ↾}_{J}) \leftrightarrow x \in J)$
134	133	biimpar	$⊢ (A \in (T \cap R) \land x \in J) \to x \in dom ({A ↾}_{J})$
135		fvco	$⊢ (Fun ({A ↾}_{J}) \land x \in dom ({A ↾}_{J})) \to (bits \circ ({A ↾}_{J})) (x) = bits (({A ↾}_{J}) (x))$
136	65 134 135	syl2an2r	$⊢ (A \in (T \cap R) \land x \in J) \to (bits \circ ({A ↾}_{J})) (x) = bits (({A ↾}_{J}) (x))$
137		fvres	$⊢ x \in J \to ({A ↾}_{J}) (x) = A (x)$
138	137	fveq2d	$⊢ x \in J \to bits (({A ↾}_{J}) (x)) = bits (A (x))$
139	138	adantl	$⊢ (A \in (T \cap R) \land x \in J) \to bits (({A ↾}_{J}) (x)) = bits (A (x))$
140	136 139	eqtrd	$⊢ (A \in (T \cap R) \land x \in J) \to (bits \circ ({A ↾}_{J})) (x) = bits (A (x))$
141	129 130 140	syl2anc	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to (bits \circ ({A ↾}_{J})) (x) = bits (A (x))$
142	131 141	eleqtrrd	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to y \in (bits \circ ({A ↾}_{J})) (x)$
143	48	eleq2d	$⊢ A \in (T \cap R) \to (⟨x, y⟩ \in M (bits \circ ({A ↾}_{J})) \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\})$
144		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))\} \leftrightarrow (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))$
145	143 144	bitrdi	$⊢ A \in (T \cap R) \to (⟨x, y⟩ \in M (bits \circ ({A ↾}_{J})) \leftrightarrow (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x)))$
146	145	biimpar	$⊢ (A \in (T \cap R) \land (x \in J \land y \in (bits \circ ({A ↾}_{J})) (x))) \to ⟨x, y⟩ \in M (bits \circ ({A ↾}_{J}))$
147	129 130 142 146	syl12anc	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to ⟨x, y⟩ \in M (bits \circ ({A ↾}_{J}))$
148		simpr	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to 2^{y} x = B$
149	34	ad4antr	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to M (bits \circ ({A ↾}_{J})) \subseteq J \times ℕ_{0}$
150	149 147	sseldd	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to ⟨x, y⟩ \in (J \times ℕ_{0})$
151		opeq1	$⊢ t = x \to ⟨t, y⟩ = ⟨x, y⟩$
152	151	eleq1d	$⊢ t = x \to (⟨t, y⟩ \in (J \times ℕ_{0}) \leftrightarrow ⟨x, y⟩ \in (J \times ℕ_{0}))$
153	151	fveq2d	$⊢ t = x \to F (⟨t, y⟩) = F (⟨x, y⟩)$
154		oveq2	$⊢ t = x \to 2^{y} t = 2^{y} x$
155	153 154	eqeq12d	$⊢ t = x \to (F (⟨t, y⟩) = 2^{y} t \leftrightarrow F (⟨x, y⟩) = 2^{y} x)$
156	152 155	imbi12d	$⊢ t = x \to ((⟨t, y⟩ \in (J \times ℕ_{0}) \to F (⟨t, y⟩) = 2^{y} t) \leftrightarrow (⟨x, y⟩ \in (J \times ℕ_{0}) \to F (⟨x, y⟩) = 2^{y} x))$
157		opeq2	$⊢ n = y \to ⟨t, n⟩ = ⟨t, y⟩$
158	157	eleq1d	$⊢ n = y \to (⟨t, n⟩ \in (J \times ℕ_{0}) \leftrightarrow ⟨t, y⟩ \in (J \times ℕ_{0}))$
159	157	fveq2d	$⊢ n = y \to F (⟨t, n⟩) = F (⟨t, y⟩)$
160		oveq2	$⊢ n = y \to 2^{n} = 2^{y}$
161	160	oveq1d	$⊢ n = y \to 2^{n} t = 2^{y} t$
162	159 161	eqeq12d	$⊢ n = y \to (F (⟨t, n⟩) = 2^{n} t \leftrightarrow F (⟨t, y⟩) = 2^{y} t)$
163	158 162	imbi12d	$⊢ n = y \to ((⟨t, n⟩ \in (J \times ℕ_{0}) \to F (⟨t, n⟩) = 2^{n} t) \leftrightarrow (⟨t, y⟩ \in (J \times ℕ_{0}) \to F (⟨t, y⟩) = 2^{y} t))$
164	163 113	chvarvv	$⊢ ⟨t, y⟩ \in (J \times ℕ_{0}) \to F (⟨t, y⟩) = 2^{y} t$
165	156 164	chvarvv	$⊢ ⟨x, y⟩ \in (J \times ℕ_{0}) \to F (⟨x, y⟩) = 2^{y} x$
166		eqeq2	$⊢ 2^{y} x = B \to (F (⟨x, y⟩) = 2^{y} x \leftrightarrow F (⟨x, y⟩) = B)$
167	166	biimpa	$⊢ (2^{y} x = B \land F (⟨x, y⟩) = 2^{y} x) \to F (⟨x, y⟩) = B$
168	165 167	sylan2	$⊢ (2^{y} x = B \land ⟨x, y⟩ \in (J \times ℕ_{0})) \to F (⟨x, y⟩) = B$
169	148 150 168	syl2anc	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to F (⟨x, y⟩) = B$
170		fveqeq2	$⊢ w = ⟨x, y⟩ \to (F (w) = B \leftrightarrow F (⟨x, y⟩) = B)$
171	170	rspcev	$⊢ (⟨x, y⟩ \in M (bits \circ ({A ↾}_{J})) \land F (⟨x, y⟩) = B) \to \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B$
172	147 169 171	syl2anc	$⊢ (((((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \land x \in J) \land y \in bits (A (x))) \land 2^{y} x = B) \to \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B$
173		oveq2	$⊢ t = x \to 2^{n} t = 2^{n} x$
174	173	eqeq1d	$⊢ t = x \to (2^{n} t = B \leftrightarrow 2^{n} x = B)$
175	160	oveq1d	$⊢ n = y \to 2^{n} x = 2^{y} x$
176	175	eqeq1d	$⊢ n = y \to (2^{n} x = B \leftrightarrow 2^{y} x = B)$
177	174 176	sylan9bb	$⊢ (t = x \land n = y) \to (2^{n} t = B \leftrightarrow 2^{y} x = B)$
178		simpl	$⊢ (t = x \land n = y) \to t = x$
179	178	fveq2d	$⊢ (t = x \land n = y) \to A (t) = A (x)$
180	179	fveq2d	$⊢ (t = x \land n = y) \to bits (A (t)) = bits (A (x))$
181	177 180	cbvrexdva2	$⊢ t = x \to (\exists n \in bits (A (t)) 2^{n} t = B \leftrightarrow \exists y \in bits (A (x)) 2^{y} x = B)$
182	181	cbvrexvw	$⊢ \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B \leftrightarrow \exists x \in ℕ \exists y \in bits (A (x)) 2^{y} x = B$
183		nfv	$⊢ Ⅎ y A \in (T \cap R)$
184		nfv	$⊢ Ⅎ y x \in ℕ$
185		nfre1	$⊢ Ⅎ y \exists y \in bits (A (x)) 2^{y} x = B$
186	184 185	nfan	$⊢ Ⅎ y (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)$
187	183 186	nfan	$⊢ Ⅎ y (A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B))$
188		simplr	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to x \in ℕ$
189	62	ffvelrnda	$⊢ (A \in (T \cap R) \land x \in ℕ) \to A (x) \in ℕ_{0}$
190	189	adantr	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to A (x) \in ℕ_{0}$
191		elnn0	$⊢ A (x) \in ℕ_{0} \leftrightarrow (A (x) \in ℕ \lor A (x) = 0)$
192	190 191	sylib	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to (A (x) \in ℕ \lor A (x) = 0)$
193		n0i	$⊢ y \in bits (A (x)) \to \neg bits (A (x)) = \emptyset$
194	193	adantl	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to \neg bits (A (x)) = \emptyset$
195		fveq2	$⊢ A (x) = 0 \to bits (A (x)) = bits (0)$
196		0bits	$⊢ bits (0) = \emptyset$
197	195 196	eqtrdi	$⊢ A (x) = 0 \to bits (A (x)) = \emptyset$
198	194 197	nsyl	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to \neg A (x) = 0$
199	192 198	olcnd	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to A (x) \in ℕ$
200	58	simp3bi	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq J$
201	200	sselda	$⊢ (A \in (T \cap R) \land n \in A^{-1} [ℕ]) \to n \in J$
202		breq2	$⊢ z = n \to (2 ∥ z \leftrightarrow 2 ∥ n)$
203	202	notbid	$⊢ z = n \to (\neg 2 ∥ z \leftrightarrow \neg 2 ∥ n)$
204	203 4	elrab2	$⊢ n \in J \leftrightarrow (n \in ℕ \land \neg 2 ∥ n)$
205	204	simprbi	$⊢ n \in J \to \neg 2 ∥ n$
206	201 205	syl	$⊢ (A \in (T \cap R) \land n \in A^{-1} [ℕ]) \to \neg 2 ∥ n$
207	206	ralrimiva	$⊢ A \in (T \cap R) \to \forall n \in A^{-1} [ℕ] \neg 2 ∥ n$
208		ffn	$⊢ A : ℕ ⟶ ℕ_{0} \to A Fn ℕ$
209		elpreima	$⊢ A Fn ℕ \to (n \in A^{-1} [ℕ] \leftrightarrow (n \in ℕ \land A (n) \in ℕ))$
210	62 208 209	3syl	$⊢ A \in (T \cap R) \to (n \in A^{-1} [ℕ] \leftrightarrow (n \in ℕ \land A (n) \in ℕ))$
211	210	imbi1d	$⊢ A \in (T \cap R) \to ((n \in A^{-1} [ℕ] \to \neg 2 ∥ n) \leftrightarrow ((n \in ℕ \land A (n) \in ℕ) \to \neg 2 ∥ n))$
212		impexp	$⊢ ((n \in ℕ \land A (n) \in ℕ) \to \neg 2 ∥ n) \leftrightarrow (n \in ℕ \to (A (n) \in ℕ \to \neg 2 ∥ n))$
213	211 212	bitrdi	$⊢ A \in (T \cap R) \to ((n \in A^{-1} [ℕ] \to \neg 2 ∥ n) \leftrightarrow (n \in ℕ \to (A (n) \in ℕ \to \neg 2 ∥ n)))$
214	213	ralbidv2	$⊢ A \in (T \cap R) \to (\forall n \in A^{-1} [ℕ] \neg 2 ∥ n \leftrightarrow \forall n \in ℕ (A (n) \in ℕ \to \neg 2 ∥ n))$
215	207 214	mpbid	$⊢ A \in (T \cap R) \to \forall n \in ℕ (A (n) \in ℕ \to \neg 2 ∥ n)$
216		fveq2	$⊢ x = n \to A (x) = A (n)$
217	216	eleq1d	$⊢ x = n \to (A (x) \in ℕ \leftrightarrow A (n) \in ℕ)$
218		breq2	$⊢ x = n \to (2 ∥ x \leftrightarrow 2 ∥ n)$
219	218	notbid	$⊢ x = n \to (\neg 2 ∥ x \leftrightarrow \neg 2 ∥ n)$
220	217 219	imbi12d	$⊢ x = n \to ((A (x) \in ℕ \to \neg 2 ∥ x) \leftrightarrow (A (n) \in ℕ \to \neg 2 ∥ n))$
221	220	cbvralvw	$⊢ \forall x \in ℕ (A (x) \in ℕ \to \neg 2 ∥ x) \leftrightarrow \forall n \in ℕ (A (n) \in ℕ \to \neg 2 ∥ n)$
222	215 221	sylibr	$⊢ A \in (T \cap R) \to \forall x \in ℕ (A (x) \in ℕ \to \neg 2 ∥ x)$
223	222	r19.21bi	$⊢ (A \in (T \cap R) \land x \in ℕ) \to (A (x) \in ℕ \to \neg 2 ∥ x)$
224	223	imp	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land A (x) \in ℕ) \to \neg 2 ∥ x$
225	199 224	syldan	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to \neg 2 ∥ x$
226		breq2	$⊢ z = x \to (2 ∥ z \leftrightarrow 2 ∥ x)$
227	226	notbid	$⊢ z = x \to (\neg 2 ∥ z \leftrightarrow \neg 2 ∥ x)$
228	227 4	elrab2	$⊢ x \in J \leftrightarrow (x \in ℕ \land \neg 2 ∥ x)$
229	188 225 228	sylanbrc	$⊢ ((A \in (T \cap R) \land x \in ℕ) \land y \in bits (A (x))) \to x \in J$
230	229	adantlrr	$⊢ ((A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)) \land y \in bits (A (x))) \to x \in J$
231	230	adantr	$⊢ (((A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)) \land y \in bits (A (x))) \land 2^{y} x = B) \to x \in J$
232		simprr	$⊢ (A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)) \to \exists y \in bits (A (x)) 2^{y} x = B$
233	187 231 232	r19.29af	$⊢ (A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)) \to x \in J$
234	233 232	jca	$⊢ (A \in (T \cap R) \land (x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B)) \to (x \in J \land \exists y \in bits (A (x)) 2^{y} x = B)$
235	234	ex	$⊢ A \in (T \cap R) \to ((x \in ℕ \land \exists y \in bits (A (x)) 2^{y} x = B) \to (x \in J \land \exists y \in bits (A (x)) 2^{y} x = B))$
236	235	reximdv2	$⊢ A \in (T \cap R) \to (\exists x \in ℕ \exists y \in bits (A (x)) 2^{y} x = B \to \exists x \in J \exists y \in bits (A (x)) 2^{y} x = B)$
237	236	imp	$⊢ (A \in (T \cap R) \land \exists x \in ℕ \exists y \in bits (A (x)) 2^{y} x = B) \to \exists x \in J \exists y \in bits (A (x)) 2^{y} x = B$
238	237	adantlr	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land \exists x \in ℕ \exists y \in bits (A (x)) 2^{y} x = B) \to \exists x \in J \exists y \in bits (A (x)) 2^{y} x = B$
239	182 238	sylan2b	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \to \exists x \in J \exists y \in bits (A (x)) 2^{y} x = B$
240	172 239	r19.29vva	$⊢ ((A \in (T \cap R) \land B \in ℕ) \land \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B) \to \exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B$
241	128 240	impbida	$⊢ (A \in (T \cap R) \land B \in ℕ) \to (\exists w \in M (bits \circ ({A ↾}_{J})) F (w) = B \leftrightarrow \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B)$
242	36 241	bitrd	$⊢ (A \in (T \cap R) \land B \in ℕ) \to (B \in F [M (bits \circ ({A ↾}_{J}))] \leftrightarrow \exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B)$
243	242	ifbid	$⊢ (A \in (T \cap R) \land B \in ℕ) \to if (B \in F [M (bits \circ ({A ↾}_{J}))], 1, 0) = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B, 1, 0)$
244	13 23 243	3eqtrd	$⊢ (A \in (T \cap R) \land B \in ℕ) \to G (A) (B) = if (\exists t \in ℕ \exists n \in bits (A (t)) 2^{n} t = B, 1, 0)$

Metamath Proof Explorer

Theorem eulerpartlemgvv

Proof