Theorem eulerpartlemgh 30440

Description: Lemma for eulerpart 30444: The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-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 ) ) ) ) ) )
eulerpartlemgh.1	|- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) )

Assertion

Ref	Expression
eulerpartlemgh	|- ( A e. ( T i^i R ) -> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )

Distinct variable groups:   z, t   f, g, k, n, t, A   f, J, n, t   f, N, k, n, t   n, O, t   P, g, k   R, f, k, n, t   T, n, t   x, t, y, z   f, m, x, g, k, n, t, A   n, F, t, x   y, f, n   x, J, y   t, P

Allowed substitution hints:   A( y, z, o, r)   D( x, y, z, t, f, g, k, m, n, o, r)   P( x, y, z, f, m, n, o, r)   R( x, y, z, g, m, o, r)   T( x, y, z, f, g, k, m, o, r)   U( x, y, z, t, f, g, k, m, n, o, r)   F( y, z, f, g, k, m, o, r)   G( x, y, z, t, f, g, k, m, n, o, r)   H( x, y, z, t, f, g, k, m, n, o, r)   J( z, g, k, m, o, r)   M( x, y, z, t, f, g, k, m, n, o, r)   N( x, y, z, g, m, o, r)   O( x, y, z, f, g, k, m, o, r)

Proof of Theorem eulerpartlemgh

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerpart.j	. . . . 5 |- J = { z e. NN | -. 2 || z }
2		eulerpart.f	. . . . 5 |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
3	1, 2	oddpwdc 30416	. . . 4 |- F : ( J X. NN0 ) -1-1-onto-> NN
4		f1of1 6136	. . . 4 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) -1-1-> NN )
5	3, 4	ax-mp 5	. . 3 |- F : ( J X. NN0 ) -1-1-> NN
6		eulerpartlemgh.1	. . . 4 |- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) )
7		iunss 4561	. . . . 5 |- ( U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) <-> A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
8		inss2 3834	. . . . . . . 8 |- ( ( `' A " NN ) i^i J ) C_ J
9	8	sseli 3599	. . . . . . 7 |- ( t e. ( ( `' A " NN ) i^i J ) -> t e. J )
10	9	snssd 4340	. . . . . 6 |- ( t e. ( ( `' A " NN ) i^i J ) -> { t } C_ J )
11		bitsss 15148	. . . . . 6 |- (bits ` ( A ` t ) ) C_ NN0
12		xpss12 5225	. . . . . 6 |- ( ( { t } C_ J /\ (bits ` ( A ` t ) ) C_ NN0 ) -> ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
13	10, 11, 12	sylancl 694	. . . . 5 |- ( t e. ( ( `' A " NN ) i^i J ) -> ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
14	7, 13	mprgbir 2927	. . . 4 |- U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 )
15	6, 14	eqsstri 3635	. . 3 |- U C_ ( J X. NN0 )
16		f1ores 6151	. . 3 |- ( ( F : ( J X. NN0 ) -1-1-> NN /\ U C_ ( J X. NN0 ) ) -> ( F |` U ) : U -1-1-onto-> ( F " U ) )
17	5, 15, 16	mp2an 708	. 2 |- ( F |` U ) : U -1-1-onto-> ( F " U )
18		simpr 477	. . . . . . . . . . 11 |- ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> ( ( 2 ^ n ) x. t ) = p )
19		2nn 11185	. . . . . . . . . . . . . . 15 |- 2 e. NN
20	19	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) -> 2 e. NN )
21	11	sseli 3599	. . . . . . . . . . . . . . 15 |- ( n e. (bits ` ( A ` t ) ) -> n e. NN0 )
22	21	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) -> n e. NN0 )
23	20, 22	nnexpcld 13030	. . . . . . . . . . . . 13 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) -> ( 2 ^ n ) e. NN )
24		simplr 792	. . . . . . . . . . . . 13 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) -> t e. NN )
25	23, 24	nnmulcld 11068	. . . . . . . . . . . 12 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) -> ( ( 2 ^ n ) x. t ) e. NN )
26	25	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> ( ( 2 ^ n ) x. t ) e. NN )
27	18, 26	eqeltrrd 2702	. . . . . . . . . 10 |- ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. (bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> p e. NN )
28	27	exp31 630	. . . . . . . . 9 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( n e. (bits ` ( A ` t ) ) -> ( ( ( 2 ^ n ) x. t ) = p -> p e. NN ) ) )
29	28	rexlimdv 3030	. . . . . . . 8 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> p e. NN ) )
30	29	rexlimdva 3031	. . . . . . 7 |- ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> p e. NN ) )
31	30	pm4.71rd 667	. . . . . 6 |- ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> ( p e. NN /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
32		rex0 3938	. . . . . . . . . . . . . . 15 |- -. E. n e. (/) ( ( 2 ^ n ) x. t ) = p
33		simplr 792	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> t e. NN )
34		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. t e. ( `' A " NN ) )
35		eulerpart.p	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
36		eulerpart.o	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
37		eulerpart.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
38		eulerpart.h	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
39		eulerpart.m	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
40		eulerpart.r	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- R = { f | ( `' f " NN ) e. Fin }
41		eulerpart.t	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
42	35, 36, 37, 1, 2, 38, 39, 40, 41	eulerpartlemt0 30431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
43	42	simp1bi 1076	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
44		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
45	43, 44	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A e. ( T i^i R ) -> A : NN --> NN0 )
46	45	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> A : NN --> NN0 )
47		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A : NN --> NN0 -> A Fn NN )
48		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( A Fn NN -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
49	46, 47, 48	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
50	34, 49	mtbid 314	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. ( t e. NN /\ ( A ` t ) e. NN ) )
51		imnan 438	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( t e. NN -> -. ( A ` t ) e. NN ) <-> -. ( t e. NN /\ ( A ` t ) e. NN ) )
52	50, 51	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( t e. NN -> -. ( A ` t ) e. NN ) )
53	33, 52	mpd 15	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. ( A ` t ) e. NN )
54	46, 33	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( A ` t ) e. NN0 )
55		elnn0 11294	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A ` t ) e. NN0 <-> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
56	54, 55	sylib 208	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
57		orel1 397	. . . . . . . . . . . . . . . . . . 19 |- ( -. ( A ` t ) e. NN -> ( ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) -> ( A ` t ) = 0 ) )
58	53, 56, 57	sylc 65	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( A ` t ) = 0 )
59	58	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> (bits ` ( A ` t ) ) = (bits ` 0 ) )
60		0bits 15161	. . . . . . . . . . . . . . . . 17 |- (bits ` 0 ) = (/)
61	59, 60	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> (bits ` ( A ` t ) ) = (/) )
62	61	rexeqdv 3145	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. n e. (/) ( ( 2 ^ n ) x. t ) = p ) )
63	32, 62	mtbiri 317	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
64	63	ex 450	. . . . . . . . . . . . 13 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( -. t e. ( `' A " NN ) -> -. E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
65	64	con4d 114	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> t e. ( `' A " NN ) ) )
66	65	impr 649	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. ( `' A " NN ) )
67		eldif 3584	. . . . . . . . . . . . . . . . . . . 20 |- ( t e. ( NN \ J ) <-> ( t e. NN /\ -. t e. J ) )
68	35, 36, 37, 1, 2, 38, 39, 40, 41	eulerpartlemf 30432	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) = 0 )
69	67, 68	sylan2br 493	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ -. t e. J ) ) -> ( A ` t ) = 0 )
70	69	anassrs 680	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( A ` t ) = 0 )
71	70	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> (bits ` ( A ` t ) ) = (bits ` 0 ) )
72	71, 60	syl6eq 2672	. . . . . . . . . . . . . . . 16 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> (bits ` ( A ` t ) ) = (/) )
73	72	rexeqdv 3145	. . . . . . . . . . . . . . 15 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. n e. (/) ( ( 2 ^ n ) x. t ) = p ) )
74	32, 73	mtbiri 317	. . . . . . . . . . . . . 14 |- ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> -. E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
75	74	ex 450	. . . . . . . . . . . . 13 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( -. t e. J -> -. E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
76	75	con4d 114	. . . . . . . . . . . 12 |- ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> t e. J ) )
77	76	impr 649	. . . . . . . . . . 11 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. J )
78	66, 77	elind 3798	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. ( ( `' A " NN ) i^i J ) )
79		simprr 796	. . . . . . . . . 10 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
80	78, 79	jca 554	. . . . . . . . 9 |- ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> ( t e. ( ( `' A " NN ) i^i J ) /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
81	80	ex 450	. . . . . . . 8 |- ( A e. ( T i^i R ) -> ( ( t e. NN /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) -> ( t e. ( ( `' A " NN ) i^i J ) /\ E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
82	81	reximdv2 3014	. . . . . . 7 |- ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
83		ssrab2 3687	. . . . . . . . . 10 |- { z e. NN | -. 2 || z } C_ NN
84	1, 83	eqsstri 3635	. . . . . . . . 9 |- J C_ NN
85	8, 84	sstri 3612	. . . . . . . 8 |- ( ( `' A " NN ) i^i J ) C_ NN
86		ssrexv 3667	. . . . . . . 8 |- ( ( ( `' A " NN ) i^i J ) C_ NN -> ( E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
87	85, 86	mp1i 13	. . . . . . 7 |- ( A e. ( T i^i R ) -> ( E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
88	82, 87	impbid 202	. . . . . 6 |- ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
89	31, 88	bitr3d 270	. . . . 5 |- ( A e. ( T i^i R ) -> ( ( p e. NN /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
90		eqeq2 2633	. . . . . . . 8 |- ( m = p -> ( ( ( 2 ^ n ) x. t ) = m <-> ( ( 2 ^ n ) x. t ) = p ) )
91	90	2rexbidv 3057	. . . . . . 7 |- ( m = p -> ( E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m <-> E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
92	91	elrab 3363	. . . . . 6 |- ( p e. { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> ( p e. NN /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
93	92	a1i 11	. . . . 5 |- ( A e. ( T i^i R ) -> ( p e. { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> ( p e. NN /\ E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
94	6	imaeq2i 5464	. . . . . . . . 9 |- ( F " U ) = ( F " U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) ) )
95		imaiun 6503	. . . . . . . . 9 |- ( F " U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. (bits ` ( A ` t ) ) ) ) = U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. (bits ` ( A ` t ) ) ) )
96	94, 95	eqtri 2644	. . . . . . . 8 |- ( F " U ) = U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. (bits ` ( A ` t ) ) ) )
97	96	eleq2i 2693	. . . . . . 7 |- ( p e. ( F " U ) <-> p e. U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) )
98		eliun 4524	. . . . . . 7 |- ( p e. U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. t e. ( ( `' A " NN ) i^i J ) p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) )
99		f1ofn 6138	. . . . . . . . . . . . 13 |- ( F : ( J X. NN0 ) -1-1-onto-> NN -> F Fn ( J X. NN0 ) )
100	3, 99	ax-mp 5	. . . . . . . . . . . 12 |- F Fn ( J X. NN0 )
101		snssi 4339	. . . . . . . . . . . . 13 |- ( t e. J -> { t } C_ J )
102	101, 11, 12	sylancl 694	. . . . . . . . . . . 12 |- ( t e. J -> ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
103		ovelimab 6812	. . . . . . . . . . . 12 |- ( ( F Fn ( J X. NN0 ) /\ ( { t } X. (bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) -> ( p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. x e. { t } E. n e. (bits ` ( A ` t ) ) p = ( x F n ) ) )
104	100, 102, 103	sylancr 695	. . . . . . . . . . 11 |- ( t e. J -> ( p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. x e. { t } E. n e. (bits ` ( A ` t ) ) p = ( x F n ) ) )
105		vex 3203	. . . . . . . . . . . 12 |- t e. _V
106		oveq1 6657	. . . . . . . . . . . . . 14 |- ( x = t -> ( x F n ) = ( t F n ) )
107	106	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( x = t -> ( p = ( x F n ) <-> p = ( t F n ) ) )
108	107	rexbidv 3052	. . . . . . . . . . . 12 |- ( x = t -> ( E. n e. (bits ` ( A ` t ) ) p = ( x F n ) <-> E. n e. (bits ` ( A ` t ) ) p = ( t F n ) ) )
109	105, 108	rexsn 4223	. . . . . . . . . . 11 |- ( E. x e. { t } E. n e. (bits ` ( A ` t ) ) p = ( x F n ) <-> E. n e. (bits ` ( A ` t ) ) p = ( t F n ) )
110	104, 109	syl6bb 276	. . . . . . . . . 10 |- ( t e. J -> ( p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. n e. (bits ` ( A ` t ) ) p = ( t F n ) ) )
111		df-ov 6653	. . . . . . . . . . . . . . 15 |- ( t F n ) = ( F ` <. t , n >. )
112	111	eqeq1i 2627	. . . . . . . . . . . . . 14 |- ( ( t F n ) = p <-> ( F ` <. t , n >. ) = p )
113		eqcom 2629	. . . . . . . . . . . . . 14 |- ( ( t F n ) = p <-> p = ( t F n ) )
114	112, 113	bitr3i 266	. . . . . . . . . . . . 13 |- ( ( F ` <. t , n >. ) = p <-> p = ( t F n ) )
115		opelxpi 5148	. . . . . . . . . . . . . . 15 |- ( ( t e. J /\ n e. NN0 ) -> <. t , n >. e. ( J X. NN0 ) )
116	1, 2	oddpwdcv 30417	. . . . . . . . . . . . . . . 16 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
117		vex 3203	. . . . . . . . . . . . . . . . . . 19 |- n e. _V
118	105, 117	op2nd 7177	. . . . . . . . . . . . . . . . . 18 |- ( 2nd ` <. t , n >. ) = n
119	118	oveq2i 6661	. . . . . . . . . . . . . . . . 17 |- ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
120	105, 117	op1st 7176	. . . . . . . . . . . . . . . . 17 |- ( 1st ` <. t , n >. ) = t
121	119, 120	oveq12i 6662	. . . . . . . . . . . . . . . 16 |- ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
122	116, 121	syl6eq 2672	. . . . . . . . . . . . . . 15 |- ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
123	115, 122	syl 17	. . . . . . . . . . . . . 14 |- ( ( t e. J /\ n e. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
124	123	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( ( t e. J /\ n e. NN0 ) -> ( ( F ` <. t , n >. ) = p <-> ( ( 2 ^ n ) x. t ) = p ) )
125	114, 124	syl5bbr 274	. . . . . . . . . . . 12 |- ( ( t e. J /\ n e. NN0 ) -> ( p = ( t F n ) <-> ( ( 2 ^ n ) x. t ) = p ) )
126	21, 125	sylan2 491	. . . . . . . . . . 11 |- ( ( t e. J /\ n e. (bits ` ( A ` t ) ) ) -> ( p = ( t F n ) <-> ( ( 2 ^ n ) x. t ) = p ) )
127	126	rexbidva 3049	. . . . . . . . . 10 |- ( t e. J -> ( E. n e. (bits ` ( A ` t ) ) p = ( t F n ) <-> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
128	110, 127	bitrd 268	. . . . . . . . 9 |- ( t e. J -> ( p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
129	9, 128	syl 17	. . . . . . . 8 |- ( t e. ( ( `' A " NN ) i^i J ) -> ( p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
130	129	rexbiia 3040	. . . . . . 7 |- ( E. t e. ( ( `' A " NN ) i^i J ) p e. ( F " ( { t } X. (bits ` ( A ` t ) ) ) ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
131	97, 98, 130	3bitri 286	. . . . . 6 |- ( p e. ( F " U ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
132	131	a1i 11	. . . . 5 |- ( A e. ( T i^i R ) -> ( p e. ( F " U ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
133	89, 93, 132	3bitr4rd 301	. . . 4 |- ( A e. ( T i^i R ) -> ( p e. ( F " U ) <-> p e. { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
134	133	eqrdv 2620	. . 3 |- ( A e. ( T i^i R ) -> ( F " U ) = { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )
135		f1oeq3 6129	. . 3 |- ( ( F " U ) = { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( ( F |` U ) : U -1-1-onto-> ( F " U ) <-> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
136	134, 135	syl 17	. 2 |- ( A e. ( T i^i R ) -> ( ( F |` U ) : U -1-1-onto-> ( F " U ) <-> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
137	17, 136	mpbii 223	1 |- ( A e. ( T i^i R ) -> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. (bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   {copab 4712   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   |` cres 5116   "cima 5117   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   1stc1st 7166   2ndc2nd 7167   supp csupp 7295   ^m cmap 7857   Fincfn 7955   0cc0 9936   1c1 9937   x. cmul 9941   <_ cle 10075   NNcn 11020   2c2 11070   NN0cn0 11292   ^cexp 12860   sum_csu 14416   || cdvds 14983  bitscbits 15141  𝟭cind 30072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-dvds 14984  df-bits 15144

This theorem is referenced by:  eulerpartlemgs2  30442