Theorem eulerpartlemgvv 28834

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

Hypotheses

Ref	Expression
eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j	|- J = { z e. NN | -. 2 || z }
eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )

Assertion

Ref	Expression
eulerpartlemgvv	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = if ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B , 1 , 0 ) )

Distinct variable groups:   f, k, n, t, x, y, z   f, o, r, A   o, F   H, r   f, J   n, o, r, J, x, y   o, M   f, N   g, n, P   R, o   T, o   t, A, n, x, y   B, n, t, x, y   n, F, t, x, y   t, J   n, M, t, x, y   R, n   t, r, R, x, y   T, n, r, t, x, y

Allowed substitution hints:   A( z, g, k)   B( z, f, g, k, o, r)   D( x, y, z, t, f, g, k, n, o, r)   P( x, y, z, t, f, k, o, r)   R( z, f, g, k)   T( z, f, g, k)   F( z, f, g, k, r)   G( x, y, z, t, f, g, k, n, o, r)   H( x, y, z, t, f, g, k, n, o)   J( z, g, k)   M( z, f, g, k, r)   N( x, y, z, t, g, k, n, o, r)   O( x, y, z, t, f, g, k, n, o, r)

Proof of Theorem eulerpartlemgvv

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerpart.p	. . . . 5 |- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2		eulerpart.o	. . . . 5 |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3		eulerpart.d	. . . . 5 |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4		eulerpart.j	. . . . 5 |- J = { z e. NN | -. 2 || z }
5		eulerpart.f	. . . . 5 |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6		eulerpart.h	. . . . 5 |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7		eulerpart.m	. . . . 5 |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8		eulerpart.r	. . . . 5 |- R = { f | ( `' f " NN ) e. Fin }
9		eulerpart.t	. . . . 5 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10		eulerpart.g	. . . . 5 |- G = ( o e. ( T i^i R ) |-> ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( o |` J ) ) ) ) ) )
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemgv 28831	. . . 4 |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d 5853	. . 3 |- ( A e. ( T i^i R ) -> ( ( G ` A ) ` B ) = ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) )
13	12	adantr 465	. 2 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) )
14		nnex 10584	. . . 4 |- NN e. _V
15	14	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> NN e. _V )
16		imassrn 5170	. . . . 5 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ ran F
17	4, 5	oddpwdc 28812	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
18		f1of 5801	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
19		frn 5722	. . . . . 6 |- ( F : ( J X. NN0 ) --> NN -> ran F C_ NN )
20	17, 18, 19	mp2b 10	. . . . 5 |- ran F C_ NN
21	16, 20	sstri 3453	. . . 4 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ NN
22	21	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ NN )
23		simpr 461	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> B e. NN )
24		indfval 28477	. . 3 |- ( ( NN e. _V /\ ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ NN /\ B e. NN ) -> ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) = if ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) , 1 , 0 ) )
25	15, 22, 23, 24	syl3anc 1232	. 2 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) = if ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) , 1 , 0 ) )
26		ffn 5716	. . . . . 6 |- ( F : ( J X. NN0 ) --> NN -> F Fn ( J X. NN0 ) )
27	17, 18, 26	mp2b 10	. . . . 5 |- F Fn ( J X. NN0 )
28		inss1 3661	. . . . . . . 8 |- ( ~P ( J X. NN0 ) i^i Fin ) C_ ~P ( J X. NN0 )
29	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	eulerpartlemmf 28833	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
30	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 28825	. . . . . . . . . . 11 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
31		f1of 5801	. . . . . . . . . . 11 |- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M : H --> ( ~P ( J X. NN0 ) i^i Fin ) )
32	30, 31	ax-mp 5	. . . . . . . . . 10 |- M : H --> ( ~P ( J X. NN0 ) i^i Fin )
33	32	ffvelrni 6010	. . . . . . . . 9 |- ( (bits o. ( A |` J ) ) e. H -> ( M ` (bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
34	29, 33	syl 17	. . . . . . . 8 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
35	28, 34	sseldi 3442	. . . . . . 7 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
36	35	adantr 465	. . . . . 6 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
37	36	elpwid 3967	. . . . 5 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
38		fvelimab 5907	. . . . 5 |- ( ( F Fn ( J X. NN0 ) /\ ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) ) -> ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) <-> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B ) )
39	27, 37, 38	sylancr 663	. . . 4 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) <-> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B ) )
40		ssrab2 3526	. . . . . . . . . 10 |- { z e. NN | -. 2 || z } C_ NN
41	4, 40	eqsstri 3474	. . . . . . . . 9 |- J C_ NN
42	7	a1i 11	. . . . . . . . . . . . . . . 16 |- ( A e. ( T i^i R ) -> M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) )
43		fveq1 5850	. . . . . . . . . . . . . . . . . . . 20 |- ( r = (bits o. ( A |` J ) ) -> ( r ` x ) = ( (bits o. ( A |` J ) ) ` x ) )
44	43	eleq2d 2474	. . . . . . . . . . . . . . . . . . 19 |- ( r = (bits o. ( A |` J ) ) -> ( y e. ( r ` x ) <-> y e. ( (bits o. ( A |` J ) ) ` x ) ) )
45	44	anbi2d 704	. . . . . . . . . . . . . . . . . 18 |- ( r = (bits o. ( A |` J ) ) -> ( ( x e. J /\ y e. ( r ` x ) ) <-> ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) ) )
46	45	opabbidv 4460	. . . . . . . . . . . . . . . . 17 |- ( r = (bits o. ( A |` J ) ) -> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } = { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } )
47	46	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( A e. ( T i^i R ) /\ r = (bits o. ( A |` J ) ) ) -> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } = { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } )
48	14, 41	ssexi 4541	. . . . . . . . . . . . . . . . . 18 |- J e. _V
49		abid2 2544	. . . . . . . . . . . . . . . . . . . 20 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } = ( (bits o. ( A |` J ) ) ` x )
50		fvex 5861	. . . . . . . . . . . . . . . . . . . 20 |- ( (bits o. ( A |` J ) ) ` x ) e. _V
51	49, 50	eqeltri 2488	. . . . . . . . . . . . . . . . . . 19 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } e. _V
52	51	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x e. J -> { y | y e. ( (bits o. ( A |` J ) ) ` x ) } e. _V )
53	48, 52	opabex3 6765	. . . . . . . . . . . . . . . . 17 |- { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } e. _V
54	53	a1i 11	. . . . . . . . . . . . . . . 16 |- ( A e. ( T i^i R ) -> { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } e. _V )
55	42, 47, 29, 54	fvmptd 5940	. . . . . . . . . . . . . . 15 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) = { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } )
56		simpl 457	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> x = t )
57	56	eleq1d 2473	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
58		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> y = n )
59	56	fveq2d 5855	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( (bits o. ( A |` J ) ) ` x ) = ( (bits o. ( A |` J ) ) ` t ) )
60	58, 59	eleq12d 2486	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( y e. ( (bits o. ( A |` J ) ) ` x ) <-> n e. ( (bits o. ( A |` J ) ) ` t ) ) )
61	57, 60	anbi12d 711	. . . . . . . . . . . . . . . 16 |- ( ( x = t /\ y = n ) -> ( ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) <-> ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) ) )
62	61	cbvopabv 4466	. . . . . . . . . . . . . . 15 |- { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } = { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) }
63	55, 62	syl6eq 2461	. . . . . . . . . . . . . 14 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) = { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } )
64	63	eleq2d 2474	. . . . . . . . . . . . 13 |- ( A e. ( T i^i R ) -> ( w e. ( M ` (bits o. ( A |` J ) ) ) <-> w e. { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } ) )
65	1, 2, 3, 4, 5, 6, 7, 8, 9	eulerpartlemt0 28827	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
66	65	simp1bi 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
67		nn0ex 10844	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- NN0 e. _V
68	67, 14	elmap 7487	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
69	66, 68	sylib 198	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> A : NN --> NN0 )
70		ffun 5718	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A : NN --> NN0 -> Fun A )
71		funres 5610	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Fun A -> Fun ( A |` J ) )
72	69, 70, 71	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A e. ( T i^i R ) -> Fun ( A |` J ) )
73	72	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> Fun ( A |` J ) )
74		fssres 5736	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
75	69, 41, 74	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
76		fdm 5720	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
77	76	eleq2d 2474	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A |` J ) : J --> NN0 -> ( t e. dom ( A |` J ) <-> t e. J ) )
78	75, 77	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A e. ( T i^i R ) -> ( t e. dom ( A |` J ) <-> t e. J ) )
79	78	biimpar 485	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> t e. dom ( A |` J ) )
80		fvco 5927	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Fun ( A |` J ) /\ t e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
81	73, 79, 80	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
82		fvres 5865	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
83	82	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . 21 |- ( t e. J -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
84	83	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
85	81, 84	eqtrd 2445	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( A ` t ) ) )
86	85	eleq2d 2474	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( n e. ( (bits o. ( A |` J ) ) ` t ) <-> n e. (bits ` ( A ` t ) ) ) )
87	86	pm5.32da 641	. . . . . . . . . . . . . . . . 17 |- ( A e. ( T i^i R ) -> ( ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) <-> ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) )
88	87	opabbidv 4460	. . . . . . . . . . . . . . . 16 |- ( A e. ( T i^i R ) -> { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } = { <. t , n >. | ( t e. J /\ n e. (bits ` ( A ` t ) ) ) } )
89	88	eleq2d 2474	. . . . . . . . . . . . . . 15 |- ( A e. ( T i^i R ) -> ( w e. { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } <-> w e. { <. t , n >. | ( t e. J /\ n e. (bits ` ( A ` t ) ) ) } ) )
90		elopab 4700	. . . . . . . . . . . . . . 15 |- ( w e. { <. t , n >. | ( t e. J /\ n e. (bits ` ( A ` t ) ) ) } <-> E. t E. n ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) )
91	89, 90	syl6bb 263	. . . . . . . . . . . . . 14 |- ( A e. ( T i^i R ) -> ( w e. { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } <-> E. t E. n ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) ) )
92		ancom 450	. . . . . . . . . . . . . . . . 17 |- ( ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) )
93		anass 649	. . . . . . . . . . . . . . . . 17 |- ( ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) <-> ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
94	92, 93	bitri 251	. . . . . . . . . . . . . . . 16 |- ( ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
95	94	2exbii 1691	. . . . . . . . . . . . . . 15 |- ( E. t E. n ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> E. t E. n ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
96		df-rex 2762	. . . . . . . . . . . . . . . . . 18 |- ( E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) )
97	96	anbi2i 694	. . . . . . . . . . . . . . . . 17 |- ( ( t e. J /\ E. n e. (bits ` ( A ` t ) ) w = <. t , n >. ) <-> ( t e. J /\ E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
98	97	exbii 1690	. . . . . . . . . . . . . . . 16 |- ( E. t ( t e. J /\ E. n e. (bits ` ( A ` t ) ) w = <. t , n >. ) <-> E. t ( t e. J /\ E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
99		df-rex 2762	. . . . . . . . . . . . . . . 16 |- ( E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. t ( t e. J /\ E. n e. (bits ` ( A ` t ) ) w = <. t , n >. ) )
100		exdistr 1802	. . . . . . . . . . . . . . . 16 |- ( E. t E. n ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) <-> E. t ( t e. J /\ E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
101	98, 99, 100	3bitr4i 279	. . . . . . . . . . . . . . 15 |- ( E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. t E. n ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
102	95, 101	bitr4i 254	. . . . . . . . . . . . . 14 |- ( E. t E. n ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. )
103	91, 102	syl6bb 263	. . . . . . . . . . . . 13 |- ( A e. ( T i^i R ) -> ( w e. { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } <-> E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. ) )
104	64, 103	bitrd 255	. . . . . . . . . . . 12 |- ( A e. ( T i^i R ) -> ( w e. ( M ` (bits o. ( A |` J ) ) ) <-> E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. ) )
105	104	biimpa 484	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) -> E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. )
106	105	adantlr 715	. . . . . . . . . 10 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) -> E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. )
107		fveq2 5851	. . . . . . . . . . . . . . . 16 |- ( w = <. t , n >. -> ( F ` w ) = ( F ` <. t , n >. ) )
108	107	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) /\ w = <. t , n >. ) -> ( F ` w ) = ( F ` <. t , n >. ) )
109		bitsss 14287	. . . . . . . . . . . . . . . . . . 19 |- (bits ` ( A ` t ) ) C_ NN0
110	109	sseli 3440	. . . . . . . . . . . . . . . . . 18 |- ( n e. (bits ` ( A ` t ) ) -> n e. NN0 )
111	110	anim2i 569	. . . . . . . . . . . . . . . . 17 |- ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) -> ( t e. J /\ n e. NN0 ) )
112	111	ad2antlr 727	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) /\ w = <. t , n >. ) -> ( t e. J /\ n e. NN0 ) )
113		opelxp 4855	. . . . . . . . . . . . . . . . 17 |- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
114	4, 5	oddpwdcv 28813	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
115		vex 3064	. . . . . . . . . . . . . . . . . . . . 21 |- t e. _V
116		vex 3064	. . . . . . . . . . . . . . . . . . . . 21 |- n e. _V
117	115, 116	op2nd 6795	. . . . . . . . . . . . . . . . . . . 20 |- ( 2nd ` <. t , n >. ) = n
118	117	oveq2i 6291	. . . . . . . . . . . . . . . . . . 19 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
119	115, 116	op1st 6794	. . . . . . . . . . . . . . . . . . 19 |- ( 1st ` <. t , n >. ) = t
120	118, 119	oveq12i 6292	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
121	114, 120	syl6eq 2461	. . . . . . . . . . . . . . . . 17 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
122	113, 121	sylbir 215	. . . . . . . . . . . . . . . 16 |- ( ( t e. J /\ n e. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
123	112, 122	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) /\ w = <. t , n >. ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
124	108, 123	eqtr2d 2446	. . . . . . . . . . . . . 14 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) /\ w = <. t , n >. ) -> ( ( 2 ^ n ) x. t ) = ( F ` w ) )
125	124	ex 434	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) -> ( w = <. t , n >. -> ( ( 2 ^ n ) x. t ) = ( F ` w ) ) )
126	125	anassrs 648	. . . . . . . . . . . 12 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ t e. J ) /\ n e. (bits ` ( A ` t ) ) ) -> ( w = <. t , n >. -> ( ( 2 ^ n ) x. t ) = ( F ` w ) ) )
127	126	reximdva 2881	. . . . . . . . . . 11 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ t e. J ) -> ( E. n e. (bits ` ( A ` t ) ) w = <. t , n >. -> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) ) )
128	127	reximdva 2881	. . . . . . . . . 10 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) -> ( E. t e. J E. n e. (bits ` ( A ` t ) ) w = <. t , n >. -> E. t e. J E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) ) )
129	106, 128	mpd 15	. . . . . . . . 9 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) -> E. t e. J E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) )
130		ssrexv 3506	. . . . . . . . 9 |- ( J C_ NN -> ( E. t e. J E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) ) )
131	41, 129, 130	mpsyl 64	. . . . . . . 8 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) )
132	131	adantr 465	. . . . . . 7 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( F ` w ) = B ) -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) )
133		eqeq2 2419	. . . . . . . . . 10 |- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
134	133	rexbidv 2920	. . . . . . . . 9 |- ( ( F ` w ) = B -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) )
135	134	adantl 466	. . . . . . . 8 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( F ` w ) = B ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) )
136	135	rexbidv 2920	. . . . . . 7 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( F ` w ) = B ) -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) )
137	132, 136	mpbid 212	. . . . . 6 |- ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ w e. ( M ` (bits o. ( A |` J ) ) ) ) /\ ( F ` w ) = B ) -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B )
138	137	r19.29an 2950	. . . . 5 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B ) -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B )
139		simp-5l 772	. . . . . . . 8 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> A e. ( T i^i R ) )
140		simpllr 763	. . . . . . . 8 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> x e. J )
141		simplr 756	. . . . . . . . 9 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> y e. (bits ` ( A ` x ) ) )
142	72	adantr 465	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> Fun ( A |` J ) )
143	76	eleq2d 2474	. . . . . . . . . . . . . 14 |- ( ( A |` J ) : J --> NN0 -> ( x e. dom ( A |` J ) <-> x e. J ) )
144	75, 143	syl 17	. . . . . . . . . . . . 13 |- ( A e. ( T i^i R ) -> ( x e. dom ( A |` J ) <-> x e. J ) )
145	144	biimpar 485	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> x e. dom ( A |` J ) )
146		fvco 5927	. . . . . . . . . . . 12 |- ( ( Fun ( A |` J ) /\ x e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
147	142, 145, 146	syl2anc 661	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
148		fvres 5865	. . . . . . . . . . . . 13 |- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
149	148	fveq2d 5855	. . . . . . . . . . . 12 |- ( x e. J -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
150	149	adantl 466	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
151	147, 150	eqtrd 2445	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( A ` x ) ) )
152	139, 140, 151	syl2anc 661	. . . . . . . . 9 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( A ` x ) ) )
153	141, 152	eleqtrrd 2495	. . . . . . . 8 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> y e. ( (bits o. ( A |` J ) ) ` x ) )
154	55	eleq2d 2474	. . . . . . . . . 10 |- ( A e. ( T i^i R ) -> ( <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) <-> <. x , y >. e. { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } ) )
155		opabid 4699	. . . . . . . . . 10 |- ( <. x , y >. e. { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } <-> ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) )
156	154, 155	syl6bb 263	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> ( <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) <-> ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) ) )
157	156	biimpar 485	. . . . . . . 8 |- ( ( A e. ( T i^i R ) /\ ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) ) -> <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) )
158	139, 140, 153, 157	syl12anc 1230	. . . . . . 7 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) )
159		simpr 461	. . . . . . . 8 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> ( ( 2 ^ y ) x. x ) = B )
160	37	ad4antr 732	. . . . . . . . 9 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
161	160, 158	sseldd 3445	. . . . . . . 8 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> <. x , y >. e. ( J X. NN0 ) )
162		opeq1 4161	. . . . . . . . . . . 12 |- ( t = x -> <. t , y >. = <. x , y >. )
163	162	eleq1d 2473	. . . . . . . . . . 11 |- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
164	162	fveq2d 5855	. . . . . . . . . . . 12 |- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
165		oveq2 6288	. . . . . . . . . . . 12 |- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
166	164, 165	eqeq12d 2426	. . . . . . . . . . 11 |- ( t = x -> ( ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) <-> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) )
167	163, 166	imbi12d 320	. . . . . . . . . 10 |- ( t = x -> ( ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) <-> ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) ) )
168		opeq2 4162	. . . . . . . . . . . . 13 |- ( n = y -> <. t , n >. = <. t , y >. )
169	168	eleq1d 2473	. . . . . . . . . . . 12 |- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
170	168	fveq2d 5855	. . . . . . . . . . . . 13 |- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
171		oveq2 6288	. . . . . . . . . . . . . 14 |- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
172	171	oveq1d 6295	. . . . . . . . . . . . 13 |- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
173	170, 172	eqeq12d 2426	. . . . . . . . . . . 12 |- ( n = y -> ( ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) <-> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) )
174	169, 173	imbi12d 320	. . . . . . . . . . 11 |- ( n = y -> ( ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) ) <-> ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) ) )
175	174, 121	chvarv 2043	. . . . . . . . . 10 |- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
176	167, 175	chvarv 2043	. . . . . . . . 9 |- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
177		eqeq2 2419	. . . . . . . . . 10 |- ( ( ( 2 ^ y ) x. x ) = B -> ( ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) <-> ( F ` <. x , y >. ) = B ) )
178	177	biimpa 484	. . . . . . . . 9 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) -> ( F ` <. x , y >. ) = B )
179	176, 178	sylan2 474	. . . . . . . 8 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ <. x , y >. e. ( J X. NN0 ) ) -> ( F ` <. x , y >. ) = B )
180	159, 161, 179	syl2anc 661	. . . . . . 7 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> ( F ` <. x , y >. ) = B )
181		fveq2 5851	. . . . . . . . 9 |- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
182	181	eqeq1d 2406	. . . . . . . 8 |- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
183	182	rspcev 3162	. . . . . . 7 |- ( ( <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) /\ ( F ` <. x , y >. ) = B ) -> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
184	158, 180, 183	syl2anc 661	. . . . . 6 |- ( ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) /\ x e. J ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
185		oveq2 6288	. . . . . . . . . . 11 |- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
186	185	eqeq1d 2406	. . . . . . . . . 10 |- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
187	171	oveq1d 6295	. . . . . . . . . . 11 |- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
188	187	eqeq1d 2406	. . . . . . . . . 10 |- ( n = y -> ( ( ( 2 ^ n ) x. x ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
189	186, 188	sylan9bb 700	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
190		simpl 457	. . . . . . . . . . 11 |- ( ( t = x /\ n = y ) -> t = x )
191	190	fveq2d 5855	. . . . . . . . . 10 |- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
192	191	fveq2d 5855	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> (bits ` ( A ` t ) ) = (bits ` ( A ` x ) ) )
193	189, 192	cbvrexdva2 3041	. . . . . . . 8 |- ( t = x -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B <-> E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
194	193	cbvrexv 3037	. . . . . . 7 |- ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B <-> E. x e. NN E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
195		nfv 1730	. . . . . . . . . . . . . 14 |- F/ y A e. ( T i^i R )
196		nfv 1730	. . . . . . . . . . . . . . 15 |- F/ y x e. NN
197		nfre1 2867	. . . . . . . . . . . . . . 15 |- F/ y E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
198	196, 197	nfan 1958	. . . . . . . . . . . . . 14 |- F/ y ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
199	195, 198	nfan 1958	. . . . . . . . . . . . 13 |- F/ y ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
200		simplr 756	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. NN )
201		n0i 3745	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. (bits ` ( A ` x ) ) -> -. (bits ` ( A ` x ) ) = (/) )
202	201	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. (bits ` ( A ` x ) ) = (/) )
203		fveq2 5851	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (bits ` 0 ) )
204		0bits 14300	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` 0 ) = (/)
205	203, 204	syl6eq 2461	. . . . . . . . . . . . . . . . . . 19 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (/) )
206	202, 205	nsyl 123	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. ( A ` x ) = 0 )
207	69	ffvelrnda 6011	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( A ` x ) e. NN0 )
208	207	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN0 )
209		elnn0 10840	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A ` x ) e. NN0 <-> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
210	208, 209	sylib 198	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
211	210	orcomd 388	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( ( A ` x ) = 0 \/ ( A ` x ) e. NN ) )
212	211	orcanai 916	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) /\ -. ( A ` x ) = 0 ) -> ( A ` x ) e. NN )
213	206, 212	mpdan 668	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN )
214	65	simp3bi 1016	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
215	214	sselda 3444	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
216		breq2 4401	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = n -> ( 2 || z <-> 2 || n ) )
217	216	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
218	217, 4	elrab2 3211	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
219	218	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. J -> -. 2 || n )
220	215, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> -. 2 || n )
221	220	ralrimiva 2820	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
222		ffn 5716	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A : NN --> NN0 -> A Fn NN )
223		elpreima 5987	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A Fn NN -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
224	69, 222, 223	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
225	224	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) ) )
226		impexp 446	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
227	225, 226	syl6bb 263	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) ) )
228	227	ralbidv2 2841	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> ( A. n e. ( `' A " NN ) -. 2 || n <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) ) )
229	221, 228	mpbid 212	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. ( T i^i R ) -> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
230		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( A ` x ) = ( A ` n ) )
231	230	eleq1d 2473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
232		breq2 4401	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( 2 || x <-> 2 || n ) )
233	232	notbid 294	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( -. 2 || x <-> -. 2 || n ) )
234	231, 233	imbi12d 320	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> ( ( ( A ` x ) e. NN -> -. 2 || x ) <-> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
235	234	cbvralv 3036	. . . . . . . . . . . . . . . . . . . 20 |- ( A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
236	229, 235	sylibr 214	. . . . . . . . . . . . . . . . . . 19 |- ( A e. ( T i^i R ) -> A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) )
237	236	r19.21bi 2775	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( ( A ` x ) e. NN -> -. 2 || x ) )
238	237	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ ( A ` x ) e. NN ) -> -. 2 || x )
239	213, 238	syldan 470	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. 2 || x )
240		breq2 4401	. . . . . . . . . . . . . . . . . 18 |- ( z = x -> ( 2 || z <-> 2 || x ) )
241	240	notbid 294	. . . . . . . . . . . . . . . . 17 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
242	241, 4	elrab2 3211	. . . . . . . . . . . . . . . 16 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
243	200, 239, 242	sylanbrc 664	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. J )
244	243	adantlrr 721	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. J )
245	244	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) /\ y e. (bits ` ( A ` x ) ) ) /\ ( ( 2 ^ y ) x. x ) = B ) -> x e. J )
246		simprr 760	. . . . . . . . . . . . 13 |- ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) -> E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
247	199, 245, 246	r19.29af 2949	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) -> x e. J )
248	247, 246	jca 532	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) -> ( x e. J /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
249	248	ex 434	. . . . . . . . . 10 |- ( A e. ( T i^i R ) -> ( ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) -> ( x e. J /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) )
250	249	reximdv2 2877	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> ( E. x e. NN E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B -> E. x e. J E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
251	250	imp 429	. . . . . . . 8 |- ( ( A e. ( T i^i R ) /\ E. x e. NN E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) -> E. x e. J E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
252	251	adantlr 715	. . . . . . 7 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. x e. NN E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) -> E. x e. J E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
253	194, 252	sylan2b 475	. . . . . 6 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) -> E. x e. J E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
254	184, 253	r19.29vva 2953	. . . . 5 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) -> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
255	138, 254	impbida 835	. . . 4 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B <-> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) )
256	39, 255	bitrd 255	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) <-> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B ) )
257	256	ifbid 3909	. 2 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> if ( B e. ( F " ( M ` (bits o. ( A |` J ) ) ) ) , 1 , 0 ) = if ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B , 1 , 0 ) )
258	13, 25, 257	3eqtrd 2449	1 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = if ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B , 1 , 0 ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 186   \/ wo 368   /\ wa 369   = wceq 1407   E.wex 1635   e. wcel 1844   {cab 2389   A.wral 2756   E.wrex 2757   {crab 2760   _Vcvv 3061   i^i cin 3415   C_ wss 3416   (/)c0 3740   ifcif 3887   ~Pcpw 3957   <.cop 3980   class class class wbr 4397   {copab 4454   |-> cmpt 4455   X. cxp 4823   `'ccnv 4824   dom cdm 4825   ran crn 4826   |` cres 4827   "cima 4828   o. ccom 4829   Fun wfun 5565   Fn wfn 5566   -->wf 5567   -1-1-onto->wf1o 5570   ` cfv 5571  (class class class)co 6280   |-> cmpt2 6282   1stc1st 6784   2ndc2nd 6785   supp csupp 6904   ^m cmap 7459   Fincfn 7556   0cc0 9524   1c1 9525   x. cmul 9529   <_ cle 9661   NNcn 10578   2c2 10628   NN0cn0 10838   ^cexp 12212   sum_csu 13659   || cdvds 14197  bitscbits 14280  𝟭cind 28471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-rep 4509  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-inf2 8093  ax-ac2 8877  ax-cnex 9580  ax-resscn 9581  ax-1cn 9582  ax-icn 9583  ax-addcl 9584  ax-addrcl 9585  ax-mulcl 9586  ax-mulrcl 9587  ax-mulcom 9588  ax-addass 9589  ax-mulass 9590  ax-distr 9591  ax-i2m1 9592  ax-1ne0 9593  ax-1rid 9594  ax-rnegex 9595  ax-rrecex 9596  ax-cnre 9597  ax-pre-lttri 9598  ax-pre-lttrn 9599  ax-pre-ltadd 9600  ax-pre-mulgt0 9601  ax-pre-sup 9602

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-fal 1413  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-nel 2603  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-disj 4369  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-se 4785  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-isom 5580  df-riota 6242  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-1st 6786  df-2nd 6787  df-supp 6905  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-2o 7170  df-oadd 7173  df-er 7350  df-map 7461  df-pm 7462  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560  df-sup 7937  df-oi 7971  df-card 8354  df-acn 8357  df-ac 8531  df-cda 8582  df-pnf 9662  df-mnf 9663  df-xr 9664  df-ltxr 9665  df-le 9666  df-sub 9845  df-neg 9846  df-div 10250  df-nn 10579  df-2 10637  df-3 10638  df-n0 10839  df-z 10908  df-uz 11130  df-rp 11268  df-fz 11729  df-fzo 11857  df-fl 11968  df-mod 12037  df-seq 12154  df-exp 12213  df-hash 12455  df-cj 13083  df-re 13084  df-im 13085  df-sqrt 13219  df-abs 13220  df-clim 13462  df-sum 13660  df-dvds 14198  df-bits 14283  df-ind 28472

This theorem is referenced by:  eulerpartlemgs2  28838