Theorem oddpwdc 26742

Description: Lemma for eulerpart 26770. 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 10484	. . . . . . . 8 |- 2 e. NN
3	2	a1i 11	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> 2 e. NN )
4		simpl 457	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> y e. NN0 )
5	3, 4	nnexpcld 12034	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> ( 2 ^ y ) e. NN )
6		oddpwdc.j	. . . . . . . 8 |- J = { z e. NN | -. 2 || z }
7		ssrab2 3442	. . . . . . . 8 |- { z e. NN | -. 2 || z } C_ NN
8	6, 7	eqsstri 3391	. . . . . . 7 |- J C_ NN
9		simpr 461	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> x e. J )
10	8, 9	sseldi 3359	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> x e. NN )
11	5, 10	nnmulcld 10374	. . . . 5 |- ( ( y e. NN0 /\ x e. J ) -> ( ( 2 ^ y ) x. x ) e. NN )
12	11	ancoms 453	. . . 4 |- ( ( x e. J /\ y e. NN0 ) -> ( ( 2 ^ y ) x. x ) e. NN )
13	12	adantl 466	. . 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 10588	. . . . . . . . . . 11 |- NN0 C_ RR
17		ltso 9460	. . . . . . . . . . 11 |- < Or RR
18		soss 4664	. . . . . . . . . . 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 10663	. . . . . . . . . 10 |- ( a e. NN -> 0 e. ZZ )
22		ssrab2 3442	. . . . . . . . . . 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 10673	. . . . . . . . . . 11 |- ( a e. NN -> a e. ZZ )
25		oveq2 6104	. . . . . . . . . . . . . . 15 |- ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
26	25	breq1d 4307	. . . . . . . . . . . . . 14 |- ( k = n -> ( ( 2 ^ k ) || a <-> ( 2 ^ n ) || a ) )
27	26	elrab 3122	. . . . . . . . . . . . 13 |- ( n e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( n e. NN0 /\ ( 2 ^ n ) || a ) )
28		simprl 755	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. NN0 )
29	28	nn0red 10642	. . . . . . . . . . . . . 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 12034	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. NN )
32	31	nnred 10342	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. RR )
33		simpl 457	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. NN )
34	33	nnred 10342	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. RR )
35		2re 10396	. . . . . . . . . . . . . . . 16 |- 2 e. RR
36	35	leidi 9879	. . . . . . . . . . . . . . . 16 |- 2 <_ 2
37		nexple 26453	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN0 /\ 2 e. RR /\ 2 <_ 2 ) -> n <_ ( 2 ^ n ) )
38	35, 36, 37	mp3an23 1306	. . . . . . . . . . . . . . 15 |- ( n e. NN0 -> n <_ ( 2 ^ n ) )
39	38	ad2antrl 727	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ ( 2 ^ n ) )
40	31	nnzd 10751	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. ZZ )
41		simprr 756	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) || a )
42		dvdsle 13583	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) -> ( ( 2 ^ n ) || a -> ( 2 ^ n ) <_ a ) )
43	42	imp 429	. . . . . . . . . . . . . . 15 |- ( ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) /\ ( 2 ^ n ) || a ) -> ( 2 ^ n ) <_ a )
44	40, 33, 41, 43	syl21anc 1217	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) <_ a )
45	29, 32, 34, 39, 44	letrd 9533	. . . . . . . . . . . . 13 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ a )
46	27, 45	sylan2b 475	. . . . . . . . . . . 12 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n <_ a )
47	46	ralrimiva 2804	. . . . . . . . . . 11 |- ( a e. NN -> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a )
48		breq2 4301	. . . . . . . . . . . . 13 |- ( m = a -> ( n <_ m <-> n <_ a ) )
49	48	ralbidv 2740	. . . . . . . . . . . 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 3078	. . . . . . . . . . 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 661	. . . . . . . . . 10 |- ( a e. NN -> E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m )
52		nn0uz 10900	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
53	52	uzsupss 10952	. . . . . . . . . 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 1218	. . . . . . . . 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 7713	. . . . . . . 8 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
56	15, 55	nnexpcld 12034	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN )
57		fzfi 11799	. . . . . . . . . . . 12 |- ( 0 ... a ) e. Fin
58		0zd 10663	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 e. ZZ )
59	24	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> a e. ZZ )
60	27, 28	sylan2b 475	. . . . . . . . . . . . . . . 16 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. NN0 )
61	60	nn0zd 10750	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ZZ )
62	60	nn0ge0d 10644	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 <_ n )
63		elfz4 11451	. . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ( 0 ... a ) )
65	64	ex 434	. . . . . . . . . . . . 13 |- ( a e. NN -> ( n e. { k e. NN0 | ( 2 ^ k ) || a } -> n e. ( 0 ... a ) ) )
66	65	ssrdv 3367	. . . . . . . . . . . 12 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) )
67		ssfi 7538	. . . . . . . . . . . 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 663	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
69		0nn0 10599	. . . . . . . . . . . . . 14 |- 0 e. NN0
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( a e. NN -> 0 e. NN0 )
71		2cn 10397	. . . . . . . . . . . . . . 15 |- 2 e. CC
72		exp0 11874	. . . . . . . . . . . . . . 15 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
73	71, 72	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 2 ^ 0 ) = 1
74		1dvds 13552	. . . . . . . . . . . . . . 15 |- ( a e. ZZ -> 1 || a )
75	24, 74	syl 16	. . . . . . . . . . . . . 14 |- ( a e. NN -> 1 || a )
76	73, 75	syl5eqbr 4330	. . . . . . . . . . . . 13 |- ( a e. NN -> ( 2 ^ 0 ) || a )
77		oveq2 6104	. . . . . . . . . . . . . . 15 |- ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
78	77	breq1d 4307	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( ( 2 ^ k ) || a <-> ( 2 ^ 0 ) || a ) )
79	78	elrab 3122	. . . . . . . . . . . . 13 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( 0 e. NN0 /\ ( 2 ^ 0 ) || a ) )
80	70, 76, 79	sylanbrc 664	. . . . . . . . . . . 12 |- ( a e. NN -> 0 e. { k e. NN0 | ( 2 ^ k ) || a } )
81		ne0i 3648	. . . . . . . . . . . 12 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
82	80, 81	syl 16	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
83		fisupcl 7722	. . . . . . . . . . 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 1220	. . . . . . . . . 10 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
85		oveq2 6104	. . . . . . . . . . . 12 |- ( k = l -> ( 2 ^ k ) = ( 2 ^ l ) )
86	85	breq1d 4307	. . . . . . . . . . 11 |- ( k = l -> ( ( 2 ^ k ) || a <-> ( 2 ^ l ) || a ) )
87	86	cbvrabv 2976	. . . . . . . . . 10 |- { k e. NN0 | ( 2 ^ k ) || a } = { l e. NN0 | ( 2 ^ l ) || a }
88	84, 87	syl6eleq 2533	. . . . . . . . 9 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } )
89		oveq2 6104	. . . . . . . . . . 11 |- ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( 2 ^ l ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
90	89	breq1d 4307	. . . . . . . . . 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 3122	. . . . . . . . 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 196	. . . . . . . 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 463	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a )
94		nndivdvds 13546	. . . . . . . 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 484	. . . . . . 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 1217	. . . . . 6 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
97		1nn0 10600	. . . . . . . . . . 11 |- 1 e. NN0
98	97	a1i 11	. . . . . . . . . 10 |- ( a e. NN -> 1 e. NN0 )
99	55, 98	nn0addcld 10645	. . . . . . . . 9 |- ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 )
100	55	nn0red 10642	. . . . . . . . . . . . . 14 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
101	100	ltp1d 10268	. . . . . . . . . . . . 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 7714	. . . . . . . . . . . . 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 117	. . . . . . . . . . . 12 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } )
104	87	eleq2i 2507	. . . . . . . . . . . 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 304	. . . . . . . . . . 11 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } )
106		oveq2 6104	. . . . . . . . . . . . 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 4307	. . . . . . . . . . . 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 3122	. . . . . . . . . . 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 304	. . . . . . . . . 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 422	. . . . . . . . . 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 212	. . . . . . . . 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 11877	. . . . . . . . . 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 663	. . . . . . . . 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 4307	. . . . . . . 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 300	. . . . . . 7 |- ( a e. NN -> -. ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a )
117		nncn 10335	. . . . . . . . . . 11 |- ( a e. NN -> a e. CC )
118	56	nncnd 10343	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
119	56	nnne0d 10371	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
120	117, 118, 119	divcan2d 10114	. . . . . . . . . 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 2448	. . . . . . . . 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 4309	. . . . . . . 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 10751	. . . . . . . . 9 |- ( a e. NN -> 2 e. ZZ )
124	96	nnzd 10751	. . . . . . . . 9 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
125	56	nnzd 10751	. . . . . . . . 9 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ )
126		dvdscmulr 13566	. . . . . . . . 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 1222	. . . . . . . 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 253	. . . . . . 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 300	. . . . . 6 |- ( a e. NN -> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
130		breq2 4301	. . . . . . . 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 294	. . . . . . 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 3124	. . . . . 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 664	. . . . 5 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J )
134	133, 55	jca 532	. . . 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 466	. . 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 461	. . . . . . 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 754	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. NN0 )
139	137, 138	nnexpcld 12034	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. NN )
140	8	sseli 3357	. . . . . . . . 9 |- ( x e. J -> x e. NN )
141	140	ad2antrr 725	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. NN )
142	139, 141	nnmulcld 10374	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
143	136, 142	eqeltrd 2517	. . . . . 6 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. NN )
144		simplll 757	. . . . . . . . . 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 4301	. . . . . . . . . . . . . 14 |- ( z = x -> ( 2 || z <-> 2 || x ) )
146	145	notbid 294	. . . . . . . . . . . . 13 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
147	146, 6	elrab2 3124	. . . . . . . . . . . 12 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
148	147	simprbi 464	. . . . . . . . . . 11 |- ( x e. J -> -. 2 || x )
149		2z 10683	. . . . . . . . . . . . . 14 |- 2 e. ZZ
150	138	adantr 465	. . . . . . . . . . . . . . . 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 10750	. . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 7713	. . . . . . . . . . . . . . . 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 10750	. . . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . 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 10696	. . . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 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 1217	. . . . . . . . . . . . . 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 13561	. . . . . . . . . . . . . 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 663	. . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . 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 10641	. . . . . . . . . . . . . . 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 11885	. . . . . . . . . . . . . . 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 663	. . . . . . . . . . . . . 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 13573	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . 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 10343	. . . . . . . . . . . . . 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 10399	. . . . . . . . . . . . . . . 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 12013	. . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . 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 10343	. . . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . 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 10419	. . . . . . . . . . . . . . . . . 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 12019	. . . . . . . . . . . . . . . 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 10112	. . . . . . . . . . . . . . 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 9411	. . . . . . . . . . . . . 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 12013	. . . . . . . . . . . . . 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 12019	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . . . 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 754	. . . . . . . . . . . . . . . 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 10643	. . . . . . . . . . . . . . . . . . . 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 10643	. . . . . . . . . . . . . . . . . . . 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 9727	. . . . . . . . . . . . . . . . . . 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 6112	. . . . . . . . . . . . . . . . . 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 12015	. . . . . . . . . . . . . . . . . 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 2477	. . . . . . . . . . . . . . . . 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 6111	. . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . . 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 9414	. . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . 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 9976	. . . . . . . . . . . . 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 9412	. . . . . . . . . . . . 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 2478	. . . . . . . . . . . 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 4323	. . . . . . . . . . 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 119	. . . . . . . . . 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 576	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
204	141	nnzd 10751	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. ZZ )
205	139	nnzd 10751	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. ZZ )
206	143	nnzd 10751	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. ZZ )
207	139	nncnd 10343	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. CC )
208	141	nncnd 10343	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. CC )
209	207, 208	mulcomd 9412	. . . . . . . . . . . . 13 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) = ( x x. ( 2 ^ y ) ) )
210	136, 209	eqtr2d 2476	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x x. ( 2 ^ y ) ) = a )
211		dvds0lem 13548	. . . . . . . . . . . 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 1221	. . . . . . . . . . 11 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) || a )
213		oveq2 6104	. . . . . . . . . . . . 13 |- ( k = y -> ( 2 ^ k ) = ( 2 ^ y ) )
214	213	breq1d 4307	. . . . . . . . . . . 12 |- ( k = y -> ( ( 2 ^ k ) || a <-> ( 2 ^ y ) || a ) )
215	214	elrab 3122	. . . . . . . . . . 11 |- ( y e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( y e. NN0 /\ ( 2 ^ y ) || a ) )
216	138, 212, 215	sylanbrc 664	. . . . . . . . . 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 7714	. . . . . . . . . 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 10642	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. RR )
221	143, 100	syl 16	. . . . . . . . . 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 9519	. . . . . . . . 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 913	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
224		simplr 754	. . . . . . . . . . 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 465	. . . . . . . . . . . . 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 10343	. . . . . . . . . . . 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 465	. . . . . . . . . . . . 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 10343	. . . . . . . . . . . 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 11883	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. NN /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
230	2, 229	mpan 670	. . . . . . . . . . . . . . 15 |- ( y e. NN0 -> ( 2 ^ y ) e. NN )
231	230	nncnd 10343	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) e. CC )
232	230	nnne0d 10371	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
233	231, 232	jca 532	. . . . . . . . . . . . 13 |- ( y e. NN0 -> ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) )
234	233	ad3antlr 730	. . . . . . . . . . . 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 10003	. . . . . . . . . . . 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 1218	. . . . . . . . . . 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 232	. . . . . . . . . 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 461	. . . . . . . . . . . 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 6112	. . . . . . . . . . 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 6112	. . . . . . . . . 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 2477	. . . . . . . . 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 434	. . . . . . . 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 536	. . . . . . 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 451	. . . . . 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 532	. . . . 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 755	. . . . . . 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 465	. . . . . . 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 2517	. . . . . 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 756	. . . . . . 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 465	. . . . . . 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 2517	. . . . . 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 465	. . . . . . 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 6112	. . . . . . . 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 6114	. . . . . . 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 2478	. . . . . 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 534	. . . . 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 188	. . . 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 26029	. 2 |- ( T. -> F : ( J X. NN0 ) -1-1-onto-> NN )
260	259	trud 1378	1 |- F : ( J X. NN0 ) -1-1-onto-> NN

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   T. wtru 1370   e. wcel 1756   =/= wne 2611   A.wral 2720   E.wrex 2721   {crab 2724   C_ wss 3333   (/)c0 3642   class class class wbr 4297   Or wor 4645   X. cxp 4843   -1-1-onto->wf1o 5422  (class class class)co 6096   e. cmpt2 6098   Fincfn 7315   supcsup 7695   CCcc 9285   RRcr 9286   0cc0 9287   1c1 9288   + caddc 9290   x. cmul 9292   < clt 9423   <_ cle 9424   - cmin 9600   / cdiv 9998   NNcn 10327   2c2 10376   NN0cn0 10584   ZZcz 10651   ...cfz 11442   ^cexp 11870   || cdivides 13540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-cnex 9343  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363  ax-pre-mulgt0 9364

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-om 6482  df-1st 6582  df-2nd 6583  df-recs 6837  df-rdg 6871  df-1o 6925  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-fin 7319  df-sup 7696  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-sub 9602  df-neg 9603  df-div 9999  df-nn 10328  df-2 10385  df-n0 10585  df-z 10652  df-uz 10867  df-fz 11443  df-seq 11812  df-exp 11871  df-dvds 13541

This theorem is referenced by:  eulerpartgbij  26760  eulerpartlemgvv  26764  eulerpartlemgh  26766  eulerpartlemgf  26767