Theorem eulerpartlemgvv 26781

Description: Lemma for eulerpart 26787: 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 26778	. . . 4 |- ( A e. ( T i^i R ) -> ( G ` A ) = ( (𝟭 ` NN ) ` ( F " ( M ` (bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d 5714	. . 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 10349	. . . 4 |- NN e. _V
15	14	a1i 11	. . 3 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> NN e. _V )
16		imassrn 5201	. . . . 5 |- ( F " ( M ` (bits o. ( A |` J ) ) ) ) C_ ran F
17	4, 5	oddpwdc 26759	. . . . . 6 |- F : ( J X. NN0 ) -1-1-onto-> NN
18		f1of 5662	. . . . . 6 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
19		frn 5586	. . . . . 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 3386	. . . 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 26495	. . 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 1218	. 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 5580	. . . . . 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 3591	. . . . . . . 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 26780	. . . . . . . . 9 |- ( A e. ( T i^i R ) -> (bits o. ( A |` J ) ) e. H )
30	1, 2, 3, 4, 5, 6, 7	eulerpartlem1 26772	. . . . . . . . . . 11 |- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
31		f1of 5662	. . . . . . . . . . 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 5863	. . . . . . . . 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 3375	. . . . . . 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 3891	. . . . 5 |- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` (bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
38		fvelimab 5768	. . . . 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 1673	. . . . . . 7 |- F/ w ( A e. ( T i^i R ) /\ B e. NN )
41		nfre1 2793	. . . . . . 7 |- F/ w E. w e. ( M ` (bits o. ( A |` J ) ) ) ( F ` w ) = B
42	40, 41	nfan 1861	. . . . . 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 3458	. . . . . . . . . . 11 |- { z e. NN | -. 2 || z } C_ NN
44	4, 43	eqsstri 3407	. . . . . . . . . 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 5711	. . . . . . . . . . . . . . . . . . . . 21 |- ( r = (bits o. ( A |` J ) ) -> ( r ` x ) = ( (bits o. ( A |` J ) ) ` x ) )
47	46	eleq2d 2510	. . . . . . . . . . . . . . . . . . . 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 4376	. . . . . . . . . . . . . . . . . 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 4458	. . . . . . . . . . . . . . . . . . 19 |- J e. _V
52		abid2 2567	. . . . . . . . . . . . . . . . . . . . 21 |- { y | y e. ( (bits o. ( A |` J ) ) ` x ) } = ( (bits o. ( A |` J ) ) ` x )
53		fvex 5722	. . . . . . . . . . . . . . . . . . . . 21 |- ( (bits o. ( A |` J ) ) ` x ) e. _V
54	52, 53	eqeltri 2513	. . . . . . . . . . . . . . . . . . . 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 6577	. . . . . . . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . . . 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 2509	. . . . . . . . . . . . . . . . . 18 |- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
61		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = t /\ y = n ) -> y = n )
62	59	fveq2d 5716	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = t /\ y = n ) -> ( (bits o. ( A |` J ) ) ` x ) = ( (bits o. ( A |` J ) ) ` t ) )
63	61, 62	eleq12d 2511	. . . . . . . . . . . . . . . . . 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 4382	. . . . . . . . . . . . . . . 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 2491	. . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . 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 26774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
69	68	simp1bi 1003	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
70		nn0ex 10606	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- NN0 e. _V
71	70, 14	elmap 7262	. . . . . . . . . . . . . . . . . . . . . . . . 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 5582	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A : NN --> NN0 -> Fun A )
74		funres 5478	. . . . . . . . . . . . . . . . . . . . . . . 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 5599	. . . . . . . . . . . . . . . . . . . . . . . . 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 5584	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
80	79	eleq2d 2510	. . . . . . . . . . . . . . . . . . . . . . . 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 5788	. . . . . . . . . . . . . . . . . . . . . 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 5725	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
86	85	fveq2d 5716	. . . . . . . . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( (bits o. ( A |` J ) ) ` t ) = (bits ` ( A ` t ) ) )
89	88	eleq2d 2510	. . . . . . . . . . . . . . . . . . 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 4376	. . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . . 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 4618	. . . . . . . . . . . . . . . 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 1635	. . . . . . . . . . . . . . . 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 2742	. . . . . . . . . . . . . . . . . . 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 1634	. . . . . . . . . . . . . . . . 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 2742	. . . . . . . . . . . . . . . . 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 1925	. . . . . . . . . . . . . . . . 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 5712	. . . . . . . . . . . . . . . . 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 13643	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` ( A ` t ) ) C_ NN0
113	112	sseli 3373	. . . . . . . . . . . . . . . . . . 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 4890	. . . . . . . . . . . . . . . . . 18 |- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
117	4, 5	oddpwdcv 26760	. . . . . . . . . . . . . . . . . . 19 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
118		vex 2996	. . . . . . . . . . . . . . . . . . . . . 22 |- t e. _V
119		vex 2996	. . . . . . . . . . . . . . . . . . . . . 22 |- n e. _V
120	118, 119	op2nd 6607	. . . . . . . . . . . . . . . . . . . . 21 |- ( 2nd ` <. t , n >. ) = n
121	120	oveq2i 6123	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
122	118, 119	op1st 6606	. . . . . . . . . . . . . . . . . . . 20 |- ( 1st ` <. t , n >. ) = t
123	121, 122	oveq12i 6124	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
124	117, 123	syl6eq 2491	. . . . . . . . . . . . . . . . . 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 2476	. . . . . . . . . . . . . . 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 2849	. . . . . . . . . . . 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 2849	. . . . . . . . . . 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 3438	. . . . . . . . . 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 2452	. . . . . . . . . . 11 |- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
137	136	rexbidv 2757	. . . . . . . . . 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 2757	. . . . . . . 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 2882	. . . . 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 2510	. . . . . . . . . . . . . 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 5788	. . . . . . . . . . . 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 5725	. . . . . . . . . . . . 13 |- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
154	153	fveq2d 5716	. . . . . . . . . . . 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 2475	. . . . . . . . . 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 2520	. . . . . . . 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 2510	. . . . . . . . . 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 4617	. . . . . . . . . 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 1216	. . . . . . 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 3378	. . . . . . . 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 4080	. . . . . . . . . . . 12 |- ( t = x -> <. t , y >. = <. x , y >. )
168	167	eleq1d 2509	. . . . . . . . . . 11 |- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
169	167	fveq2d 5716	. . . . . . . . . . . 12 |- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
170		oveq2 6120	. . . . . . . . . . . 12 |- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
171	169, 170	eqeq12d 2457	. . . . . . . . . . 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 4081	. . . . . . . . . . . . 13 |- ( n = y -> <. t , n >. = <. t , y >. )
174	173	eleq1d 2509	. . . . . . . . . . . 12 |- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
175	173	fveq2d 5716	. . . . . . . . . . . . 13 |- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
176		oveq2 6120	. . . . . . . . . . . . . 14 |- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
177	176	oveq1d 6127	. . . . . . . . . . . . 13 |- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
178	175, 177	eqeq12d 2457	. . . . . . . . . . . 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 1958	. . . . . . . . . 10 |- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
181	172, 180	chvarv 1958	. . . . . . . . 9 |- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
182		eqeq2 2452	. . . . . . . . . 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 5712	. . . . . . . . 9 |- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
187	186	eqeq1d 2451	. . . . . . . 8 |- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
188	187	rspcev 3094	. . . . . . 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 6120	. . . . . . . . . . 11 |- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
191	190	eqeq1d 2451	. . . . . . . . . 10 |- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
192	176	oveq1d 6127	. . . . . . . . . . 11 |- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
193	192	eqeq1d 2451	. . . . . . . . . 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 5716	. . . . . . . . . 10 |- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
197	196	fveq2d 5716	. . . . . . . . 9 |- ( ( t = x /\ n = y ) -> (bits ` ( A ` t ) ) = (bits ` ( A ` x ) ) )
198	194, 197	cbvrexdva2 2973	. . . . . . . 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 2969	. . . . . . 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 1673	. . . . . . . . . . . . . 14 |- F/ y A e. ( T i^i R )
201		nfv 1673	. . . . . . . . . . . . . . 15 |- F/ y x e. NN
202		nfre1 2793	. . . . . . . . . . . . . . 15 |- F/ y E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
203	201, 202	nfan 1861	. . . . . . . . . . . . . 14 |- F/ y ( x e. NN /\ E. y e. (bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
204	200, 203	nfan 1861	. . . . . . . . . . . . 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 3663	. . . . . . . . . . . . . . . . . . . 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 5712	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` x ) = 0 -> (bits ` ( A ` x ) ) = (bits ` 0 ) )
209		0bits 13656	. . . . . . . . . . . . . . . . . . . 20 |- (bits ` 0 ) = (/)
210	208, 209	syl6eq 2491	. . . . . . . . . . . . . . . . . . 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 5864	. . . . . . . . . . . . . . . . . . . . . 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 10602	. . . . . . . . . . . . . . . . . . . . 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 904	. . . . . . . . . . . . . . . . . 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 1005	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
220	219	sselda 3377	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
221		breq2 4317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z = n -> ( 2 || z <-> 2 || n ) )
222	221	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
223	222, 4	elrab2 3140	. . . . . . . . . . . . . . . . . . . . . . . 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 2820	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
227		ffn 5580	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A : NN --> NN0 -> A Fn NN )
228		elpreima 5844	. . . . . . . . . . . . . . . . . . . . . . . . 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 2758	. . . . . . . . . . . . . . . . . . . . 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 5712	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = n -> ( A ` x ) = ( A ` n ) )
236	235	eleq1d 2509	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
237		breq2 4317	. . . . . . . . . . . . . . . . . . . . . . 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 2968	. . . . . . . . . . . . . . . . . . . 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 2835	. . . . . . . . . . . . . . . . . 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 4317	. . . . . . . . . . . . . . . . . 18 |- ( z = x -> ( 2 || z <-> 2 || x ) )
246	245	notbid 294	. . . . . . . . . . . . . . . . 17 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
247	246, 4	elrab2 3140	. . . . . . . . . . . . . . . 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 2882	. . . . . . . . . . . 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 2846	. . . . . . . . 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 2885	. . . . 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 828	. . . 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 3832	. 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 2479	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 1369   E.wex 1586   e. wcel 1756   {cab 2429   A.wral 2736   E.wrex 2737   {crab 2740   _Vcvv 2993   i^i cin 3348   C_ wss 3349   (/)c0 3658   ifcif 3812   ~Pcpw 3881   <.cop 3904   class class class wbr 4313   {copab 4370   e. cmpt 4371   X. cxp 4859   `'ccnv 4860   dom cdm 4861   ran crn 4862   |` cres 4863   "cima 4864   o. ccom 4865   Fun wfun 5433   Fn wfn 5434   -->wf 5435   -1-1-onto->wf1o 5438   ` cfv 5439  (class class class)co 6112   e. cmpt2 6114   1stc1st 6596   2ndc2nd 6597   supp csupp 6711   ^m cmap 7235   Fincfn 7331   0cc0 9303   1c1 9304   x. cmul 9308   <_ cle 9440   NNcn 10343   2c2 10392   NN0cn0 10600   ^cexp 11886   sum_csu 13184   || cdivides 13556  bitscbits 13636  𝟭cind 26489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-ac2 8653  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-disj 4284  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-pm 7238  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-sup 7712  df-oi 7745  df-card 8130  df-acn 8133  df-ac 8307  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-n0 10601  df-z 10668  df-uz 10883  df-rp 11013  df-fz 11459  df-fzo 11570  df-fl 11663  df-mod 11730  df-seq 11828  df-exp 11887  df-hash 12125  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-clim 12987  df-sum 13185  df-dvds 13557  df-bits 13639  df-ind 26490

This theorem is referenced by:  eulerpartlemgs2  26785