Theorem oddpwdc 30416

Description: Lemma for eulerpart 30444. The function F that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)

Hypotheses

Ref	Expression
oddpwdc.j	|- J = { z e. NN | -. 2 || z }
oddpwdc.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )

Assertion

Ref	Expression
oddpwdc	|- F : ( J X. NN0 ) -1-1-onto-> NN

Distinct variable groups:   x, y, z   x, J, y

Allowed substitution hints:   F( x, y, z)   J( z)

Proof of Theorem oddpwdc

Dummy variables k a l m n o are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oddpwdc.f	. . 3 |- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
2		2nn 11185	. . . . . . . 8 |- 2 e. NN
3	2	a1i 11	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> 2 e. NN )
4		simpl 473	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> y e. NN0 )
5	3, 4	nnexpcld 13030	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> ( 2 ^ y ) e. NN )
6		oddpwdc.j	. . . . . . . 8 |- J = { z e. NN | -. 2 || z }
7		ssrab2 3687	. . . . . . . 8 |- { z e. NN | -. 2 || z } C_ NN
8	6, 7	eqsstri 3635	. . . . . . 7 |- J C_ NN
9		simpr 477	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> x e. J )
10	8, 9	sseldi 3601	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> x e. NN )
11	5, 10	nnmulcld 11068	. . . . 5 |- ( ( y e. NN0 /\ x e. J ) -> ( ( 2 ^ y ) x. x ) e. NN )
12	11	ancoms 469	. . . 4 |- ( ( x e. J /\ y e. NN0 ) -> ( ( 2 ^ y ) x. x ) e. NN )
13	12	adantl 482	. . 3 |- ( ( T. /\ ( x e. J /\ y e. NN0 ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
14		id 22	. . . . . . 7 |- ( a e. NN -> a e. NN )
15	2	a1i 11	. . . . . . . 8 |- ( a e. NN -> 2 e. NN )
16		nn0ssre 11296	. . . . . . . . . . 11 |- NN0 C_ RR
17		ltso 10118	. . . . . . . . . . 11 |- < Or RR
18		soss 5053	. . . . . . . . . . 11 |- ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
19	16, 17, 18	mp2 9	. . . . . . . . . 10 |- < Or NN0
20	19	a1i 11	. . . . . . . . 9 |- ( a e. NN -> < Or NN0 )
21		0zd 11389	. . . . . . . . . 10 |- ( a e. NN -> 0 e. ZZ )
22		ssrab2 3687	. . . . . . . . . . 11 |- { k e. NN0 | ( 2 ^ k ) || a } C_ NN0
23	22	a1i 11	. . . . . . . . . 10 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ NN0 )
24		nnz 11399	. . . . . . . . . . 11 |- ( a e. NN -> a e. ZZ )
25		oveq2 6658	. . . . . . . . . . . . . . 15 |- ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
26	25	breq1d 4663	. . . . . . . . . . . . . 14 |- ( k = n -> ( ( 2 ^ k ) || a <-> ( 2 ^ n ) || a ) )
27	26	elrab 3363	. . . . . . . . . . . . 13 |- ( n e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( n e. NN0 /\ ( 2 ^ n ) || a ) )
28		simprl 794	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. NN0 )
29	28	nn0red 11352	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. RR )
30	2	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> 2 e. NN )
31	30, 28	nnexpcld 13030	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. NN )
32	31	nnred 11035	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. RR )
33		simpl 473	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. NN )
34	33	nnred 11035	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. RR )
35		2re 11090	. . . . . . . . . . . . . . . 16 |- 2 e. RR
36	35	leidi 10562	. . . . . . . . . . . . . . . 16 |- 2 <_ 2
37		nexple 30071	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN0 /\ 2 e. RR /\ 2 <_ 2 ) -> n <_ ( 2 ^ n ) )
38	35, 36, 37	mp3an23 1416	. . . . . . . . . . . . . . 15 |- ( n e. NN0 -> n <_ ( 2 ^ n ) )
39	38	ad2antrl 764	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ ( 2 ^ n ) )
40	31	nnzd 11481	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. ZZ )
41		simprr 796	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) || a )
42		dvdsle 15032	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) -> ( ( 2 ^ n ) || a -> ( 2 ^ n ) <_ a ) )
43	42	imp 445	. . . . . . . . . . . . . . 15 |- ( ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) /\ ( 2 ^ n ) || a ) -> ( 2 ^ n ) <_ a )
44	40, 33, 41, 43	syl21anc 1325	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) <_ a )
45	29, 32, 34, 39, 44	letrd 10194	. . . . . . . . . . . . 13 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ a )
46	27, 45	sylan2b 492	. . . . . . . . . . . 12 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n <_ a )
47	46	ralrimiva 2966	. . . . . . . . . . 11 |- ( a e. NN -> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a )
48		breq2 4657	. . . . . . . . . . . . 13 |- ( m = a -> ( n <_ m <-> n <_ a ) )
49	48	ralbidv 2986	. . . . . . . . . . . 12 |- ( m = a -> ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m <-> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a ) )
50	49	rspcev 3309	. . . . . . . . . . 11 |- ( ( a e. ZZ /\ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a ) -> E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m )
51	24, 47, 50	syl2anc 693	. . . . . . . . . 10 |- ( a e. NN -> E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m )
52		nn0uz 11722	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
53	52	uzsupss 11780	. . . . . . . . . 10 |- ( ( 0 e. ZZ /\ { k e. NN0 | ( 2 ^ k ) || a } C_ NN0 /\ E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m ) -> E. m e. NN0 ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } -. m < n /\ A. n e. NN0 ( n < m -> E. o e. { k e. NN0 | ( 2 ^ k ) || a } n < o ) ) )
54	21, 23, 51, 53	syl3anc 1326	. . . . . . . . 9 |- ( a e. NN -> E. m e. NN0 ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } -. m < n /\ A. n e. NN0 ( n < m -> E. o e. { k e. NN0 | ( 2 ^ k ) || a } n < o ) ) )
55	20, 54	supcl 8364	. . . . . . . 8 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
56	15, 55	nnexpcld 13030	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN )
57		fzfi 12771	. . . . . . . . . . . 12 |- ( 0 ... a ) e. Fin
58		0zd 11389	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 e. ZZ )
59	24	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> a e. ZZ )
60	27, 28	sylan2b 492	. . . . . . . . . . . . . . . 16 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. NN0 )
61	60	nn0zd 11480	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ZZ )
62	60	nn0ge0d 11354	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 <_ n )
63		elfz4 12335	. . . . . . . . . . . . . . 15 |- ( ( ( 0 e. ZZ /\ a e. ZZ /\ n e. ZZ ) /\ ( 0 <_ n /\ n <_ a ) ) -> n e. ( 0 ... a ) )
64	58, 59, 61, 62, 46, 63	syl32anc 1334	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ( 0 ... a ) )
65	64	ex 450	. . . . . . . . . . . . 13 |- ( a e. NN -> ( n e. { k e. NN0 | ( 2 ^ k ) || a } -> n e. ( 0 ... a ) ) )
66	65	ssrdv 3609	. . . . . . . . . . . 12 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) )
67		ssfi 8180	. . . . . . . . . . . 12 |- ( ( ( 0 ... a ) e. Fin /\ { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) ) -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
68	57, 66, 67	sylancr 695	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
69		0nn0 11307	. . . . . . . . . . . . . 14 |- 0 e. NN0
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( a e. NN -> 0 e. NN0 )
71		2cn 11091	. . . . . . . . . . . . . . 15 |- 2 e. CC
72		exp0 12864	. . . . . . . . . . . . . . 15 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
73	71, 72	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 2 ^ 0 ) = 1
74		1dvds 14996	. . . . . . . . . . . . . . 15 |- ( a e. ZZ -> 1 || a )
75	24, 74	syl 17	. . . . . . . . . . . . . 14 |- ( a e. NN -> 1 || a )
76	73, 75	syl5eqbr 4688	. . . . . . . . . . . . 13 |- ( a e. NN -> ( 2 ^ 0 ) || a )
77		oveq2 6658	. . . . . . . . . . . . . . 15 |- ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
78	77	breq1d 4663	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( ( 2 ^ k ) || a <-> ( 2 ^ 0 ) || a ) )
79	78	elrab 3363	. . . . . . . . . . . . 13 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( 0 e. NN0 /\ ( 2 ^ 0 ) || a ) )
80	70, 76, 79	sylanbrc 698	. . . . . . . . . . . 12 |- ( a e. NN -> 0 e. { k e. NN0 | ( 2 ^ k ) || a } )
81		ne0i 3921	. . . . . . . . . . . 12 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
82	80, 81	syl 17	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
83		fisupcl 8375	. . . . . . . . . . 11 |- ( ( < Or NN0 /\ ( { k e. NN0 | ( 2 ^ k ) || a } e. Fin /\ { k e. NN0 | ( 2 ^ k ) || a } =/= (/) /\ { k e. NN0 | ( 2 ^ k ) || a } C_ NN0 ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
84	20, 68, 82, 23, 83	syl13anc 1328	. . . . . . . . . 10 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
85		oveq2 6658	. . . . . . . . . . . 12 |- ( k = l -> ( 2 ^ k ) = ( 2 ^ l ) )
86	85	breq1d 4663	. . . . . . . . . . 11 |- ( k = l -> ( ( 2 ^ k ) || a <-> ( 2 ^ l ) || a ) )
87	86	cbvrabv 3199	. . . . . . . . . 10 |- { k e. NN0 | ( 2 ^ k ) || a } = { l e. NN0 | ( 2 ^ l ) || a }
88	84, 87	syl6eleq 2711	. . . . . . . . 9 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } )
89		oveq2 6658	. . . . . . . . . . 11 |- ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( 2 ^ l ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
90	89	breq1d 4663	. . . . . . . . . 10 |- ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( ( 2 ^ l ) || a <-> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) )
91	90	elrab 3363	. . . . . . . . 9 |- ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } <-> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) )
92	88, 91	sylib 208	. . . . . . . 8 |- ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) )
93	92	simprd 479	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a )
94		nndivdvds 14989	. . . . . . . 8 |- ( ( a e. NN /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN ) -> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a <-> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN ) )
95	94	biimpa 501	. . . . . . 7 |- ( ( ( a e. NN /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN ) /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
96	14, 56, 93, 95	syl21anc 1325	. . . . . 6 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
97		1nn0 11308	. . . . . . . . . . 11 |- 1 e. NN0
98	97	a1i 11	. . . . . . . . . 10 |- ( a e. NN -> 1 e. NN0 )
99	55, 98	nn0addcld 11355	. . . . . . . . 9 |- ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 )
100	55	nn0red 11352	. . . . . . . . . . . . . 14 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
101	100	ltp1d 10954	. . . . . . . . . . . . 13 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) )
102	20, 54	supub 8365	. . . . . . . . . . . . 13 |- ( a e. NN -> ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } -> -. sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) )
103	101, 102	mt2d 131	. . . . . . . . . . . 12 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } )
104	87	eleq2i 2693	. . . . . . . . . . . 12 |- ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } )
105	103, 104	sylnib 318	. . . . . . . . . . 11 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } )
106		oveq2 6658	. . . . . . . . . . . . 13 |- ( l = ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) -> ( 2 ^ l ) = ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) )
107	106	breq1d 4663	. . . . . . . . . . . 12 |- ( l = ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) -> ( ( 2 ^ l ) || a <-> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
108	107	elrab 3363	. . . . . . . . . . 11 |- ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } <-> ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 /\ ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
109	105, 108	sylnib 318	. . . . . . . . . 10 |- ( a e. NN -> -. ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 /\ ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
110		imnan 438	. . . . . . . . . 10 |- ( ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 -> -. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) <-> -. ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 /\ ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
111	109, 110	sylibr 224	. . . . . . . . 9 |- ( a e. NN -> ( ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 -> -. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
112	99, 111	mpd 15	. . . . . . . 8 |- ( a e. NN -> -. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a )
113		expp1 12867	. . . . . . . . . 10 |- ( ( 2 e. CC /\ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 ) -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) )
114	71, 55, 113	sylancr 695	. . . . . . . . 9 |- ( a e. NN -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) )
115	114	breq1d 4663	. . . . . . . 8 |- ( a e. NN -> ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a <-> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a ) )
116	112, 115	mtbid 314	. . . . . . 7 |- ( a e. NN -> -. ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a )
117		nncn 11028	. . . . . . . . . . 11 |- ( a e. NN -> a e. CC )
118	56	nncnd 11036	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
119	56	nnne0d 11065	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
120	117, 118, 119	divcan2d 10803	. . . . . . . . . 10 |- ( a e. NN -> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) = a )
121	120	eqcomd 2628	. . . . . . . . 9 |- ( a e. NN -> a = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
122	121	breq2d 4665	. . . . . . . 8 |- ( a e. NN -> ( ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a <-> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) ) )
123	15	nnzd 11481	. . . . . . . . 9 |- ( a e. NN -> 2 e. ZZ )
124	96	nnzd 11481	. . . . . . . . 9 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
125	56	nnzd 11481	. . . . . . . . 9 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ )
126		dvdscmulr 15010	. . . . . . . . 9 |- ( ( 2 e. ZZ /\ ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ /\ ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 ) ) -> ( ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) <-> 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
127	123, 124, 125, 119, 126	syl112anc 1330	. . . . . . . 8 |- ( a e. NN -> ( ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) <-> 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
128	122, 127	bitrd 268	. . . . . . 7 |- ( a e. NN -> ( ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a <-> 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
129	116, 128	mtbid 314	. . . . . 6 |- ( a e. NN -> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
130		breq2 4657	. . . . . . . 8 |- ( z = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( 2 || z <-> 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
131	130	notbid 308	. . . . . . 7 |- ( z = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( -. 2 || z <-> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
132	131, 6	elrab2 3366	. . . . . 6 |- ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J <-> ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN /\ -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
133	96, 129, 132	sylanbrc 698	. . . . 5 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J )
134	133, 55	jca 554	. . . 4 |- ( a e. NN -> ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J /\ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 ) )
135	134	adantl 482	. . 3 |- ( ( T. /\ a e. NN ) -> ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J /\ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 ) )
136		simpr 477	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a = ( ( 2 ^ y ) x. x ) )
137	2	a1i 11	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> 2 e. NN )
138		simplr 792	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. NN0 )
139	137, 138	nnexpcld 13030	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. NN )
140	8	sseli 3599	. . . . . . . . 9 |- ( x e. J -> x e. NN )
141	140	ad2antrr 762	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. NN )
142	139, 141	nnmulcld 11068	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
143	136, 142	eqeltrd 2701	. . . . . 6 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. NN )
144		simplll 798	. . . . . . . . . 10 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. J )
145		breq2 4657	. . . . . . . . . . . . . 14 |- ( z = x -> ( 2 || z <-> 2 || x ) )
146	145	notbid 308	. . . . . . . . . . . . 13 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
147	146, 6	elrab2 3366	. . . . . . . . . . . 12 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
148	147	simprbi 480	. . . . . . . . . . 11 |- ( x e. J -> -. 2 || x )
149		2z 11409	. . . . . . . . . . . . . 14 |- 2 e. ZZ
150	138	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. NN0 )
151	150	nn0zd 11480	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. ZZ )
152	19	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> < Or NN0 )
153	143, 54	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> E. m e. NN0 ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } -. m < n /\ A. n e. NN0 ( n < m -> E. o e. { k e. NN0 | ( 2 ^ k ) || a } n < o ) ) )
154	153	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> E. m e. NN0 ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } -. m < n /\ A. n e. NN0 ( n < m -> E. o e. { k e. NN0 | ( 2 ^ k ) || a } n < o ) ) )
155	152, 154	supcl 8364	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
156	155	nn0zd 11480	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. ZZ )
157		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
158		znnsub 11423	. . . . . . . . . . . . . . . 16 |- ( ( y e. ZZ /\ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. ZZ ) -> ( y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) <-> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN ) )
159	158	biimpa 501	. . . . . . . . . . . . . . 15 |- ( ( ( y e. ZZ /\ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. ZZ ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN )
160	151, 156, 157, 159	syl21anc 1325	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN )
161		iddvdsexp 15005	. . . . . . . . . . . . . 14 |- ( ( 2 e. ZZ /\ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN ) -> 2 || ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) )
162	149, 160, 161	sylancr 695	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 || ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) )
163	149	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 e. ZZ )
164	143, 124	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
165	164	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
166	160	nnnn0d 11351	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN0 )
167		zexpcl 12875	. . . . . . . . . . . . . . 15 |- ( ( 2 e. ZZ /\ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) e. NN0 ) -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) e. ZZ )
168	149, 166, 167	sylancr 695	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) e. ZZ )
169		dvdsmultr2 15021	. . . . . . . . . . . . . 14 |- ( ( 2 e. ZZ /\ ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ /\ ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) e. ZZ ) -> ( 2 || ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) -> 2 || ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) ) )
170	163, 165, 168, 169	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 || ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) -> 2 || ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) ) )
171	162, 170	mpd 15	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 || ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) )
172	141	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. NN )
173	172	nncnd 11036	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. CC )
174		2cnd 11093	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 e. CC )
175	174, 166	expcld 13008	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) e. CC )
176	143	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. NN )
177	176	nncnd 11036	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. CC )
178	176, 118	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
179		2ne0 11113	. . . . . . . . . . . . . . . . . 18 |- 2 =/= 0
180	179	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 =/= 0 )
181	174, 180, 156	expne0d 13014	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
182	177, 178, 181	divcld 10801	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. CC )
183	175, 182	mulcld 10060	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) e. CC )
184	174, 150	expcld 13008	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) e. CC )
185	174, 180, 151	expne0d 13014	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) =/= 0 )
186	176, 121	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
187		simplr 792	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a = ( ( 2 ^ y ) x. x ) )
188	150	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. CC )
189	155	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. CC )
190	188, 189	pncan3d 10395	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( y + ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
191	190	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ ( y + ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
192	174, 166, 150	expaddd 13010	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ ( y + ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) = ( ( 2 ^ y ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) )
193	191, 192	eqtr3d 2658	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) = ( ( 2 ^ y ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) )
194	193	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) = ( ( ( 2 ^ y ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
195	186, 187, 194	3eqtr3d 2664	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( 2 ^ y ) x. x ) = ( ( ( 2 ^ y ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
196	184, 175, 182	mulassd 10063	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( ( 2 ^ y ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) = ( ( 2 ^ y ) x. ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) ) )
197	195, 196	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( 2 ^ y ) x. x ) = ( ( 2 ^ y ) x. ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) ) )
198	173, 183, 184, 185, 197	mulcanad 10662	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x = ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
199	182, 175	mulcomd 10061	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) = ( ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
200	198, 199	eqtr4d 2659	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x = ( ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) x. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) ) )
201	171, 200	breqtrrd 4681	. . . . . . . . . . 11 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 || x )
202	148, 201	nsyl3 133	. . . . . . . . . 10 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> -. x e. J )
203	144, 202	pm2.65da 600	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
204	141	nnzd 11481	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. ZZ )
205	139	nnzd 11481	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. ZZ )
206	143	nnzd 11481	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. ZZ )
207	139	nncnd 11036	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. CC )
208	141	nncnd 11036	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. CC )
209	207, 208	mulcomd 10061	. . . . . . . . . . . . 13 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) = ( x x. ( 2 ^ y ) ) )
210	136, 209	eqtr2d 2657	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x x. ( 2 ^ y ) ) = a )
211		dvds0lem 14992	. . . . . . . . . . . 12 |- ( ( ( x e. ZZ /\ ( 2 ^ y ) e. ZZ /\ a e. ZZ ) /\ ( x x. ( 2 ^ y ) ) = a ) -> ( 2 ^ y ) || a )
212	204, 205, 206, 210, 211	syl31anc 1329	. . . . . . . . . . 11 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) || a )
213		oveq2 6658	. . . . . . . . . . . . 13 |- ( k = y -> ( 2 ^ k ) = ( 2 ^ y ) )
214	213	breq1d 4663	. . . . . . . . . . . 12 |- ( k = y -> ( ( 2 ^ k ) || a <-> ( 2 ^ y ) || a ) )
215	214	elrab 3363	. . . . . . . . . . 11 |- ( y e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( y e. NN0 /\ ( 2 ^ y ) || a ) )
216	138, 212, 215	sylanbrc 698	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. { k e. NN0 | ( 2 ^ k ) || a } )
217	19	a1i 11	. . . . . . . . . . 11 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> < Or NN0 )
218	217, 153	supub 8365	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( y e. { k e. NN0 | ( 2 ^ k ) || a } -> -. sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < y ) )
219	216, 218	mpd 15	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < y )
220	138	nn0red 11352	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. RR )
221	143, 100	syl 17	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
222	220, 221	lttri3d 10177	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) <-> ( -. y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) /\ -. sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < y ) ) )
223	203, 219, 222	mpbir2and 957	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
224		simplr 792	. . . . . . . . . . 11 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a = ( ( 2 ^ y ) x. x ) )
225	143	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. NN )
226	225	nncnd 11036	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. CC )
227	141	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. NN )
228	227	nncnd 11036	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. CC )
229		nnexpcl 12873	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. NN /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
230	2, 229	mpan 706	. . . . . . . . . . . . . . 15 |- ( y e. NN0 -> ( 2 ^ y ) e. NN )
231	230	nncnd 11036	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) e. CC )
232	230	nnne0d 11065	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
233	231, 232	jca 554	. . . . . . . . . . . . 13 |- ( y e. NN0 -> ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) )
234	233	ad3antlr 767	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) )
235		divmul2 10689	. . . . . . . . . . . 12 |- ( ( a e. CC /\ x e. CC /\ ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) ) -> ( ( a / ( 2 ^ y ) ) = x <-> a = ( ( 2 ^ y ) x. x ) ) )
236	226, 228, 234, 235	syl3anc 1326	. . . . . . . . . . 11 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( ( a / ( 2 ^ y ) ) = x <-> a = ( ( 2 ^ y ) x. x ) ) )
237	224, 236	mpbird 247	. . . . . . . . . 10 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( a / ( 2 ^ y ) ) = x )
238		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
239	238	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
240	239	oveq2d 6666	. . . . . . . . . 10 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( a / ( 2 ^ y ) ) = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
241	237, 240	eqtr3d 2658	. . . . . . . . 9 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
242	241	ex 450	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
243	223, 242	jcai 559	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) /\ x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
244	243	ancomd 467	. . . . . 6 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
245	143, 244	jca 554	. . . . 5 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
246		simprl 794	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
247	133	adantr 481	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J )
248	246, 247	eqeltrd 2701	. . . . . 6 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> x e. J )
249		simprr 796	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
250	55	adantr 481	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
251	249, 250	eqeltrd 2701	. . . . . 6 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> y e. NN0 )
252	121	adantr 481	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> a = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
253	249	oveq2d 6666	. . . . . . . 8 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( 2 ^ y ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
254	253, 246	oveq12d 6668	. . . . . . 7 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( ( 2 ^ y ) x. x ) = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
255	252, 254	eqtr4d 2659	. . . . . 6 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> a = ( ( 2 ^ y ) x. x ) )
256	248, 251, 255	jca31 557	. . . . 5 |- ( ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) )
257	245, 256	impbii 199	. . . 4 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) <-> ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
258	257	a1i 11	. . 3 |- ( T. -> ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) <-> ( a e. NN /\ ( x = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
259	1, 13, 135, 258	f1od2 29499	. 2 |- ( T. -> F : ( J X. NN0 ) -1-1-onto-> NN )
260	259	trud 1493	1 |- F : ( J X. NN0 ) -1-1-onto-> NN

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   T. wtru 1484   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   C_ wss 3574   (/)c0 3915   class class class wbr 4653   Or wor 5034   X. cxp 5112   -1-1-onto->wf1o 5887  (class class class)co 6650   |-> cmpt2 6652   Fincfn 7955   supcsup 8346   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ...cfz 12326   ^cexp 12860   || cdvds 14983

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

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-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-fz 12327  df-seq 12802  df-exp 12861  df-dvds 14984

This theorem is referenced by:  eulerpartgbij  30434  eulerpartlemgvv  30438  eulerpartlemgh  30440  eulerpartlemgf  30441