Theorem eulerpartlemgvv 27983

Description: Lemma for eulerpart 27989: 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 27980	. . . 4 |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d 5868	. . 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 10542	. . . 4 |- NN e. _V
15	14	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> NN e. _V )
16		imassrn 5348	. . . . 5 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ ran F
17	4, 5	oddpwdc 27961	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
18		f1of 5816	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
19		frn 5737	. . . . . 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 3513	. . . 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 27698	. . 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 1228	. 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 5731	. . . . . 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 3718	. . . . . . . 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 27982	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
30	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 27974	. . . . . . . . . . 11 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
31		f1of 5816	. . . . . . . . . . 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 6020	. . . . . . . . 9 |- ( (bits o. ( A |` J ) ) e. H -> ( M ` (bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
34	29, 33	syl 16	. . . . . . . 8 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
35	28, 34	sseldi 3502	. . . . . . 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 4020	. . . . 5 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
38		fvelimab 5923	. . . . 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		nfv 1683	. . . . . . 7 |- F/ w ( A e. ( T i^i R ) /\ B e. NN )
41		nfre1 2925	. . . . . . 7 |- F/ w E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B
42	40, 41	nfan 1875	. . . . . 6 |- F/ w ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
43		ssrab2 3585	. . . . . . . . . . 11 |- { z e. NN | -. 2 || z } C_ NN
44	4, 43	eqsstri 3534	. . . . . . . . . 10 |- J C_ NN
45	7	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( A e. ( T i^i R ) -> M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } ) )
46		fveq1 5865	. . . . . . . . . . . . . . . . . . . . 21 |- ( r = (bits o. ( A |` J ) ) -> ( r ` x ) = ( (bits o. ( A |` J ) ) ` x ) )
47	46	eleq2d 2537	. . . . . . . . . . . . . . . . . . . 20 |- ( r = (bits o. ( A |` J ) ) -> ( y e. ( r ` x ) <-> y e. ( (bits o. ( A |` J ) ) ` x ) ) )
48	47	anbi2d 703	. . . . . . . . . . . . . . . . . . 19 |- ( r = (bits o. ( A |` J ) ) -> ( ( x e. J /\ y e. ( r ` x ) ) <-> ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) ) )
49	48	opabbidv 4510	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) } )
50	49	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) } )
51	14, 44	ssexi 4592	. . . . . . . . . . . . . . . . . . 19 |- J e. _V
52		abid2 2607	. . . . . . . . . . . . . . . . . . . . 21 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } = ( (bits o. ( A |` J ) ) ` x )
53		fvex 5876	. . . . . . . . . . . . . . . . . . . . 21 |- ( (bits o. ( A |` J ) ) ` x ) e. _V
54	52, 53	eqeltri 2551	. . . . . . . . . . . . . . . . . . . 20 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } e. _V
55	54	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( x e. J -> { y | y e. ( (bits o. ( A |` J ) ) ` x ) } e. _V )
56	51, 55	opabex3 6763	. . . . . . . . . . . . . . . . . 18 |- { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } e. _V
57	56	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( A e. ( T i^i R ) -> { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } e. _V )
58	45, 50, 29, 57	fvmptd 5955	. . . . . . . . . . . . . . . 16 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) = { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } )
59		simpl 457	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = t /\ y = n ) -> x = t )
60	59	eleq1d 2536	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
61		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = t /\ y = n ) -> y = n )
62	59	fveq2d 5870	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = t /\ y = n ) -> ( (bits o. ( A |` J ) ) ` x ) = ( (bits o. ( A |` J ) ) ` t ) )
63	61, 62	eleq12d 2549	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( y e. ( (bits o. ( A |` J ) ) ` x ) <-> n e. ( (bits o. ( A |` J ) ) ` t ) ) )
64	60, 63	anbi12d 710	. . . . . . . . . . . . . . . . 17 |- ( ( x = t /\ y = n ) -> ( ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) <-> ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) ) )
65	64	cbvopabv 4516	. . . . . . . . . . . . . . . 16 |- { <. x , y >. | ( x e. J /\ y e. ( (bits o. ( A |` J ) ) ` x ) ) } = { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) }
66	58, 65	syl6eq 2524	. . . . . . . . . . . . . . 15 |- ( A e. ( T i^i R ) -> ( M ` (bits o. ( A |` J ) ) ) = { <. t , n >. | ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) } )
67	66	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( 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 ) ) } ) )
68	1, 2, 3, 4, 5, 6, 7, 8, 9	eulerpartlemt0 27976	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
69	68	simp1bi 1011	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
70		nn0ex 10801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- NN0 e. _V
71	70, 14	elmap 7447	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
72	69, 71	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> A : NN --> NN0 )
73		ffun 5733	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A : NN --> NN0 -> Fun A )
74		funres 5627	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Fun A -> Fun ( A |` J ) )
75	72, 73, 74	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> Fun ( A |` J ) )
76	75	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> Fun ( A |` J ) )
77		fssres 5751	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
78	72, 44, 77	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
79		fdm 5735	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
80	79	eleq2d 2537	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A |` J ) : J --> NN0 -> ( t e. dom ( A |` J ) <-> t e. J ) )
81	78, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( t e. dom ( A |` J ) <-> t e. J ) )
82	81	biimpar 485	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> t e. dom ( A |` J ) )
83		fvco 5943	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( Fun ( A |` J ) /\ t e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
84	76, 82, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( ( A |` J ) ` t ) ) )
85		fvres 5880	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
86	85	fveq2d 5870	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. J -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
87	86	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> (bits ` ( ( A |` J ) ` t ) ) = (bits ` ( A ` t ) ) )
88	84, 87	eqtrd 2508	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( A ` t ) ) )
89	88	eleq2d 2537	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( n e. ( (bits o. ( A |` J ) ) ` t ) <-> n e. (bits ` ( A ` t ) ) ) )
90	89	pm5.32da 641	. . . . . . . . . . . . . . . . . 18 |- ( A e. ( T i^i R ) -> ( ( t e. J /\ n e. ( (bits o. ( A |` J ) ) ` t ) ) <-> ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) )
91	90	opabbidv 4510	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) } )
92	91	eleq2d 2537	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) } ) )
93		elopab 4755	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
94	92, 93	syl6bb 261	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
95		ancom 450	. . . . . . . . . . . . . . . . . 18 |- ( ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) )
96		anass 649	. . . . . . . . . . . . . . . . . 18 |- ( ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) <-> ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
97	95, 96	bitri 249	. . . . . . . . . . . . . . . . 17 |- ( ( w = <. t , n >. /\ ( t e. J /\ n e. (bits ` ( A ` t ) ) ) ) <-> ( t e. J /\ ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
98	97	2exbii 1645	. . . . . . . . . . . . . . . 16 |- ( 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 >. ) ) )
99		df-rex 2820	. . . . . . . . . . . . . . . . . . 19 |- ( E. n e. (bits ` ( A ` t ) ) w = <. t , n >. <-> E. n ( n e. (bits ` ( A ` t ) ) /\ w = <. t , n >. ) )
100	99	anbi2i 694	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 >. ) ) )
101	100	exbii 1644	. . . . . . . . . . . . . . . . 17 |- ( 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 >. ) ) )
102		df-rex 2820	. . . . . . . . . . . . . . . . 17 |- ( 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 >. ) )
103		exdistr 1950	. . . . . . . . . . . . . . . . 17 |- ( 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 >. ) ) )
104	101, 102, 103	3bitr4i 277	. . . . . . . . . . . . . . . 16 |- ( 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 >. ) ) )
105	98, 104	bitr4i 252	. . . . . . . . . . . . . . 15 |- ( 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 >. )
106	94, 105	syl6bb 261	. . . . . . . . . . . . . 14 |- ( 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 >. ) )
107	67, 106	bitrd 253	. . . . . . . . . . . . 13 |- ( 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 >. ) )
108	107	biimpa 484	. . . . . . . . . . . 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 >. )
109	108	adantlr 714	. . . . . . . . . . 11 |- ( ( ( 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 >. )
110		fveq2 5866	. . . . . . . . . . . . . . . . 17 |- ( w = <. t , n >. -> ( F ` w ) = ( F ` <. t , n >. ) )
111	110	adantl 466	. . . . . . . . . . . . . . . 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 >. ) -> ( F ` w ) = ( F ` <. t , n >. ) )
112		bitsss 13935	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` ( A ` t ) ) C_ NN0
113	112	sseli 3500	. . . . . . . . . . . . . . . . . . 19 |- ( n e. (bits ` ( A ` t ) ) -> n e. NN0 )
114	113	anim2i 569	. . . . . . . . . . . . . . . . . 18 |- ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) -> ( t e. J /\ n e. NN0 ) )
115	114	ad2antlr 726	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( 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 ) )
116		opelxp 5029	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
117	4, 5	oddpwdcv 27962	. . . . . . . . . . . . . . . . . . 19 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
118		vex 3116	. . . . . . . . . . . . . . . . . . . . . 22 |- t e. _V
119		vex 3116	. . . . . . . . . . . . . . . . . . . . . 22 |- n e. _V
120	118, 119	op2nd 6793	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2nd ` <. t , n >. ) = n
121	120	oveq2i 6295	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
122	118, 119	op1st 6792	. . . . . . . . . . . . . . . . . . . 20 |- ( 1st ` <. t , n >. ) = t
123	121, 122	oveq12i 6296	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
124	117, 123	syl6eq 2524	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
125	116, 124	sylbir 213	. . . . . . . . . . . . . . . . 17 |- ( ( t e. J /\ n e. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
126	115, 125	syl 16	. . . . . . . . . . . . . . . 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 >. ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
127	111, 126	eqtr2d 2509	. . . . . . . . . . . . . . 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 >. ) -> ( ( 2 ^ n ) x. t ) = ( F ` w ) )
128	127	ex 434	. . . . . . . . . . . . . 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 ) ) )
129	128	anassrs 648	. . . . . . . . . . . . 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 ) ) )
130	129	reximdva 2938	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
131	130	reximdva 2938	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
132	109, 131	mpd 15	. . . . . . . . . 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 ) ) ( ( 2 ^ n ) x. t ) = ( F ` w ) )
133		ssrexv 3565	. . . . . . . . . 10 |- ( 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 ) ) )
134	44, 132, 133	mpsyl 63	. . . . . . . . 9 |- ( ( ( 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 ) )
135	134	adantr 465	. . . . . . . 8 |- ( ( ( ( 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 ) )
136		eqeq2 2482	. . . . . . . . . . 11 |- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
137	136	rexbidv 2973	. . . . . . . . . 10 |- ( ( 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 ) )
138	137	adantl 466	. . . . . . . . 9 |- ( ( ( ( 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 ) )
139	138	rexbidv 2973	. . . . . . . 8 |- ( ( ( ( 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 ) )
140	135, 139	mpbid 210	. . . . . . 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 ) = B )
141	140	adantllr 718	. . . . . 6 |- ( ( ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B ) /\ 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 )
142		simpr 461	. . . . . 6 |- ( ( ( A e. ( T i^i R ) /\ B e. NN ) /\ E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B ) -> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
143	42, 141, 142	r19.29af 3001	. . . . 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 )
144		simp-5l 767	. . . . . . . 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 ) )
145		simpllr 758	. . . . . . . 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 )
146		simplr 754	. . . . . . . . 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 ) ) )
147	75	adantr 465	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> Fun ( A |` J ) )
148	79	eleq2d 2537	. . . . . . . . . . . . . 14 |- ( ( A |` J ) : J --> NN0 -> ( x e. dom ( A |` J ) <-> x e. J ) )
149	78, 148	syl 16	. . . . . . . . . . . . 13 |- ( A e. ( T i^i R ) -> ( x e. dom ( A |` J ) <-> x e. J ) )
150	149	biimpar 485	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> x e. dom ( A |` J ) )
151		fvco 5943	. . . . . . . . . . . 12 |- ( ( Fun ( A |` J ) /\ x e. dom ( A |` J ) ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
152	147, 150, 151	syl2anc 661	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( ( A |` J ) ` x ) ) )
153		fvres 5880	. . . . . . . . . . . . 13 |- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
154	153	fveq2d 5870	. . . . . . . . . . . 12 |- ( x e. J -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
155	154	adantl 466	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> (bits ` ( ( A |` J ) ` x ) ) = (bits ` ( A ` x ) ) )
156	152, 155	eqtrd 2508	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( (bits o. ( A |` J ) ) ` x ) = (bits ` ( A ` x ) ) )
157	144, 145, 156	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 ) ) )
158	146, 157	eleqtrrd 2558	. . . . . . . 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 ) )
159	58	eleq2d 2537	. . . . . . . . . 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 ) ) } ) )
160		opabid 4754	. . . . . . . . . 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 ) ) )
161	159, 160	syl6bb 261	. . . . . . . . 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 ) ) ) )
162	161	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 ) ) ) )
163	144, 145, 158, 162	syl12anc 1226	. . . . . . 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 ) ) ) )
164		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 )
165	37	ad4antr 731	. . . . . . . . 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 ) )
166	165, 163	sseldd 3505	. . . . . . . 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 ) )
167		opeq1 4213	. . . . . . . . . . . 12 |- ( t = x -> <. t , y >. = <. x , y >. )
168	167	eleq1d 2536	. . . . . . . . . . 11 |- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
169	167	fveq2d 5870	. . . . . . . . . . . 12 |- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
170		oveq2 6292	. . . . . . . . . . . 12 |- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
171	169, 170	eqeq12d 2489	. . . . . . . . . . 11 |- ( t = x -> ( ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) <-> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) )
172	168, 171	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 ) ) ) )
173		opeq2 4214	. . . . . . . . . . . . 13 |- ( n = y -> <. t , n >. = <. t , y >. )
174	173	eleq1d 2536	. . . . . . . . . . . 12 |- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
175	173	fveq2d 5870	. . . . . . . . . . . . 13 |- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
176		oveq2 6292	. . . . . . . . . . . . . 14 |- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
177	176	oveq1d 6299	. . . . . . . . . . . . 13 |- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
178	175, 177	eqeq12d 2489	. . . . . . . . . . . 12 |- ( n = y -> ( ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) <-> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) )
179	174, 178	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 ) ) ) )
180	179, 124	chvarv 1983	. . . . . . . . . 10 |- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
181	172, 180	chvarv 1983	. . . . . . . . 9 |- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
182		eqeq2 2482	. . . . . . . . . 10 |- ( ( ( 2 ^ y ) x. x ) = B -> ( ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) <-> ( F ` <. x , y >. ) = B ) )
183	182	biimpa 484	. . . . . . . . 9 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) -> ( F ` <. x , y >. ) = B )
184	181, 183	sylan2 474	. . . . . . . 8 |- ( ( ( ( 2 ^ y ) x. x ) = B /\ <. x , y >. e. ( J X. NN0 ) ) -> ( F ` <. x , y >. ) = B )
185	164, 166, 184	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 )
186		fveq2 5866	. . . . . . . . 9 |- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
187	186	eqeq1d 2469	. . . . . . . 8 |- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
188	187	rspcev 3214	. . . . . . 7 |- ( ( <. x , y >. e. ( M ` (bits o. ( A |` J ) ) ) /\ ( F ` <. x , y >. ) = B ) -> E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B )
189	163, 185, 188	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 )
190		oveq2 6292	. . . . . . . . . . 11 |- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
191	190	eqeq1d 2469	. . . . . . . . . 10 |- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
192	176	oveq1d 6299	. . . . . . . . . . 11 |- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
193	192	eqeq1d 2469	. . . . . . . . . 10 |- ( n = y -> ( ( ( 2 ^ n ) x. x ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
194	191, 193	sylan9bb 699	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
195		simpl 457	. . . . . . . . . . 11 |- ( ( t = x /\ n = y ) -> t = x )
196	195	fveq2d 5870	. . . . . . . . . 10 |- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
197	196	fveq2d 5870	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> (bits ` ( A ` t ) ) = (bits ` ( A ` x ) ) )
198	194, 197	cbvrexdva2 3093	. . . . . . . 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 ) )
199	198	cbvrexv 3089	. . . . . . 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 )
200		nfv 1683	. . . . . . . . . . . . . 14 |- F/ y A e. ( T i^i R )
201		nfv 1683	. . . . . . . . . . . . . . 15 |- F/ y x e. NN
202		nfre1 2925	. . . . . . . . . . . . . . 15 |- F/ y E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
203	201, 202	nfan 1875	. . . . . . . . . . . . . 14 |- F/ y ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
204	200, 203	nfan 1875	. . . . . . . . . . . . 13 |- F/ y ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
205		simplr 754	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. NN )
206		n0i 3790	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. (bits ` ( A ` x ) ) -> -. (bits ` ( A ` x ) ) = (/) )
207	206	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. (bits ` ( A ` x ) ) = (/) )
208		fveq2 5866	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (bits ` 0 ) )
209		0bits 13948	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` 0 ) = (/)
210	208, 209	syl6eq 2524	. . . . . . . . . . . . . . . . . . 19 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (/) )
211	207, 210	nsyl 121	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. ( A ` x ) = 0 )
212	72	ffvelrnda 6021	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( A ` x ) e. NN0 )
213	212	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN0 )
214		elnn0 10797	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A ` x ) e. NN0 <-> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
215	213, 214	sylib 196	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
216	215	orcomd 388	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( ( A ` x ) = 0 \/ ( A ` x ) e. NN ) )
217	216	orcanai 911	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) /\ -. ( A ` x ) = 0 ) -> ( A ` x ) e. NN )
218	211, 217	mpdan 668	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN )
219	68	simp3bi 1013	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
220	219	sselda 3504	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
221		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = n -> ( 2 || z <-> 2 || n ) )
222	221	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
223	222, 4	elrab2 3263	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
224	223	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. J -> -. 2 || n )
225	220, 224	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> -. 2 || n )
226	225	ralrimiva 2878	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
227		ffn 5731	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A : NN --> NN0 -> A Fn NN )
228		elpreima 6001	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A Fn NN -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
229	72, 227, 228	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
230	229	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) ) )
231		impexp 446	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
232	230, 231	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 |- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) ) )
233	232	ralbidv2 2899	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> ( A. n e. ( `' A " NN ) -. 2 || n <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) ) )
234	226, 233	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. ( T i^i R ) -> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
235		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( A ` x ) = ( A ` n ) )
236	235	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
237		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( 2 || x <-> 2 || n ) )
238	237	notbid 294	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( -. 2 || x <-> -. 2 || n ) )
239	236, 238	imbi12d 320	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> ( ( ( A ` x ) e. NN -> -. 2 || x ) <-> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
240	239	cbvralv 3088	. . . . . . . . . . . . . . . . . . . 20 |- ( A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
241	234, 240	sylibr 212	. . . . . . . . . . . . . . . . . . 19 |- ( A e. ( T i^i R ) -> A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) )
242	241	r19.21bi 2833	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( ( A ` x ) e. NN -> -. 2 || x ) )
243	242	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ ( A ` x ) e. NN ) -> -. 2 || x )
244	218, 243	syldan 470	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> -. 2 || x )
245		breq2 4451	. . . . . . . . . . . . . . . . . 18 |- ( z = x -> ( 2 || z <-> 2 || x ) )
246	245	notbid 294	. . . . . . . . . . . . . . . . 17 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
247	246, 4	elrab2 3263	. . . . . . . . . . . . . . . 16 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
248	205, 244, 247	sylanbrc 664	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. (bits ` ( A ` x ) ) ) -> x e. J )
249	248	adantlrr 720	. . . . . . . . . . . . . 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 )
250	249	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 )
251		simprr 756	. . . . . . . . . . . . 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 )
252	204, 250, 251	r19.29af 3001	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) -> x e. J )
253	252, 251	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 ) )
254	253	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 ) ) )
255	254	reximdv2 2934	. . . . . . . . 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 ) )
256	255	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 )
257	256	adantlr 714	. . . . . . 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 )
258	199, 257	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 )
259	189, 258	r19.29_2a 3005	. . . . 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 )
260	143, 259	impbida 830	. . . 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 ) )
261	39, 260	bitrd 253	. . 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 ) )
262	261	ifbid 3961	. 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 ) )
263	13, 25, 262	3eqtrd 2512	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 184   \/ wo 368   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815   {crab 2818   _Vcvv 3113   i^i cin 3475   C_ wss 3476   (/)c0 3785   ifcif 3939   ~Pcpw 4010   <.cop 4033   class class class wbr 4447   {copab 4504   |-> cmpt 4505   X. cxp 4997   `'ccnv 4998   dom cdm 4999   ran crn 5000   |` cres 5001   "cima 5002   o. ccom 5003   Fun wfun 5582   Fn wfn 5583   -->wf 5584   -1-1-onto->wf1o 5587   ` cfv 5588  (class class class)co 6284   |-> cmpt2 6286   1stc1st 6782   2ndc2nd 6783   supp csupp 6901   ^m cmap 7420   Fincfn 7516   0cc0 9492   1c1 9493   x. cmul 9497   <_ cle 9629   NNcn 10536   2c2 10585   NN0cn0 10795   ^cexp 12134   sum_csu 13471   || cdivides 13847  bitscbits 13928  𝟭cind 27692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-ac2 8843  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-sup 7901  df-oi 7935  df-card 8320  df-acn 8323  df-ac 8497  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-n0 10796  df-z 10865  df-uz 11083  df-rp 11221  df-fz 11673  df-fzo 11793  df-fl 11897  df-mod 11965  df-seq 12076  df-exp 12135  df-hash 12374  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-clim 13274  df-sum 13472  df-dvds 13848  df-bits 13931  df-ind 27693

This theorem is referenced by:  eulerpartlemgs2  27987