Theorem eulerpartlemgvv 29209

Description: Lemma for eulerpart 29215: 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 29206	. . . 4 |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d 5867	. . 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 10615	. . . 4 |- NN e. _V
15	14	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> NN e. _V )
16		imassrn 5179	. . . . 5 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ ran F
17	4, 5	oddpwdc 29187	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
18		f1of 5814	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
19		frn 5735	. . . . . 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 3441	. . . 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 28838	. . 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 1268	. 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 5728	. . . . . 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 3652	. . . . . . . 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 29208	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
30	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 29200	. . . . . . . . . . 11 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
31		f1of 5814	. . . . . . . . . . 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 6021	. . . . . . . . 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 3430	. . . . . . 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 3961	. . . . 5 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
38		fvelimab 5921	. . . . 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 669	. . . 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 3514	. . . . . . . . . 10 |- { z e. NN | -. 2 || z } C_ NN
41	4, 40	eqsstri 3462	. . . . . . . . 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 5864	. . . . . . . . . . . . . . . . . . . 20 |- ( r = (bits o. ( A |` J ) ) -> ( r ` x ) = ( (bits o. ( A |` J ) ) ` x ) )
44	43	eleq2d 2514	. . . . . . . . . . . . . . . . . . 19 |- ( r = (bits o. ( A |` J ) ) -> ( y e. ( r ` x ) <-> y e. ( (bits o. ( A |` J ) ) ` x ) ) )
45	44	anbi2d 710	. . . . . . . . . . . . . . . . . 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 4466	. . . . . . . . . . . . . . . . 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 4548	. . . . . . . . . . . . . . . . . 18 |- J e. _V
49		abid2 2573	. . . . . . . . . . . . . . . . . . . 20 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } = ( (bits o. ( A |` J ) ) ` x )
50		fvex 5875	. . . . . . . . . . . . . . . . . . . 20 |- ( (bits o. ( A |` J ) ) ` x ) e. _V
51	49, 50	eqeltri 2525	. . . . . . . . . . . . . . . . . . 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 6772	. . . . . . . . . . . . . . . . 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 5954	. . . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
58		simpr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> y = n )
59	56	fveq2d 5869	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( (bits o. ( A |` J ) ) ` x ) = ( (bits o. ( A |` J ) ) ` t ) )
60	58, 59	eleq12d 2523	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( y e. ( (bits o. ( A |` J ) ) ` x ) <-> n e. ( (bits o. ( A |` J ) ) ` t ) ) )
61	57, 60	anbi12d 717	. . . . . . . . . . . . . . . 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 4472	. . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . 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 2514	. . . . . . . . . . . . 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 29202	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
66	65	simp1bi 1023	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
67		nn0ex 10875	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- NN0 e. _V
68	67, 14	elmap 7500	. . . . . . . . . . . . . . . . . . . . . . . 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 5731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A : NN --> NN0 -> Fun A )
71		funres 5621	. . . . . . . . . . . . . . . . . . . . . . 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 5749	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
75	69, 41, 74	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
76		fdm 5733	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
77	76	eleq2d 2514	. . . . . . . . . . . . . . . . . . . . . . 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 5941	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( Fun ( A |` J ) /\ t e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
81	73, 79, 80	syl2anc 667	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
82		fvres 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
83	82	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . 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 2485	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( A ` t ) ) )
86	85	eleq2d 2514	. . . . . . . . . . . . . . . . . 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 647	. . . . . . . . . . . . . . . . 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 4466	. . . . . . . . . . . . . . . 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 2514	. . . . . . . . . . . . . . 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 4709	. . . . . . . . . . . . . . 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 655	. . . . . . . . . . . . . . . . 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 1719	. . . . . . . . . . . . . . 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 2743	. . . . . . . . . . . . . . . . . 18 |- ( E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) )
97	96	anbi2i 700	. . . . . . . . . . . . . . . . 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 1718	. . . . . . . . . . . . . . . 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 2743	. . . . . . . . . . . . . . . 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 1835	. . . . . . . . . . . . . . . 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 721	. . . . . . . . . 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 5865	. . . . . . . . . . . . . . . 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 14399	. . . . . . . . . . . . . . . . . . 19 |- (bits ` ( A ` t ) ) C_ NN0
110	109	sseli 3428	. . . . . . . . . . . . . . . . . 18 |- ( n e. (bits ` ( A ` t ) ) -> n e. NN0 )
111	110	anim2i 573	. . . . . . . . . . . . . . . . 17 |- ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) -> ( t e. J /\ n e. NN0 ) )
112	111	ad2antlr 733	. . . . . . . . . . . . . . . 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 4864	. . . . . . . . . . . . . . . . 17 |- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
114	4, 5	oddpwdcv 29188	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
115		vex 3048	. . . . . . . . . . . . . . . . . . . . 21 |- t e. _V
116		vex 3048	. . . . . . . . . . . . . . . . . . . . 21 |- n e. _V
117	115, 116	op2nd 6802	. . . . . . . . . . . . . . . . . . . 20 |- ( 2nd ` <. t , n >. ) = n
118	117	oveq2i 6301	. . . . . . . . . . . . . . . . . . 19 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
119	115, 116	op1st 6801	. . . . . . . . . . . . . . . . . . 19 |- ( 1st ` <. t , n >. ) = t
120	118, 119	oveq12i 6302	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
121	114, 120	syl6eq 2501	. . . . . . . . . . . . . . . . 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 2486	. . . . . . . . . . . . . 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 654	. . . . . . . . . . . 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 2862	. . . . . . . . . . 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 2862	. . . . . . . . . 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 3494	. . . . . . . . 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 65	. . . . . . . 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 2462	. . . . . . . . . 10 |- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
134	133	rexbidv 2901	. . . . . . . . 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 2901	. . . . . . 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 2931	. . . . 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 778	. . . . . . . 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 769	. . . . . . . 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 762	. . . . . . . . 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 2514	. . . . . . . . . . . . . 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 5941	. . . . . . . . . . . 12 |- ( ( Fun ( A |` J ) /\ x e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
147	142, 145, 146	syl2anc 667	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
148		fvres 5879	. . . . . . . . . . . . 13 |- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
149	148	fveq2d 5869	. . . . . . . . . . . 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 2485	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( A ` x ) ) )
152	139, 140, 151	syl2anc 667	. . . . . . . . 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 2532	. . . . . . . 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 2514	. . . . . . . . . 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 4708	. . . . . . . . . 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 1266	. . . . . . 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 738	. . . . . . . . 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 3433	. . . . . . . 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 4166	. . . . . . . . . . . 12 |- ( t = x -> <. t , y >. = <. x , y >. )
163	162	eleq1d 2513	. . . . . . . . . . 11 |- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
164	162	fveq2d 5869	. . . . . . . . . . . 12 |- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
165		oveq2 6298	. . . . . . . . . . . 12 |- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
166	164, 165	eqeq12d 2466	. . . . . . . . . . 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 4167	. . . . . . . . . . . . 13 |- ( n = y -> <. t , n >. = <. t , y >. )
169	168	eleq1d 2513	. . . . . . . . . . . 12 |- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
170	168	fveq2d 5869	. . . . . . . . . . . . 13 |- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
171		oveq2 6298	. . . . . . . . . . . . . 14 |- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
172	171	oveq1d 6305	. . . . . . . . . . . . 13 |- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
173	170, 172	eqeq12d 2466	. . . . . . . . . . . 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 2107	. . . . . . . . . 10 |- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
176	167, 175	chvarv 2107	. . . . . . . . 9 |- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
177		eqeq2 2462	. . . . . . . . . 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 667	. . . . . . 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 5865	. . . . . . . . 9 |- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
182	181	eqeq1d 2453	. . . . . . . 8 |- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
183	182	rspcev 3150	. . . . . . 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 667	. . . . . 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 6298	. . . . . . . . . . 11 |- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
186	185	eqeq1d 2453	. . . . . . . . . 10 |- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
187	171	oveq1d 6305	. . . . . . . . . . 11 |- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
188	187	eqeq1d 2453	. . . . . . . . . 10 |- ( n = y -> ( ( ( 2 ^ n ) x. x ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
189	186, 188	sylan9bb 706	. . . . . . . . 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 5869	. . . . . . . . . 10 |- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
192	191	fveq2d 5869	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> (bits ` ( A ` t ) ) = (bits ` ( A ` x ) ) )
193	189, 192	cbvrexdva2 3024	. . . . . . . 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 3020	. . . . . . 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 1761	. . . . . . . . . . . . . 14 |- F/ y A e. ( T i^i R )
196		nfv 1761	. . . . . . . . . . . . . . 15 |- F/ y x e. NN
197		nfre1 2848	. . . . . . . . . . . . . . 15 |- F/ y E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
198	196, 197	nfan 2011	. . . . . . . . . . . . . 14 |- F/ y ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
199	195, 198	nfan 2011	. . . . . . . . . . . . 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 762	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. NN )
201		n0i 3736	. . . . . . . . . . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (bits ` 0 ) )
204		0bits 14413	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` 0 ) = (/)
205	203, 204	syl6eq 2501	. . . . . . . . . . . . . . . . . . 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 6022	. . . . . . . . . . . . . . . . . . . . . 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 10871	. . . . . . . . . . . . . . . . . . . . 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 924	. . . . . . . . . . . . . . . . . 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 674	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN )
214	65	simp3bi 1025	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
215	214	sselda 3432	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
216		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = n -> ( 2 || z <-> 2 || n ) )
217	216	notbid 296	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
218	217, 4	elrab2 3198	. . . . . . . . . . . . . . . . . . . . . . . 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 2802	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
222		ffn 5728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A : NN --> NN0 -> A Fn NN )
223		elpreima 6002	. . . . . . . . . . . . . . . . . . . . . . . . 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 2823	. . . . . . . . . . . . . . . . . . . . 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 5865	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( A ` x ) = ( A ` n ) )
231	230	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
232		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . 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 3019	. . . . . . . . . . . . . . . . . . . 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 2757	. . . . . . . . . . . . . . . . . 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 4406	. . . . . . . . . . . . . . . . . 18 |- ( z = x -> ( 2 || z <-> 2 || x ) )
241	240	notbid 296	. . . . . . . . . . . . . . . . 17 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
242	241, 4	elrab2 3198	. . . . . . . . . . . . . . . 16 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
243	200, 239, 242	sylanbrc 670	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. J )
244	243	adantlrr 727	. . . . . . . . . . . . . 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 766	. . . . . . . . . . . . 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 2930	. . . . . . . . . . . 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 2858	. . . . . . . . 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 721	. . . . . . 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 2934	. . . . 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 843	. . . 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 3903	. 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 2489	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 1444   E.wex 1663   e. wcel 1887   {cab 2437   A.wral 2737   E.wrex 2738   {crab 2741   _Vcvv 3045   i^i cin 3403   C_ wss 3404   (/)c0 3731   ifcif 3881   ~Pcpw 3951   <.cop 3974   class class class wbr 4402   {copab 4460   |-> cmpt 4461   X. cxp 4832   `'ccnv 4833   dom cdm 4834   ran crn 4835   |` cres 4836   "cima 4837   o. ccom 4838   Fun wfun 5576   Fn wfn 5577   -->wf 5578   -1-1-onto->wf1o 5581   ` cfv 5582  (class class class)co 6290   |-> cmpt2 6292   1stc1st 6791   2ndc2nd 6792   supp csupp 6914   ^m cmap 7472   Fincfn 7569   0cc0 9539   1c1 9540   x. cmul 9544   <_ cle 9676   NNcn 10609   2c2 10659   NN0cn0 10869   ^cexp 12272   sum_csu 13752   || cdvds 14305  bitscbits 14392  𝟭cind 28832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-ac2 8893  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-disj 4374  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-acn 8376  df-ac 8547  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-fz 11785  df-fzo 11916  df-fl 12028  df-mod 12097  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-clim 13552  df-sum 13753  df-dvds 14306  df-bits 14395  df-ind 28833

This theorem is referenced by:  eulerpartlemgs2  29213