Theorem oddpwdc 27933

Description: Lemma for eulerpart 27961. 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 10689	. . . . . . . 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 12295	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> ( 2 ^ y ) e. NN )
6		oddpwdc.j	. . . . . . . 8 |- J = { z e. NN | -. 2 || z }
7		ssrab2 3585	. . . . . . . 8 |- { z e. NN | -. 2 || z } C_ NN
8	6, 7	eqsstri 3534	. . . . . . 7 |- J C_ NN
9		simpr 461	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> x e. J )
10	8, 9	sseldi 3502	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> x e. NN )
11	5, 10	nnmulcld 10579	. . . . 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 10795	. . . . . . . . . . 11 |- NN0 C_ RR
17		ltso 9661	. . . . . . . . . . 11 |- < Or RR
18		soss 4818	. . . . . . . . . . 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 10872	. . . . . . . . . 10 |- ( a e. NN -> 0 e. ZZ )
22		ssrab2 3585	. . . . . . . . . . 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 10882	. . . . . . . . . . 11 |- ( a e. NN -> a e. ZZ )
25		oveq2 6290	. . . . . . . . . . . . . . 15 |- ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
26	25	breq1d 4457	. . . . . . . . . . . . . 14 |- ( k = n -> ( ( 2 ^ k ) || a <-> ( 2 ^ n ) || a ) )
27	26	elrab 3261	. . . . . . . . . . . . 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 10849	. . . . . . . . . . . . . 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 12295	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. NN )
32	31	nnred 10547	. . . . . . . . . . . . . 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 10547	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. RR )
35		2re 10601	. . . . . . . . . . . . . . . 16 |- 2 e. RR
36	35	leidi 10083	. . . . . . . . . . . . . . . 16 |- 2 <_ 2
37		nexple 27645	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN0 /\ 2 e. RR /\ 2 <_ 2 ) -> n <_ ( 2 ^ n ) )
38	35, 36, 37	mp3an23 1316	. . . . . . . . . . . . . . 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 10961	. . . . . . . . . . . . . . 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 13886	. . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) <_ a )
45	29, 32, 34, 39, 44	letrd 9734	. . . . . . . . . . . . 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 2878	. . . . . . . . . . 11 |- ( a e. NN -> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a )
48		breq2 4451	. . . . . . . . . . . . 13 |- ( m = a -> ( n <_ m <-> n <_ a ) )
49	48	ralbidv 2903	. . . . . . . . . . . 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 3214	. . . . . . . . . . 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 11112	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
53	52	uzsupss 11170	. . . . . . . . . 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 1228	. . . . . . . . 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 7914	. . . . . . . 8 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
56	15, 55	nnexpcld 12295	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN )
57		fzfi 12046	. . . . . . . . . . . 12 |- ( 0 ... a ) e. Fin
58		0zd 10872	. . . . . . . . . . . . . . 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 10960	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ZZ )
62	60	nn0ge0d 10851	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 <_ n )
63		elfz4 11677	. . . . . . . . . . . . . . 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 1236	. . . . . . . . . . . . . 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 3510	. . . . . . . . . . . 12 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) )
67		ssfi 7737	. . . . . . . . . . . 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 10806	. . . . . . . . . . . . . 14 |- 0 e. NN0
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( a e. NN -> 0 e. NN0 )
71		2cn 10602	. . . . . . . . . . . . . . 15 |- 2 e. CC
72		exp0 12134	. . . . . . . . . . . . . . 15 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
73	71, 72	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 2 ^ 0 ) = 1
74		1dvds 13855	. . . . . . . . . . . . . . 15 |- ( a e. ZZ -> 1 || a )
75	24, 74	syl 16	. . . . . . . . . . . . . 14 |- ( a e. NN -> 1 || a )
76	73, 75	syl5eqbr 4480	. . . . . . . . . . . . 13 |- ( a e. NN -> ( 2 ^ 0 ) || a )
77		oveq2 6290	. . . . . . . . . . . . . . 15 |- ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
78	77	breq1d 4457	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( ( 2 ^ k ) || a <-> ( 2 ^ 0 ) || a ) )
79	78	elrab 3261	. . . . . . . . . . . . 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 3791	. . . . . . . . . . . 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 7923	. . . . . . . . . . 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 1230	. . . . . . . . . 10 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
85		oveq2 6290	. . . . . . . . . . . 12 |- ( k = l -> ( 2 ^ k ) = ( 2 ^ l ) )
86	85	breq1d 4457	. . . . . . . . . . 11 |- ( k = l -> ( ( 2 ^ k ) || a <-> ( 2 ^ l ) || a ) )
87	86	cbvrabv 3112	. . . . . . . . . 10 |- { k e. NN0 | ( 2 ^ k ) || a } = { l e. NN0 | ( 2 ^ l ) || a }
88	84, 87	syl6eleq 2565	. . . . . . . . 9 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } )
89		oveq2 6290	. . . . . . . . . . 11 |- ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( 2 ^ l ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
90	89	breq1d 4457	. . . . . . . . . 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 3261	. . . . . . . . 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 13849	. . . . . . . 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 1227	. . . . . 6 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
97		1nn0 10807	. . . . . . . . . . 11 |- 1 e. NN0
98	97	a1i 11	. . . . . . . . . 10 |- ( a e. NN -> 1 e. NN0 )
99	55, 98	nn0addcld 10852	. . . . . . . . 9 |- ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 )
100	55	nn0red 10849	. . . . . . . . . . . . . 14 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
101	100	ltp1d 10472	. . . . . . . . . . . . 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 7915	. . . . . . . . . . . . 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 2545	. . . . . . . . . . . 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 6290	. . . . . . . . . . . . 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 4457	. . . . . . . . . . . 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 3261	. . . . . . . . . . 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 12137	. . . . . . . . . 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 4457	. . . . . . . 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 10540	. . . . . . . . . . 11 |- ( a e. NN -> a e. CC )
118	56	nncnd 10548	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
119	56	nnne0d 10576	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
120	117, 118, 119	divcan2d 10318	. . . . . . . . . 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 2475	. . . . . . . . 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 4459	. . . . . . . 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 10961	. . . . . . . . 9 |- ( a e. NN -> 2 e. ZZ )
124	96	nnzd 10961	. . . . . . . . 9 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
125	56	nnzd 10961	. . . . . . . . 9 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ )
126		dvdscmulr 13869	. . . . . . . . 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 1232	. . . . . . . 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 4451	. . . . . . . 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 3263	. . . . . 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 12295	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. NN )
140	8	sseli 3500	. . . . . . . . 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 10579	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
143	136, 142	eqeltrd 2555	. . . . . 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 4451	. . . . . . . . . . . . . 14 |- ( z = x -> ( 2 || z <-> 2 || x ) )
146	145	notbid 294	. . . . . . . . . . . . 13 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
147	146, 6	elrab2 3263	. . . . . . . . . . . 12 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
148	147	simprbi 464	. . . . . . . . . . 11 |- ( x e. J -> -. 2 || x )
149		2z 10892	. . . . . . . . . . . . . 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 10960	. . . . . . . . . . . . . . 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 7914	. . . . . . . . . . . . . . . 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 10960	. . . . . . . . . . . . . . 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 10905	. . . . . . . . . . . . . . . 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 1227	. . . . . . . . . . . . . 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 13864	. . . . . . . . . . . . . 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 10848	. . . . . . . . . . . . . . 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 12145	. . . . . . . . . . . . . . 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 13876	. . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . 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 10548	. . . . . . . . . . . . . 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 10604	. . . . . . . . . . . . . . . 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 12274	. . . . . . . . . . . . . . 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 10548	. . . . . . . . . . . . . . . 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 10624	. . . . . . . . . . . . . . . . . 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 12280	. . . . . . . . . . . . . . . 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 10316	. . . . . . . . . . . . . . 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 9612	. . . . . . . . . . . . . 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 12274	. . . . . . . . . . . . . 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 12280	. . . . . . . . . . . . . 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 10850	. . . . . . . . . . . . . . . . . . . 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 10850	. . . . . . . . . . . . . . . . . . . 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 9929	. . . . . . . . . . . . . . . . . . 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 6298	. . . . . . . . . . . . . . . . . 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 12276	. . . . . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . . . . 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 6297	. . . . . . . . . . . . . . . 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 2516	. . . . . . . . . . . . . . 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 9615	. . . . . . . . . . . . . . 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 2508	. . . . . . . . . . . . . 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 10180	. . . . . . . . . . . . 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 9613	. . . . . . . . . . . . 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 2511	. . . . . . . . . . . 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 4473	. . . . . . . . . . 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 10961	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. ZZ )
205	139	nnzd 10961	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. ZZ )
206	143	nnzd 10961	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. ZZ )
207	139	nncnd 10548	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. CC )
208	141	nncnd 10548	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. CC )
209	207, 208	mulcomd 9613	. . . . . . . . . . . . 13 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) = ( x x. ( 2 ^ y ) ) )
210	136, 209	eqtr2d 2509	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x x. ( 2 ^ y ) ) = a )
211		dvds0lem 13851	. . . . . . . . . . . 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 1231	. . . . . . . . . . 11 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) || a )
213		oveq2 6290	. . . . . . . . . . . . 13 |- ( k = y -> ( 2 ^ k ) = ( 2 ^ y ) )
214	213	breq1d 4457	. . . . . . . . . . . 12 |- ( k = y -> ( ( 2 ^ k ) || a <-> ( 2 ^ y ) || a ) )
215	214	elrab 3261	. . . . . . . . . . 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 7915	. . . . . . . . . 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 10849	. . . . . . . . . 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 9720	. . . . . . . . 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 920	. . . . . . . 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 10548	. . . . . . . . . . . 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 10548	. . . . . . . . . . . 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 12143	. . . . . . . . . . . . . . . 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 10548	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) e. CC )
232	230	nnne0d 10576	. . . . . . . . . . . . . 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 10207	. . . . . . . . . . . 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 1228	. . . . . . . . . . 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 6298	. . . . . . . . . . 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 6298	. . . . . . . . . 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 2510	. . . . . . . . 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 2555	. . . . . 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 2555	. . . . . 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 6298	. . . . . . . 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 6300	. . . . . . 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 2511	. . . . . 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 27219	. 2 |- ( T. -> F : ( J X. NN0 ) -1-1-onto-> NN )
260	259	trud 1388	1 |- F : ( J X. NN0 ) -1-1-onto-> NN

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   T. wtru 1380   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   {crab 2818   C_ wss 3476   (/)c0 3785   class class class wbr 4447   Or wor 4799   X. cxp 4997   -1-1-onto->wf1o 5585  (class class class)co 6282   |-> cmpt2 6284   Fincfn 7513   supcsup 7896   CCcc 9486   RRcr 9487   0cc0 9488   1c1 9489   + caddc 9491   x. cmul 9493   < clt 9624   <_ cle 9625   - cmin 9801   / cdiv 10202   NNcn 10532   2c2 10581   NN0cn0 10791   ZZcz 10860   ...cfz 11668   ^cexp 12130   || cdivides 13843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-sup 7897  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-n0 10792  df-z 10861  df-uz 11079  df-fz 11669  df-seq 12072  df-exp 12131  df-dvds 13844

This theorem is referenced by:  eulerpartgbij  27951  eulerpartlemgvv  27955  eulerpartlemgh  27957  eulerpartlemgf  27958