Theorem oddpwdc 29260

Description: Lemma for eulerpart 29288. 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 10790	. . . . . . . 8 |- 2 e. NN
3	2	a1i 11	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> 2 e. NN )
4		simpl 464	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> y e. NN0 )
5	3, 4	nnexpcld 12475	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> ( 2 ^ y ) e. NN )
6		oddpwdc.j	. . . . . . . 8 |- J = { z e. NN | -. 2 || z }
7		ssrab2 3500	. . . . . . . 8 |- { z e. NN | -. 2 || z } C_ NN
8	6, 7	eqsstri 3448	. . . . . . 7 |- J C_ NN
9		simpr 468	. . . . . . 7 |- ( ( y e. NN0 /\ x e. J ) -> x e. J )
10	8, 9	sseldi 3416	. . . . . 6 |- ( ( y e. NN0 /\ x e. J ) -> x e. NN )
11	5, 10	nnmulcld 10679	. . . . 5 |- ( ( y e. NN0 /\ x e. J ) -> ( ( 2 ^ y ) x. x ) e. NN )
12	11	ancoms 460	. . . 4 |- ( ( x e. J /\ y e. NN0 ) -> ( ( 2 ^ y ) x. x ) e. NN )
13	12	adantl 473	. . 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 10897	. . . . . . . . . . 11 |- NN0 C_ RR
17		ltso 9732	. . . . . . . . . . 11 |- < Or RR
18		soss 4778	. . . . . . . . . . 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 10973	. . . . . . . . . 10 |- ( a e. NN -> 0 e. ZZ )
22		ssrab2 3500	. . . . . . . . . . 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 10983	. . . . . . . . . . 11 |- ( a e. NN -> a e. ZZ )
25		oveq2 6316	. . . . . . . . . . . . . . 15 |- ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
26	25	breq1d 4405	. . . . . . . . . . . . . 14 |- ( k = n -> ( ( 2 ^ k ) || a <-> ( 2 ^ n ) || a ) )
27	26	elrab 3184	. . . . . . . . . . . . 13 |- ( n e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( n e. NN0 /\ ( 2 ^ n ) || a ) )
28		simprl 772	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. NN0 )
29	28	nn0red 10950	. . . . . . . . . . . . . 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 12475	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. NN )
32	31	nnred 10646	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. RR )
33		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. NN )
34	33	nnred 10646	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. RR )
35		2re 10701	. . . . . . . . . . . . . . . 16 |- 2 e. RR
36	35	leidi 10169	. . . . . . . . . . . . . . . 16 |- 2 <_ 2
37		nexple 28905	. . . . . . . . . . . . . . . 16 |- ( ( n e. NN0 /\ 2 e. RR /\ 2 <_ 2 ) -> n <_ ( 2 ^ n ) )
38	35, 36, 37	mp3an23 1382	. . . . . . . . . . . . . . 15 |- ( n e. NN0 -> n <_ ( 2 ^ n ) )
39	38	ad2antrl 742	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ ( 2 ^ n ) )
40	31	nnzd 11062	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. ZZ )
41		simprr 774	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) || a )
42		dvdsle 14427	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) -> ( ( 2 ^ n ) || a -> ( 2 ^ n ) <_ a ) )
43	42	imp 436	. . . . . . . . . . . . . . 15 |- ( ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) /\ ( 2 ^ n ) || a ) -> ( 2 ^ n ) <_ a )
44	40, 33, 41, 43	syl21anc 1291	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) <_ a )
45	29, 32, 34, 39, 44	letrd 9809	. . . . . . . . . . . . 13 |- ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ a )
46	27, 45	sylan2b 483	. . . . . . . . . . . 12 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n <_ a )
47	46	ralrimiva 2809	. . . . . . . . . . 11 |- ( a e. NN -> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a )
48		breq2 4399	. . . . . . . . . . . . 13 |- ( m = a -> ( n <_ m <-> n <_ a ) )
49	48	ralbidv 2829	. . . . . . . . . . . 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 3136	. . . . . . . . . . 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 673	. . . . . . . . . 10 |- ( a e. NN -> E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m )
52		nn0uz 11217	. . . . . . . . . . 11 |- NN0 = ( ZZ>= ` 0 )
53	52	uzsupss 11279	. . . . . . . . . 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 1292	. . . . . . . . 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 7990	. . . . . . . 8 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
56	15, 55	nnexpcld 12475	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN )
57		fzfi 12223	. . . . . . . . . . . 12 |- ( 0 ... a ) e. Fin
58		0zd 10973	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 e. ZZ )
59	24	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> a e. ZZ )
60	27, 28	sylan2b 483	. . . . . . . . . . . . . . . 16 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. NN0 )
61	60	nn0zd 11061	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ZZ )
62	60	nn0ge0d 10952	. . . . . . . . . . . . . . 15 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 <_ n )
63		elfz4 11819	. . . . . . . . . . . . . . 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 1300	. . . . . . . . . . . . . 14 |- ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ( 0 ... a ) )
65	64	ex 441	. . . . . . . . . . . . 13 |- ( a e. NN -> ( n e. { k e. NN0 | ( 2 ^ k ) || a } -> n e. ( 0 ... a ) ) )
66	65	ssrdv 3424	. . . . . . . . . . . 12 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) )
67		ssfi 7810	. . . . . . . . . . . 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 676	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
69		0nn0 10908	. . . . . . . . . . . . . 14 |- 0 e. NN0
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( a e. NN -> 0 e. NN0 )
71		2cn 10702	. . . . . . . . . . . . . . 15 |- 2 e. CC
72		exp0 12314	. . . . . . . . . . . . . . 15 |- ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
73	71, 72	ax-mp 5	. . . . . . . . . . . . . 14 |- ( 2 ^ 0 ) = 1
74		1dvds 14394	. . . . . . . . . . . . . . 15 |- ( a e. ZZ -> 1 || a )
75	24, 74	syl 17	. . . . . . . . . . . . . 14 |- ( a e. NN -> 1 || a )
76	73, 75	syl5eqbr 4429	. . . . . . . . . . . . 13 |- ( a e. NN -> ( 2 ^ 0 ) || a )
77		oveq2 6316	. . . . . . . . . . . . . . 15 |- ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
78	77	breq1d 4405	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( ( 2 ^ k ) || a <-> ( 2 ^ 0 ) || a ) )
79	78	elrab 3184	. . . . . . . . . . . . 13 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( 0 e. NN0 /\ ( 2 ^ 0 ) || a ) )
80	70, 76, 79	sylanbrc 677	. . . . . . . . . . . 12 |- ( a e. NN -> 0 e. { k e. NN0 | ( 2 ^ k ) || a } )
81		ne0i 3728	. . . . . . . . . . . 12 |- ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
82	80, 81	syl 17	. . . . . . . . . . 11 |- ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
83		fisupcl 8003	. . . . . . . . . . 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 1294	. . . . . . . . . 10 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
85		oveq2 6316	. . . . . . . . . . . 12 |- ( k = l -> ( 2 ^ k ) = ( 2 ^ l ) )
86	85	breq1d 4405	. . . . . . . . . . 11 |- ( k = l -> ( ( 2 ^ k ) || a <-> ( 2 ^ l ) || a ) )
87	86	cbvrabv 3030	. . . . . . . . . 10 |- { k e. NN0 | ( 2 ^ k ) || a } = { l e. NN0 | ( 2 ^ l ) || a }
88	84, 87	syl6eleq 2559	. . . . . . . . 9 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } )
89		oveq2 6316	. . . . . . . . . . 11 |- ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( 2 ^ l ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
90	89	breq1d 4405	. . . . . . . . . 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 3184	. . . . . . . . 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 201	. . . . . . . 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 470	. . . . . . 7 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a )
94		nndivdvds 14388	. . . . . . . 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 492	. . . . . . 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 1291	. . . . . 6 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
97		1nn0 10909	. . . . . . . . . . 11 |- 1 e. NN0
98	97	a1i 11	. . . . . . . . . 10 |- ( a e. NN -> 1 e. NN0 )
99	55, 98	nn0addcld 10953	. . . . . . . . 9 |- ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 )
100	55	nn0red 10950	. . . . . . . . . . . . . 14 |- ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
101	100	ltp1d 10559	. . . . . . . . . . . . 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 7991	. . . . . . . . . . . . 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 121	. . . . . . . . . . . 12 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } )
104	87	eleq2i 2541	. . . . . . . . . . . 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 311	. . . . . . . . . . 11 |- ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } )
106		oveq2 6316	. . . . . . . . . . . . 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 4405	. . . . . . . . . . . 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 3184	. . . . . . . . . . 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 311	. . . . . . . . . 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 429	. . . . . . . . . 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 217	. . . . . . . . 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 12317	. . . . . . . . . 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 676	. . . . . . . . 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 4405	. . . . . . . 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 307	. . . . . . 7 |- ( a e. NN -> -. ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a )
117		nncn 10639	. . . . . . . . . . 11 |- ( a e. NN -> a e. CC )
118	56	nncnd 10647	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
119	56	nnne0d 10676	. . . . . . . . . . 11 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
120	117, 118, 119	divcan2d 10407	. . . . . . . . . 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 2477	. . . . . . . . 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 4407	. . . . . . . 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 11062	. . . . . . . . 9 |- ( a e. NN -> 2 e. ZZ )
124	96	nnzd 11062	. . . . . . . . 9 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
125	56	nnzd 11062	. . . . . . . . 9 |- ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ )
126		dvdscmulr 14408	. . . . . . . . 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 1296	. . . . . . . 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 261	. . . . . . 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 307	. . . . . 6 |- ( a e. NN -> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
130		breq2 4399	. . . . . . . 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 301	. . . . . . 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 3186	. . . . . 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 677	. . . . 5 |- ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J )
134	133, 55	jca 541	. . . 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 473	. . 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 468	. . . . . . 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 770	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. NN0 )
139	137, 138	nnexpcld 12475	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. NN )
140	8	sseli 3414	. . . . . . . . 9 |- ( x e. J -> x e. NN )
141	140	ad2antrr 740	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. NN )
142	139, 141	nnmulcld 10679	. . . . . . 7 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
143	136, 142	eqeltrd 2549	. . . . . 6 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. NN )
144		simplll 776	. . . . . . . . . 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 4399	. . . . . . . . . . . . . 14 |- ( z = x -> ( 2 || z <-> 2 || x ) )
146	145	notbid 301	. . . . . . . . . . . . 13 |- ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
147	146, 6	elrab2 3186	. . . . . . . . . . . 12 |- ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
148	147	simprbi 471	. . . . . . . . . . 11 |- ( x e. J -> -. 2 || x )
149		2z 10993	. . . . . . . . . . . . . 14 |- 2 e. ZZ
150	138	adantr 472	. . . . . . . . . . . . . . . 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 11061	. . . . . . . . . . . . . . 15 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. ZZ )
152	19	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> < Or NN0 )
153	143, 54	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> E. m e. NN0 ( A. n e. { k e. NN0 | ( 2 ^ k ) || a } -. m < n /\ A. n e. NN0 ( n < m -> E. o e. { k e. NN0 | ( 2 ^ k ) || a } n < o ) ) )
154	153	adantr 472	. . . . . . . . . . . . . . . . 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 7990	. . . . . . . . . . . . . . . 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 11061	. . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . 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 11007	. . . . . . . . . . . . . . . 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 492	. . . . . . . . . . . . . . 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 1291	. . . . . . . . . . . . . 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 14403	. . . . . . . . . . . . . 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 676	. . . . . . . . . . . . 13 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 || ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) - y ) ) )
163	149	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 e. ZZ )
164	143, 124	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
165	164	adantr 472	. . . . . . . . . . . . . 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 10949	. . . . . . . . . . . . . . 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 12325	. . . . . . . . . . . . . . 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 676	. . . . . . . . . . . . . 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 14417	. . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . 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 10647	. . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . 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 12454	. . . . . . . . . . . . . . 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 472	. . . . . . . . . . . . . . . . 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 10647	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. CC )
178	176, 118	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
179		2ne0 10724	. . . . . . . . . . . . . . . . . 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 12460	. . . . . . . . . . . . . . . 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 10405	. . . . . . . . . . . . . . 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 9681	. . . . . . . . . . . . . 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 12454	. . . . . . . . . . . . . 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 12460	. . . . . . . . . . . . . 14 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) =/= 0 )
186	176, 121	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
187		simplr 770	. . . . . . . . . . . . . . . 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 10951	. . . . . . . . . . . . . . . . . . . 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 10951	. . . . . . . . . . . . . . . . . . . 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 10008	. . . . . . . . . . . . . . . . . . 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 6324	. . . . . . . . . . . . . . . . . 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 12456	. . . . . . . . . . . . . . . . . 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 2507	. . . . . . . . . . . . . . . . 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 6323	. . . . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . . . 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 9684	. . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . 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 10269	. . . . . . . . . . . . 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 9682	. . . . . . . . . . . . 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 2508	. . . . . . . . . . . 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 4422	. . . . . . . . . . 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 123	. . . . . . . . . 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 586	. . . . . . . . 9 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
204	141	nnzd 11062	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. ZZ )
205	139	nnzd 11062	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. ZZ )
206	143	nnzd 11062	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. ZZ )
207	139	nncnd 10647	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. CC )
208	141	nncnd 10647	. . . . . . . . . . . . . 14 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. CC )
209	207, 208	mulcomd 9682	. . . . . . . . . . . . 13 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) = ( x x. ( 2 ^ y ) ) )
210	136, 209	eqtr2d 2506	. . . . . . . . . . . 12 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x x. ( 2 ^ y ) ) = a )
211		dvds0lem 14390	. . . . . . . . . . . 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 1295	. . . . . . . . . . 11 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) || a )
213		oveq2 6316	. . . . . . . . . . . . 13 |- ( k = y -> ( 2 ^ k ) = ( 2 ^ y ) )
214	213	breq1d 4405	. . . . . . . . . . . 12 |- ( k = y -> ( ( 2 ^ k ) || a <-> ( 2 ^ y ) || a ) )
215	214	elrab 3184	. . . . . . . . . . 11 |- ( y e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( y e. NN0 /\ ( 2 ^ y ) || a ) )
216	138, 212, 215	sylanbrc 677	. . . . . . . . . 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 7991	. . . . . . . . . 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 10950	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. RR )
221	143, 100	syl 17	. . . . . . . . . 10 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
222	220, 221	lttri3d 9792	. . . . . . . . 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 936	. . . . . . . 8 |- ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
224		simplr 770	. . . . . . . . . . 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 472	. . . . . . . . . . . . 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 10647	. . . . . . . . . . . 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 472	. . . . . . . . . . . . 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 10647	. . . . . . . . . . . 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 12323	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. NN /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
230	2, 229	mpan 684	. . . . . . . . . . . . . . 15 |- ( y e. NN0 -> ( 2 ^ y ) e. NN )
231	230	nncnd 10647	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) e. CC )
232	230	nnne0d 10676	. . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
233	231, 232	jca 541	. . . . . . . . . . . . 13 |- ( y e. NN0 -> ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) )
234	233	ad3antlr 745	. . . . . . . . . . . 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 10296	. . . . . . . . . . . 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 1292	. . . . . . . . . . 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 240	. . . . . . . . . 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 468	. . . . . . . . . . . 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 6324	. . . . . . . . . . 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 6324	. . . . . . . . . 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 2507	. . . . . . . . 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 441	. . . . . . . 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 545	. . . . . . 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 458	. . . . . 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 541	. . . . 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 772	. . . . . . 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 472	. . . . . . 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 2549	. . . . . 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 774	. . . . . . 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 472	. . . . . . 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 2549	. . . . . 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 472	. . . . . . 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 6324	. . . . . . . 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 6326	. . . . . . 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 2508	. . . . . 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 543	. . . . 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 192	. . . 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 28384	. 2 |- ( T. -> F : ( J X. NN0 ) -1-1-onto-> NN )
260	259	trud 1461	1 |- F : ( J X. NN0 ) -1-1-onto-> NN

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   T. wtru 1453   e. wcel 1904   =/= wne 2641   A.wral 2756   E.wrex 2757   {crab 2760   C_ wss 3390   (/)c0 3722   class class class wbr 4395   Or wor 4759   X. cxp 4837   -1-1-onto->wf1o 5588  (class class class)co 6308   |-> cmpt2 6310   Fincfn 7587   supcsup 7972   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   x. cmul 9562   < clt 9693   <_ cle 9694   - cmin 9880   / cdiv 10291   NNcn 10631   2c2 10681   NN0cn0 10893   ZZcz 10961   ...cfz 11810   ^cexp 12310   || cdvds 14382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-n0 10894  df-z 10962  df-uz 11183  df-fz 11811  df-seq 12252  df-exp 12311  df-dvds 14383

This theorem is referenced by:  eulerpartgbij  29278  eulerpartlemgvv  29282  eulerpartlemgh  29284  eulerpartlemgf  29285