Theorem eulerpartlemgvv

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

	Ref	Expression
Hypotheses	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 ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
Assertion	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 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2		eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3		eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4		eulerpart.j	|- J = { z e. NN | -. 2 || z }
5		eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6		eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7		eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8		eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
9		eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10		eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
11	1 2 3 4 5 6 7 8 9 10	eulerpartlemgv	|- ( A e. ( T i^i R ) -> ( G ` A ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )
12	11	fveq1d	|- ( A e. ( T i^i R ) -> ( ( G ` A ) ` B ) = ( ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) ` B ) )
13	12	adantr	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( G ` A ) ` B ) = ( ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) ` B ) )
14		nnex	|- NN e. _V
15		imassrn	|- ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ ran F
16	4 5	oddpwdc	|- F : ( J X. NN0 ) -1-1-onto-> NN
17		f1of	|- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) --> NN )
18		frn	|- ( F : ( J X. NN0 ) --> NN -> ran F C_ NN )
19	16 17 18	mp2b	|- ran F C_ NN
20	15 19	sstri	|- ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ NN
21		simpr	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> B e. NN )
22		indfval	|- ( ( NN e. _V /\ ( F " ( M ` ( bits o. ( A |` J ) ) ) ) C_ NN /\ B e. NN ) -> ( ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) ` B ) = if ( B e. ( F " ( M ` ( bits o. ( A |` J ) ) ) ) , 1 , 0 ) )
23	14 20 21 22	mp3an12i	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) ` B ) = if ( B e. ( F " ( M ` ( bits o. ( A |` J ) ) ) ) , 1 , 0 ) )
24		ffn	|- ( F : ( J X. NN0 ) --> NN -> F Fn ( J X. NN0 ) )
25	16 17 24	mp2b	|- F Fn ( J X. NN0 )
26	1 2 3 4 5 6 7 8 9 10	eulerpartlemmf	|- ( A e. ( T i^i R ) -> ( bits o. ( A |` J ) ) e. H )
27	1 2 3 4 5 6 7	eulerpartlem1	|- M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin )
28		f1of	|- ( M : H -1-1-onto-> ( ~P ( J X. NN0 ) i^i Fin ) -> M : H --> ( ~P ( J X. NN0 ) i^i Fin ) )
29	27 28	ax-mp	|- M : H --> ( ~P ( J X. NN0 ) i^i Fin )
30	29	ffvelcdmi	|- ( ( bits o. ( A |` J ) ) e. H -> ( M ` ( bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
31	26 30	syl	|- ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) e. ( ~P ( J X. NN0 ) i^i Fin ) )
32	31	elin1d	|- ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
33	32	adantr	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` ( bits o. ( A |` J ) ) ) e. ~P ( J X. NN0 ) )
34	33	elpwid	|- ( ( A e. ( T i^i R ) /\ B e. NN ) -> ( M ` ( bits o. ( A |` J ) ) ) C_ ( J X. NN0 ) )
35		fvelimab	|- ( ( 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 ) )
36	25 34 35	sylancr	|- ( ( 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 ) )
37	4	ssrab3	|- J C_ NN
38		fveq1	|- ( r = ( bits o. ( A |` J ) ) -> ( r ` x ) = ( ( bits o. ( A |` J ) ) ` x ) )
39	38	eleq2d	|- ( r = ( bits o. ( A |` J ) ) -> ( y e. ( r ` x ) <-> y e. ( ( bits o. ( A |` J ) ) ` x ) ) )
40	39	anbi2d	|- ( r = ( bits o. ( A |` J ) ) -> ( ( x e. J /\ y e. ( r ` x ) ) <-> ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) ) )
41	40	opabbidv	|- ( 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 ) ) } )
42	14 37	ssexi	|- J e. _V
43		abid2	|- { y | y e. ( ( bits o. ( A |` J ) ) ` x ) } = ( ( bits o. ( A |` J ) ) ` x )
44	43	fvexi	|- { y | y e. ( ( bits o. ( A |` J ) ) ` x ) } e. _V
45	44	a1i	|- ( x e. J -> { y | y e. ( ( bits o. ( A |` J ) ) ` x ) } e. _V )
46	42 45	opabex3	|- { <. x , y >. | ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) } e. _V
47	46	a1i	|- ( A e. ( T i^i R ) -> { <. x , y >. | ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) } e. _V )
48	7 41 26 47	fvmptd3	|- ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) = { <. x , y >. | ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) } )
49		simpl	|- ( ( x = t /\ y = n ) -> x = t )
50	49	eleq1d	|- ( ( x = t /\ y = n ) -> ( x e. J <-> t e. J ) )
51		simpr	|- ( ( x = t /\ y = n ) -> y = n )
52	49	fveq2d	|- ( ( x = t /\ y = n ) -> ( ( bits o. ( A |` J ) ) ` x ) = ( ( bits o. ( A |` J ) ) ` t ) )
53	51 52	eleq12d	|- ( ( x = t /\ y = n ) -> ( y e. ( ( bits o. ( A |` J ) ) ` x ) <-> n e. ( ( bits o. ( A |` J ) ) ` t ) ) )
54	50 53	anbi12d	|- ( ( x = t /\ y = n ) -> ( ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) <-> ( t e. J /\ n e. ( ( bits o. ( A |` J ) ) ` t ) ) ) )
55	54	cbvopabv	|- { <. x , y >. | ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) } = { <. t , n >. | ( t e. J /\ n e. ( ( bits o. ( A |` J ) ) ` t ) ) }
56	48 55	eqtrdi	|- ( A e. ( T i^i R ) -> ( M ` ( bits o. ( A |` J ) ) ) = { <. t , n >. | ( t e. J /\ n e. ( ( bits o. ( A |` J ) ) ` t ) ) } )
57	56	eleq2d	|- ( 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 ) ) } ) )
58	1 2 3 4 5 6 7 8 9	eulerpartlemt0	|- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
59	58	simp1bi	|- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
60		nn0ex	|- NN0 e. _V
61	60 14	elmap	|- ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
62	59 61	sylib	|- ( A e. ( T i^i R ) -> A : NN --> NN0 )
63		ffun	|- ( A : NN --> NN0 -> Fun A )
64		funres	|- ( Fun A -> Fun ( A |` J ) )
65	62 63 64	3syl	|- ( A e. ( T i^i R ) -> Fun ( A |` J ) )
66		fssres	|- ( ( A : NN --> NN0 /\ J C_ NN ) -> ( A |` J ) : J --> NN0 )
67	62 37 66	sylancl	|- ( A e. ( T i^i R ) -> ( A |` J ) : J --> NN0 )
68		fdm	|- ( ( A |` J ) : J --> NN0 -> dom ( A |` J ) = J )
69	68	eleq2d	|- ( ( A |` J ) : J --> NN0 -> ( t e. dom ( A |` J ) <-> t e. J ) )
70	67 69	syl	|- ( A e. ( T i^i R ) -> ( t e. dom ( A |` J ) <-> t e. J ) )
71	70	biimpar	|- ( ( A e. ( T i^i R ) /\ t e. J ) -> t e. dom ( A |` J ) )
72		fvco	|- ( ( Fun ( A |` J ) /\ t e. dom ( A |` J ) ) -> ( ( bits o. ( A |` J ) ) ` t ) = ( bits ` ( ( A |` J ) ` t ) ) )
73	65 71 72	syl2an2r	|- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( ( bits o. ( A |` J ) ) ` t ) = ( bits ` ( ( A |` J ) ` t ) ) )
74		fvres	|- ( t e. J -> ( ( A |` J ) ` t ) = ( A ` t ) )
75	74	fveq2d	|- ( t e. J -> ( bits ` ( ( A |` J ) ` t ) ) = ( bits ` ( A ` t ) ) )
76	75	adantl	|- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( bits ` ( ( A |` J ) ` t ) ) = ( bits ` ( A ` t ) ) )
77	73 76	eqtrd	|- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( ( bits o. ( A |` J ) ) ` t ) = ( bits ` ( A ` t ) ) )
78	77	eleq2d	|- ( ( A e. ( T i^i R ) /\ t e. J ) -> ( n e. ( ( bits o. ( A |` J ) ) ` t ) <-> n e. ( bits ` ( A ` t ) ) ) )
79	78	pm5.32da	|- ( A e. ( T i^i R ) -> ( ( t e. J /\ n e. ( ( bits o. ( A |` J ) ) ` t ) ) <-> ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) ) )
80	79	opabbidv	|- ( 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 ) ) ) } )
81	80	eleq2d	|- ( 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 ) ) ) } ) )
82		elopab	|- ( 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 ) ) ) ) )
83	81 82	bitrdi	|- ( 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 ) ) ) ) ) )
84		ancom	|- ( ( w = <. t , n >. /\ ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) ) <-> ( ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) )
85		anass	|- ( ( ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) /\ w = <. t , n >. ) <-> ( t e. J /\ ( n e. ( bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
86	84 85	bitri	|- ( ( w = <. t , n >. /\ ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) ) <-> ( t e. J /\ ( n e. ( bits ` ( A ` t ) ) /\ w = <. t , n >. ) ) )
87	86	2exbii	|- ( 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 >. ) ) )
88		df-rex	|- ( E. n e. ( bits ` ( A ` t ) ) w = <. t , n >. <-> E. n ( n e. ( bits ` ( A ` t ) ) /\ w = <. t , n >. ) )
89	88	anbi2i	|- ( ( 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 >. ) ) )
90	89	exbii	|- ( 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 >. ) ) )
91		df-rex	|- ( 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 >. ) )
92		exdistr	|- ( 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 >. ) ) )
93	90 91 92	3bitr4i	|- ( 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 >. ) ) )
94	87 93	bitr4i	|- ( 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 >. )
95	83 94	bitrdi	|- ( 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 >. ) )
96	57 95	bitrd	|- ( 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 >. ) )
97	96	biimpa	|- ( ( 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 >. )
98	97	adantlr	|- ( ( ( 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 >. )
99		fveq2	|- ( w = <. t , n >. -> ( F ` w ) = ( F ` <. t , n >. ) )
100	99	adantl	|- ( ( ( ( ( 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 >. ) )
101		bitsss	|- ( bits ` ( A ` t ) ) C_ NN0
102	101	sseli	|- ( n e. ( bits ` ( A ` t ) ) -> n e. NN0 )
103	102	anim2i	|- ( ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) -> ( t e. J /\ n e. NN0 ) )
104	103	ad2antlr	|- ( ( ( ( ( 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 ) )
105		opelxp	|- ( <. t , n >. e. ( J X. NN0 ) <-> ( t e. J /\ n e. NN0 ) )
106	4 5	oddpwdcv	|- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
107		vex	|- t e. _V
108		vex	|- n e. _V
109	107 108	op2nd	|- ( 2nd ` <. t , n >. ) = n
110	109	oveq2i	|- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
111	107 108	op1st	|- ( 1st ` <. t , n >. ) = t
112	110 111	oveq12i	|- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
113	106 112	eqtrdi	|- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
114	105 113	sylbir	|- ( ( t e. J /\ n e. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
115	104 114	syl	|- ( ( ( ( ( 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 ) )
116	100 115	eqtr2d	|- ( ( ( ( ( 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 ) )
117	116	ex	|- ( ( ( ( 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 ) ) )
118	117	reximdvva	|- ( ( ( 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 ) ) )
119	98 118	mpd	|- ( ( ( 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 ) )
120		ssrexv	|- ( 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 ) ) )
121	37 119 120	mpsyl	|- ( ( ( 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 ) )
122	121	adantr	|- ( ( ( ( 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 ) )
123		eqeq2	|- ( ( F ` w ) = B -> ( ( ( 2 ^ n ) x. t ) = ( F ` w ) <-> ( ( 2 ^ n ) x. t ) = B ) )
124	123	rexbidv	|- ( ( 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 ) )
125	124	adantl	|- ( ( ( ( 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 ) )
126	125	rexbidv	|- ( ( ( ( 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 ) )
127	122 126	mpbid	|- ( ( ( ( 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 )
128	127	r19.29an	|- ( ( ( 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 )
129		simp-5l	|- ( ( ( ( ( ( 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 ) )
130		simpllr	|- ( ( ( ( ( ( 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 )
131		simplr	|- ( ( ( ( ( ( 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 ) ) )
132	68	eleq2d	|- ( ( A |` J ) : J --> NN0 -> ( x e. dom ( A |` J ) <-> x e. J ) )
133	67 132	syl	|- ( A e. ( T i^i R ) -> ( x e. dom ( A |` J ) <-> x e. J ) )
134	133	biimpar	|- ( ( A e. ( T i^i R ) /\ x e. J ) -> x e. dom ( A |` J ) )
135		fvco	|- ( ( Fun ( A |` J ) /\ x e. dom ( A |` J ) ) -> ( ( bits o. ( A |` J ) ) ` x ) = ( bits ` ( ( A |` J ) ` x ) ) )
136	65 134 135	syl2an2r	|- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( ( bits o. ( A |` J ) ) ` x ) = ( bits ` ( ( A |` J ) ` x ) ) )
137		fvres	|- ( x e. J -> ( ( A |` J ) ` x ) = ( A ` x ) )
138	137	fveq2d	|- ( x e. J -> ( bits ` ( ( A |` J ) ` x ) ) = ( bits ` ( A ` x ) ) )
139	138	adantl	|- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( bits ` ( ( A |` J ) ` x ) ) = ( bits ` ( A ` x ) ) )
140	136 139	eqtrd	|- ( ( A e. ( T i^i R ) /\ x e. J ) -> ( ( bits o. ( A |` J ) ) ` x ) = ( bits ` ( A ` x ) ) )
141	129 130 140	syl2anc	|- ( ( ( ( ( ( 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 ) ) )
142	131 141	eleqtrrd	|- ( ( ( ( ( ( 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 ) )
143	48	eleq2d	|- ( 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 ) ) } ) )
144		opabidw	|- ( <. 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 ) ) )
145	143 144	bitrdi	|- ( A e. ( T i^i R ) -> ( <. x , y >. e. ( M ` ( bits o. ( A |` J ) ) ) <-> ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) ) )
146	145	biimpar	|- ( ( A e. ( T i^i R ) /\ ( x e. J /\ y e. ( ( bits o. ( A |` J ) ) ` x ) ) ) -> <. x , y >. e. ( M ` ( bits o. ( A |` J ) ) ) )
147	129 130 142 146	syl12anc	|- ( ( ( ( ( ( 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 ) ) ) )
148		simpr	|- ( ( ( ( ( ( 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 )
149	34	ad4antr	|- ( ( ( ( ( ( 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 ) )
150	149 147	sseldd	|- ( ( ( ( ( ( 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 ) )
151		opeq1	|- ( t = x -> <. t , y >. = <. x , y >. )
152	151	eleq1d	|- ( t = x -> ( <. t , y >. e. ( J X. NN0 ) <-> <. x , y >. e. ( J X. NN0 ) ) )
153	151	fveq2d	|- ( t = x -> ( F ` <. t , y >. ) = ( F ` <. x , y >. ) )
154		oveq2	|- ( t = x -> ( ( 2 ^ y ) x. t ) = ( ( 2 ^ y ) x. x ) )
155	153 154	eqeq12d	|- ( t = x -> ( ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) <-> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) )
156	152 155	imbi12d	|- ( 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 ) ) ) )
157		opeq2	|- ( n = y -> <. t , n >. = <. t , y >. )
158	157	eleq1d	|- ( n = y -> ( <. t , n >. e. ( J X. NN0 ) <-> <. t , y >. e. ( J X. NN0 ) ) )
159	157	fveq2d	|- ( n = y -> ( F ` <. t , n >. ) = ( F ` <. t , y >. ) )
160		oveq2	|- ( n = y -> ( 2 ^ n ) = ( 2 ^ y ) )
161	160	oveq1d	|- ( n = y -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ y ) x. t ) )
162	159 161	eqeq12d	|- ( n = y -> ( ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) <-> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) ) )
163	158 162	imbi12d	|- ( 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 ) ) ) )
164	163 113	chvarvv	|- ( <. t , y >. e. ( J X. NN0 ) -> ( F ` <. t , y >. ) = ( ( 2 ^ y ) x. t ) )
165	156 164	chvarvv	|- ( <. x , y >. e. ( J X. NN0 ) -> ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) )
166		eqeq2	|- ( ( ( 2 ^ y ) x. x ) = B -> ( ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) <-> ( F ` <. x , y >. ) = B ) )
167	166	biimpa	|- ( ( ( ( 2 ^ y ) x. x ) = B /\ ( F ` <. x , y >. ) = ( ( 2 ^ y ) x. x ) ) -> ( F ` <. x , y >. ) = B )
168	165 167	sylan2	|- ( ( ( ( 2 ^ y ) x. x ) = B /\ <. x , y >. e. ( J X. NN0 ) ) -> ( F ` <. x , y >. ) = B )
169	148 150 168	syl2anc	|- ( ( ( ( ( ( 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 )
170		fveqeq2	|- ( w = <. x , y >. -> ( ( F ` w ) = B <-> ( F ` <. x , y >. ) = B ) )
171	170	rspcev	|- ( ( <. x , y >. e. ( M ` ( bits o. ( A |` J ) ) ) /\ ( F ` <. x , y >. ) = B ) -> E. w e. ( M ` ( bits o. ( A |` J ) ) ) ( F ` w ) = B )
172	147 169 171	syl2anc	|- ( ( ( ( ( ( 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 )
173		oveq2	|- ( t = x -> ( ( 2 ^ n ) x. t ) = ( ( 2 ^ n ) x. x ) )
174	173	eqeq1d	|- ( t = x -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ n ) x. x ) = B ) )
175	160	oveq1d	|- ( n = y -> ( ( 2 ^ n ) x. x ) = ( ( 2 ^ y ) x. x ) )
176	175	eqeq1d	|- ( n = y -> ( ( ( 2 ^ n ) x. x ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
177	174 176	sylan9bb	|- ( ( t = x /\ n = y ) -> ( ( ( 2 ^ n ) x. t ) = B <-> ( ( 2 ^ y ) x. x ) = B ) )
178		simpl	|- ( ( t = x /\ n = y ) -> t = x )
179	178	fveq2d	|- ( ( t = x /\ n = y ) -> ( A ` t ) = ( A ` x ) )
180	179	fveq2d	|- ( ( t = x /\ n = y ) -> ( bits ` ( A ` t ) ) = ( bits ` ( A ` x ) ) )
181	177 180	cbvrexdva2	|- ( t = x -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = B <-> E. y e. ( bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
182	181	cbvrexvw	|- ( 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 )
183		nfv	|- F/ y A e. ( T i^i R )
184		nfv	|- F/ y x e. NN
185		nfre1	|- F/ y E. y e. ( bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B
186	184 185	nfan	|- F/ y ( x e. NN /\ E. y e. ( bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B )
187	183 186	nfan	|- F/ y ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. ( bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) )
188		simplr	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> x e. NN )
189	62	ffvelcdmda	|- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( A ` x ) e. NN0 )
190	189	adantr	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN0 )
191		elnn0	|- ( ( A ` x ) e. NN0 <-> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
192	190 191	sylib	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> ( ( A ` x ) e. NN \/ ( A ` x ) = 0 ) )
193		n0i	|- ( y e. ( bits ` ( A ` x ) ) -> -. ( bits ` ( A ` x ) ) = (/) )
194	193	adantl	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> -. ( bits ` ( A ` x ) ) = (/) )
195		fveq2	|- ( ( A ` x ) = 0 -> ( bits ` ( A ` x ) ) = ( bits ` 0 ) )
196		0bits	|- ( bits ` 0 ) = (/)
197	195 196	eqtrdi	|- ( ( A ` x ) = 0 -> ( bits ` ( A ` x ) ) = (/) )
198	194 197	nsyl	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> -. ( A ` x ) = 0 )
199	192 198	olcnd	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> ( A ` x ) e. NN )
200	58	simp3bi	|- ( A e. ( T i^i R ) -> ( `' A " NN ) C_ J )
201	200	sselda	|- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> n e. J )
202		breq2	|- ( z = n -> ( 2 || z <-> 2 || n ) )
203	202	notbid	|- ( z = n -> ( -. 2 || z <-> -. 2 || n ) )
204	203 4	elrab2	|- ( n e. J <-> ( n e. NN /\ -. 2 || n ) )
205	204	simprbi	|- ( n e. J -> -. 2 || n )
206	201 205	syl	|- ( ( A e. ( T i^i R ) /\ n e. ( `' A " NN ) ) -> -. 2 || n )
207	206	ralrimiva	|- ( A e. ( T i^i R ) -> A. n e. ( `' A " NN ) -. 2 || n )
208		ffn	|- ( A : NN --> NN0 -> A Fn NN )
209		elpreima	|- ( A Fn NN -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
210	62 208 209	3syl	|- ( A e. ( T i^i R ) -> ( n e. ( `' A " NN ) <-> ( n e. NN /\ ( A ` n ) e. NN ) ) )
211	210	imbi1d	|- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) ) )
212		impexp	|- ( ( ( n e. NN /\ ( A ` n ) e. NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
213	211 212	bitrdi	|- ( A e. ( T i^i R ) -> ( ( n e. ( `' A " NN ) -> -. 2 || n ) <-> ( n e. NN -> ( ( A ` n ) e. NN -> -. 2 || n ) ) ) )
214	213	ralbidv2	|- ( A e. ( T i^i R ) -> ( A. n e. ( `' A " NN ) -. 2 || n <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) ) )
215	207 214	mpbid	|- ( A e. ( T i^i R ) -> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
216		fveq2	|- ( x = n -> ( A ` x ) = ( A ` n ) )
217	216	eleq1d	|- ( x = n -> ( ( A ` x ) e. NN <-> ( A ` n ) e. NN ) )
218		breq2	|- ( x = n -> ( 2 || x <-> 2 || n ) )
219	218	notbid	|- ( x = n -> ( -. 2 || x <-> -. 2 || n ) )
220	217 219	imbi12d	|- ( x = n -> ( ( ( A ` x ) e. NN -> -. 2 || x ) <-> ( ( A ` n ) e. NN -> -. 2 || n ) ) )
221	220	cbvralvw	|- ( A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) <-> A. n e. NN ( ( A ` n ) e. NN -> -. 2 || n ) )
222	215 221	sylibr	|- ( A e. ( T i^i R ) -> A. x e. NN ( ( A ` x ) e. NN -> -. 2 || x ) )
223	222	r19.21bi	|- ( ( A e. ( T i^i R ) /\ x e. NN ) -> ( ( A ` x ) e. NN -> -. 2 || x ) )
224	223	imp	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ ( A ` x ) e. NN ) -> -. 2 || x )
225	199 224	syldan	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> -. 2 || x )
226		breq2	|- ( z = x -> ( 2 || z <-> 2 || x ) )
227	226	notbid	|- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
228	227 4	elrab2	|- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
229	188 225 228	sylanbrc	|- ( ( ( A e. ( T i^i R ) /\ x e. NN ) /\ y e. ( bits ` ( A ` x ) ) ) -> x e. J )
230	229	adantlrr	|- ( ( ( 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 )
231	230	adantr	|- ( ( ( ( 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 )
232		simprr	|- ( ( 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 )
233	187 231 232	r19.29af	|- ( ( A e. ( T i^i R ) /\ ( x e. NN /\ E. y e. ( bits ` ( A ` x ) ) ( ( 2 ^ y ) x. x ) = B ) ) -> x e. J )
234	233 232	jca	|- ( ( 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 ) )
235	234	ex	|- ( 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 ) ) )
236	235	reximdv2	|- ( 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 ) )
237	236	imp	|- ( ( 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 )
238	237	adantlr	|- ( ( ( 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 )
239	182 238	sylan2b	|- ( ( ( 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 )
240	172 239	r19.29vva	|- ( ( ( 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 )
241	128 240	impbida	|- ( ( 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 ) )
242	36 241	bitrd	|- ( ( 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 ) )
243	242	ifbid	|- ( ( 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 ) )
244	13 23 243	3eqtrd	|- ( ( 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 ) )