Theorem eulerpartlemgvv 29211

Description: Lemma for eulerpart 29217: 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 29208	. . . 4 |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d 5881	. . 3 |- ( A e. ( T i^i R ) -> ( ( G ` A ) ` B ) = ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) )
13	12	adantr 467	. 2 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = ( ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) ` B ) )
14		nnex 10617	. . . 4 |- NN e. _V
15	14	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> NN e. _V )
16		imassrn 5196	. . . . 5 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ ran F
17	4, 5	oddpwdc 29189	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
18		f1of 5829	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
19		frn 5750	. . . . . 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 3474	. . . 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 463	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> B e. NN )
24		indfval 28840	. . 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 1265	. 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 5744	. . . . . 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 3683	. . . . . . . 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 29210	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
30	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 29202	. . . . . . . . . . 11 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
31		f1of 5829	. . . . . . . . . . 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 6034	. . . . . . . . 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 3463	. . . . . . 7 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
36	35	adantr 467	. . . . . 6 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
37	36	elpwid 3990	. . . . 5 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
38		fvelimab 5935	. . . . 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 668	. . . 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 3547	. . . . . . . . . 10 |- { z e. NN | -. 2 || z } C_ NN
41	4, 40	eqsstri 3495	. . . . . . . . 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 5878	. . . . . . . . . . . . . . . . . . . 20 |- ( r = (bits o. ( A |` J ) ) -> ( r ` x ) = ( (bits o. ( A |` J ) ) ` x ) )
44	43	eleq2d 2493	. . . . . . . . . . . . . . . . . . 19 |- ( r = (bits o. ( A |` J ) ) -> ( y e. ( r ` x ) <-> y e. ( (bits o. ( A |` J ) ) ` x ) ) )
45	44	anbi2d 709	. . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . 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 4567	. . . . . . . . . . . . . . . . . 18 |- J e. _V
49		abid2 2563	. . . . . . . . . . . . . . . . . . . 20 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } = ( (bits o. ( A |` J ) ) ` x )
50		fvex 5889	. . . . . . . . . . . . . . . . . . . 20 |- ( (bits o. ( A |` J ) ) ` x ) e. _V
51	49, 50	eqeltri 2507	. . . . . . . . . . . . . . . . . . 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 6784	. . . . . . . . . . . . . . . . 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 5968	. . . . . . . . . . . . . . 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 459	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> x = t )
57	56	eleq1d 2492	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
58		simpr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> y = n )
59	56	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( (bits o. ( A |` J ) ) ` x ) = ( (bits o. ( A |` J ) ) ` t ) )
60	58, 59	eleq12d 2505	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( y e. ( (bits o. ( A |` J ) ) ` x ) <-> n e. ( (bits o. ( A |` J ) ) ` t ) ) )
61	57, 60	anbi12d 716	. . . . . . . . . . . . . . . 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 4491	. . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . . 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 2493	. . . . . . . . . . . . 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 29204	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
66	65	simp1bi 1021	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
67		nn0ex 10877	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- NN0 e. _V
68	67, 14	elmap 7506	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
69	66, 68	sylib 200	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> A : NN --> NN0 )
70		ffun 5746	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A : NN --> NN0 -> Fun A )
71		funres 5638	. . . . . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> Fun ( A |` J ) )
74		fssres 5764	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
75	69, 41, 74	sylancl 667	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
76		fdm 5748	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
77	76	eleq2d 2493	. . . . . . . . . . . . . . . . . . . . . . 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 488	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> t e. dom ( A |` J ) )
80		fvco 5955	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Fun ( A |` J ) /\ t e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
81	73, 79, 80	syl2anc 666	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
82		fvres 5893	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
83	82	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21 |- ( t e. J -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
84	83	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
85	81, 84	eqtrd 2464	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( A ` t ) ) )
86	85	eleq2d 2493	. . . . . . . . . . . . . . . . . 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 646	. . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . 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 2493	. . . . . . . . . . . . . . 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 4726	. . . . . . . . . . . . . . 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 265	. . . . . . . . . . . . . 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 452	. . . . . . . . . . . . . . . . 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 654	. . . . . . . . . . . . . . . . 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 253	. . . . . . . . . . . . . . . 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 1714	. . . . . . . . . . . . . . 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 2782	. . . . . . . . . . . . . . . . . 18 |- ( E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) )
97	96	anbi2i 699	. . . . . . . . . . . . . . . . 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 1713	. . . . . . . . . . . . . . . 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 2782	. . . . . . . . . . . . . . . 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 1825	. . . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . . . 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 256	. . . . . . . . . . . . . 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 265	. . . . . . . . . . . . 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 257	. . . . . . . . . . . 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 487	. . . . . . . . . . 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 720	. . . . . . . . . 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 5879	. . . . . . . . . . . . . . . 16 |- ( w = <. t , n >. -> ( F ` w ) = ( F ` <. t , n >. ) )
108	107	adantl 468	. . . . . . . . . . . . . . 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 14392	. . . . . . . . . . . . . . . . . . 19 |- (bits ` ( A ` t ) ) C_ NN0
110	109	sseli 3461	. . . . . . . . . . . . . . . . . 18 |- ( n e. (bits ` ( A ` t ) ) -> n e. NN0 )
111	110	anim2i 572	. . . . . . . . . . . . . . . . 17 |- ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) -> ( t e. J /\ n e. NN0 ) )
112	111	ad2antlr 732	. . . . . . . . . . . . . . . 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 4881	. . . . . . . . . . . . . . . . 17 |- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
114	4, 5	oddpwdcv 29190	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
115		vex 3085	. . . . . . . . . . . . . . . . . . . . 21 |- t e. _V
116		vex 3085	. . . . . . . . . . . . . . . . . . . . 21 |- n e. _V
117	115, 116	op2nd 6814	. . . . . . . . . . . . . . . . . . . 20 |- ( 2nd ` <. t , n >. ) = n
118	117	oveq2i 6314	. . . . . . . . . . . . . . . . . . 19 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
119	115, 116	op1st 6813	. . . . . . . . . . . . . . . . . . 19 |- ( 1st ` <. t , n >. ) = t
120	118, 119	oveq12i 6315	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
121	114, 120	syl6eq 2480	. . . . . . . . . . . . . . . . 17 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
122	113, 121	sylbir 217	. . . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . 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 436	. . . . . . . . . . . . 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 653	. . . . . . . . . . . 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 2901	. . . . . . . . . . 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 2901	. . . . . . . . . 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 3527	. . . . . . . . 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 66	. . . . . . . 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 467	. . . . . . 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 2438	. . . . . . . . . 10 |- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
134	133	rexbidv 2940	. . . . . . . . 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 468	. . . . . . . 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 2940	. . . . . . 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 214	. . . . . 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 2970	. . . . 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 777	. . . . . . . 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 768	. . . . . . . 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 761	. . . . . . . . 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 467	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> Fun ( A |` J ) )
143	76	eleq2d 2493	. . . . . . . . . . . . . 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 488	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> x e. dom ( A |` J ) )
146		fvco 5955	. . . . . . . . . . . 12 |- ( ( Fun ( A |` J ) /\ x e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
147	142, 145, 146	syl2anc 666	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
148		fvres 5893	. . . . . . . . . . . . 13 |- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
149	148	fveq2d 5883	. . . . . . . . . . . 12 |- ( x e. J -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
150	149	adantl 468	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
151	147, 150	eqtrd 2464	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( A ` x ) ) )
152	139, 140, 151	syl2anc 666	. . . . . . . . 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 2514	. . . . . . . 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 2493	. . . . . . . . . 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 4725	. . . . . . . . . 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 265	. . . . . . . . 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 488	. . . . . . . 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 1263	. . . . . . 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 463	. . . . . . . 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 737	. . . . . . . . 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 3466	. . . . . . . 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 4185	. . . . . . . . . . . 12 |- ( t = x -> <. t , y >. = <. x , y >. )
163	162	eleq1d 2492	. . . . . . . . . . 11 |- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
164	162	fveq2d 5883	. . . . . . . . . . . 12 |- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
165		oveq2 6311	. . . . . . . . . . . 12 |- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
166	164, 165	eqeq12d 2445	. . . . . . . . . . 11 |- ( t = x -> ( ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) <-> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) )
167	163, 166	imbi12d 322	. . . . . . . . . 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 4186	. . . . . . . . . . . . 13 |- ( n = y -> <. t , n >. = <. t , y >. )
169	168	eleq1d 2492	. . . . . . . . . . . 12 |- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
170	168	fveq2d 5883	. . . . . . . . . . . . 13 |- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
171		oveq2 6311	. . . . . . . . . . . . . 14 |- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
172	171	oveq1d 6318	. . . . . . . . . . . . 13 |- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
173	170, 172	eqeq12d 2445	. . . . . . . . . . . 12 |- ( n = y -> ( ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) <-> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) )
174	169, 173	imbi12d 322	. . . . . . . . . . 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 2069	. . . . . . . . . 10 |- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
176	167, 175	chvarv 2069	. . . . . . . . 9 |- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
177		eqeq2 2438	. . . . . . . . . 10 |- ( ( ( 2 ^ y ) x. x ) = B -> ( ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) <-> ( F ` <. x , y >. ) = B ) )
178	177	biimpa 487	. . . . . . . . 9 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) -> ( F ` <. x , y >. ) = B )
179	176, 178	sylan2 477	. . . . . . . 8 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ <. x , y >. e. ( J X. NN0 ) ) -> ( F ` <. x , y >. ) = B )
180	159, 161, 179	syl2anc 666	. . . . . . 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 5879	. . . . . . . . 9 |- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
182	181	eqeq1d 2425	. . . . . . . 8 |- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
183	182	rspcev 3183	. . . . . . 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 666	. . . . . 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 6311	. . . . . . . . . . 11 |- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
186	185	eqeq1d 2425	. . . . . . . . . 10 |- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
187	171	oveq1d 6318	. . . . . . . . . . 11 |- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
188	187	eqeq1d 2425	. . . . . . . . . 10 |- ( n = y -> ( ( ( 2 ^ n ) x. x ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
189	186, 188	sylan9bb 705	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
190		simpl 459	. . . . . . . . . . 11 |- ( ( t = x /\ n = y ) -> t = x )
191	190	fveq2d 5883	. . . . . . . . . 10 |- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
192	191	fveq2d 5883	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> (bits ` ( A ` t ) ) = (bits ` ( A ` x ) ) )
193	189, 192	cbvrexdva2 3061	. . . . . . . 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 3057	. . . . . . 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 1752	. . . . . . . . . . . . . 14 |- F/ y A e. ( T i^i R )
196		nfv 1752	. . . . . . . . . . . . . . 15 |- F/ y x e. NN
197		nfre1 2887	. . . . . . . . . . . . . . 15 |- F/ y E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
198	196, 197	nfan 1985	. . . . . . . . . . . . . 14 |- F/ y ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
199	195, 198	nfan 1985	. . . . . . . . . . . . 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 761	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. NN )
201		n0i 3767	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. (bits ` ( A ` x ) ) -> -. (bits ` ( A ` x ) ) = (/) )
202	201	adantl 468	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. (bits ` ( A ` x ) ) = (/) )
203		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (bits ` 0 ) )
204		0bits 14406	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` 0 ) = (/)
205	203, 204	syl6eq 2480	. . . . . . . . . . . . . . . . . . 19 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (/) )
206	202, 205	nsyl 125	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. ( A ` x ) = 0 )
207	69	ffvelrnda 6035	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( A ` x ) e. NN0 )
208	207	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN0 )
209		elnn0 10873	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A ` x ) e. NN0 <-> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
210	208, 209	sylib 200	. . . . . . . . . . . . . . . . . . . 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 390	. . . . . . . . . . . . . . . . . . 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 922	. . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN )
214	65	simp3bi 1023	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
215	214	sselda 3465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
216		breq2 4425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = n -> ( 2 || z <-> 2 || n ) )
217	216	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
218	217, 4	elrab2 3232	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
219	218	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
222		ffn 5744	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A : NN --> NN0 -> A Fn NN )
223		elpreima 6015	. . . . . . . . . . . . . . . . . . . . . . . . 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 319	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) ) )
226		impexp 448	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
227	225, 226	syl6bb 265	. . . . . . . . . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . . . . . . 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 214	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. ( T i^i R ) -> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
230		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( A ` x ) = ( A ` n ) )
231	230	eleq1d 2492	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
232		breq2 4425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( 2 || x <-> 2 || n ) )
233	232	notbid 296	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( -. 2 || x <-> -. 2 || n ) )
234	231, 233	imbi12d 322	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> ( ( ( A ` x ) e. NN -> -. 2 || x ) <-> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
235	234	cbvralv 3056	. . . . . . . . . . . . . . . . . . . 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 216	. . . . . . . . . . . . . . . . . . 19 |- ( A e. ( T i^i R ) -> A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) )
237	236	r19.21bi 2795	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( ( A ` x ) e. NN -> -. 2 || x ) )
238	237	imp 431	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ ( A ` x ) e. NN ) -> -. 2 || x )
239	213, 238	syldan 473	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. 2 || x )
240		breq2 4425	. . . . . . . . . . . . . . . . . 18 |- ( z = x -> ( 2 || z <-> 2 || x ) )
241	240	notbid 296	. . . . . . . . . . . . . . . . 17 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
242	241, 4	elrab2 3232	. . . . . . . . . . . . . . . 16 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
243	200, 239, 242	sylanbrc 669	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. J )
244	243	adantlrr 726	. . . . . . . . . . . . . 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 467	. . . . . . . . . . . . 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 765	. . . . . . . . . . . . 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 2969	. . . . . . . . . . . 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 535	. . . . . . . . . . 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 436	. . . . . . . . . 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 2897	. . . . . . . . 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 431	. . . . . . . 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 720	. . . . . . 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 478	. . . . . 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 2973	. . . . 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 841	. . . 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 257	. . 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 3932	. 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 2468	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 188   \/ wo 370   /\ wa 371   = wceq 1438   E.wex 1660   e. wcel 1869   {cab 2408   A.wral 2776   E.wrex 2777   {crab 2780   _Vcvv 3082   i^i cin 3436   C_ wss 3437   (/)c0 3762   ifcif 3910   ~Pcpw 3980   <.cop 4003   class class class wbr 4421   {copab 4479   |-> cmpt 4480   X. cxp 4849   `'ccnv 4850   dom cdm 4851   ran crn 4852   |` cres 4853   "cima 4854   o. ccom 4855   Fun wfun 5593   Fn wfn 5594   -->wf 5595   -1-1-onto->wf1o 5598   ` cfv 5599  (class class class)co 6303   |-> cmpt2 6305   1stc1st 6803   2ndc2nd 6804   supp csupp 6923   ^m cmap 7478   Fincfn 7575   0cc0 9541   1c1 9542   x. cmul 9546   <_ cle 9678   NNcn 10611   2c2 10661   NN0cn0 10871   ^cexp 12273   sum_csu 13745   || cdvds 14298  bitscbits 14385  𝟭cind 28834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-inf2 8150  ax-ac2 8895  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-fal 1444  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-disj 4393  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-se 4811  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-isom 5608  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-supp 6924  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-2o 7189  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-sup 7960  df-inf 7961  df-oi 8029  df-card 8376  df-acn 8379  df-ac 8549  df-cda 8600  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-n0 10872  df-z 10940  df-uz 11162  df-rp 11305  df-fz 11787  df-fzo 11918  df-fl 12029  df-mod 12098  df-seq 12215  df-exp 12274  df-hash 12517  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  df-clim 13545  df-sum 13746  df-dvds 14299  df-bits 14388  df-ind 28835

This theorem is referenced by:  eulerpartlemgs2  29215