Metamath Proof Explorer

Theorem oddpwdc

Description: Lemma for eulerpart . 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)

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

Proof

Step Hyp Ref Expression
1 oddpwdc.j 
 |-  J = { z e. NN | -. 2 || z }
2 oddpwdc.f 
 |-  F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
3 2nn 
 |-  2 e. NN
4 3 a1i 
 |-  ( ( y e. NN0 /\ x e. J ) -> 2 e. NN )
5 simpl 
 |-  ( ( y e. NN0 /\ x e. J ) -> y e. NN0 )
6 4 5 nnexpcld 
 |-  ( ( y e. NN0 /\ x e. J ) -> ( 2 ^ y ) e. NN )
7 ssrab2 
 |-  { z e. NN | -. 2 || z } C_ NN
8 1 7 eqsstri 
 |-  J C_ NN
9 simpr 
 |-  ( ( y e. NN0 /\ x e. J ) -> x e. J )
10 8 9 sseldi 
 |-  ( ( y e. NN0 /\ x e. J ) -> x e. NN )
11 6 10 nnmulcld 
 |-  ( ( y e. NN0 /\ x e. J ) -> ( ( 2 ^ y ) x. x ) e. NN )
12 11 ancoms 
 |-  ( ( x e. J /\ y e. NN0 ) -> ( ( 2 ^ y ) x. x ) e. NN )
13 12 adantl 
 |-  ( ( T. /\ ( x e. J /\ y e. NN0 ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
14 id 
 |-  ( a e. NN -> a e. NN )
15 3 a1i 
 |-  ( a e. NN -> 2 e. NN )
16 nn0ssre 
 |-  NN0 C_ RR
17 ltso 
 |-  < Or RR
18 soss 
 |-  ( NN0 C_ RR -> ( < Or RR -> < Or NN0 ) )
19 16 17 18 mp2 
 |-  < Or NN0
20 19 a1i 
 |-  ( a e. NN -> < Or NN0 )
21 0zd 
 |-  ( a e. NN -> 0 e. ZZ )
22 ssrab2 
 |-  { k e. NN0 | ( 2 ^ k ) || a } C_ NN0
23 22 a1i 
 |-  ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ NN0 )
24 nnz 
 |-  ( a e. NN -> a e. ZZ )
25 oveq2 
 |-  ( k = n -> ( 2 ^ k ) = ( 2 ^ n ) )
26 25 breq1d 
 |-  ( k = n -> ( ( 2 ^ k ) || a <-> ( 2 ^ n ) || a ) )
27 26 elrab 
 |-  ( n e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( n e. NN0 /\ ( 2 ^ n ) || a ) )
28 simprl 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. NN0 )
29 28 nn0red 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n e. RR )
30 3 a1i 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> 2 e. NN )
31 30 28 nnexpcld 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. NN )
32 31 nnred 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. RR )
33 simpl 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. NN )
34 33 nnred 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> a e. RR )
35 2re 
 |-  2 e. RR
36 35 leidi 
 |-  2 <_ 2
37 nexple 
 |-  ( ( n e. NN0 /\ 2 e. RR /\ 2 <_ 2 ) -> n <_ ( 2 ^ n ) )
38 35 36 37 mp3an23 
 |-  ( n e. NN0 -> n <_ ( 2 ^ n ) )
39 38 ad2antrl 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ ( 2 ^ n ) )
40 31 nnzd 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) e. ZZ )
41 simprr 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) || a )
42 dvdsle 
 |-  ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) -> ( ( 2 ^ n ) || a -> ( 2 ^ n ) <_ a ) )
43 42 imp 
 |-  ( ( ( ( 2 ^ n ) e. ZZ /\ a e. NN ) /\ ( 2 ^ n ) || a ) -> ( 2 ^ n ) <_ a )
44 40 33 41 43 syl21anc 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> ( 2 ^ n ) <_ a )
45 29 32 34 39 44 letrd 
 |-  ( ( a e. NN /\ ( n e. NN0 /\ ( 2 ^ n ) || a ) ) -> n <_ a )
46 27 45 sylan2b 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n <_ a )
47 46 ralrimiva 
 |-  ( a e. NN -> A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ a )
48 brralrspcev 
 |-  ( ( 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 )
49 24 47 48 syl2anc 
 |-  ( a e. NN -> E. m e. ZZ A. n e. { k e. NN0 | ( 2 ^ k ) || a } n <_ m )
50 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
51 50 uzsupss 
 |-  ( ( 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 ) ) )
52 21 23 49 51 syl3anc 
 |-  ( 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 ) ) )
53 20 52 supcl 
 |-  ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 )
54 15 53 nnexpcld 
 |-  ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. NN )
55 fzfi 
 |-  ( 0 ... a ) e. Fin
56 0zd 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 e. ZZ )
57 24 adantr 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> a e. ZZ )
58 27 28 sylan2b 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. NN0 )
59 58 nn0zd 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ZZ )
60 58 nn0ge0d 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> 0 <_ n )
61 elfz4 
 |-  ( ( ( 0 e. ZZ /\ a e. ZZ /\ n e. ZZ ) /\ ( 0 <_ n /\ n <_ a ) ) -> n e. ( 0 ... a ) )
62 56 57 59 60 46 61 syl32anc 
 |-  ( ( a e. NN /\ n e. { k e. NN0 | ( 2 ^ k ) || a } ) -> n e. ( 0 ... a ) )
63 62 ex 
 |-  ( a e. NN -> ( n e. { k e. NN0 | ( 2 ^ k ) || a } -> n e. ( 0 ... a ) ) )
64 63 ssrdv 
 |-  ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) )
65 ssfi 
 |-  ( ( ( 0 ... a ) e. Fin /\ { k e. NN0 | ( 2 ^ k ) || a } C_ ( 0 ... a ) ) -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
66 55 64 65 sylancr 
 |-  ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } e. Fin )
67 0nn0 
 |-  0 e. NN0
68 67 a1i 
 |-  ( a e. NN -> 0 e. NN0 )
69 2cn 
 |-  2 e. CC
70 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
71 69 70 ax-mp 
 |-  ( 2 ^ 0 ) = 1
72 1dvds 
 |-  ( a e. ZZ -> 1 || a )
73 24 72 syl 
 |-  ( a e. NN -> 1 || a )
74 71 73 eqbrtrid 
 |-  ( a e. NN -> ( 2 ^ 0 ) || a )
75 oveq2 
 |-  ( k = 0 -> ( 2 ^ k ) = ( 2 ^ 0 ) )
76 75 breq1d 
 |-  ( k = 0 -> ( ( 2 ^ k ) || a <-> ( 2 ^ 0 ) || a ) )
77 76 elrab 
 |-  ( 0 e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( 0 e. NN0 /\ ( 2 ^ 0 ) || a ) )
78 68 74 77 sylanbrc 
 |-  ( a e. NN -> 0 e. { k e. NN0 | ( 2 ^ k ) || a } )
79 78 ne0d 
 |-  ( a e. NN -> { k e. NN0 | ( 2 ^ k ) || a } =/= (/) )
80 fisupcl 
 |-  ( ( < 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 } )
81 20 66 79 23 80 syl13anc 
 |-  ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { k e. NN0 | ( 2 ^ k ) || a } )
82 oveq2 
 |-  ( k = l -> ( 2 ^ k ) = ( 2 ^ l ) )
83 82 breq1d 
 |-  ( k = l -> ( ( 2 ^ k ) || a <-> ( 2 ^ l ) || a ) )
84 83 cbvrabv 
 |-  { k e. NN0 | ( 2 ^ k ) || a } = { l e. NN0 | ( 2 ^ l ) || a }
85 81 84 eleqtrdi 
 |-  ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. { l e. NN0 | ( 2 ^ l ) || a } )
86 oveq2 
 |-  ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( 2 ^ l ) = ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) )
87 86 breq1d 
 |-  ( l = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) -> ( ( 2 ^ l ) || a <-> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) )
88 87 elrab 
 |-  ( 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 ) )
89 85 88 sylib 
 |-  ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. NN0 /\ ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a ) )
90 89 simprd 
 |-  ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) || a )
91 nndivdvds 
 |-  ( ( 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 ) )
92 91 biimpa 
 |-  ( ( ( 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 )
93 14 54 90 92 syl21anc 
 |-  ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. NN )
94 1nn0 
 |-  1 e. NN0
95 94 a1i 
 |-  ( a e. NN -> 1 e. NN0 )
96 53 95 nn0addcld 
 |-  ( a e. NN -> ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. NN0 )
97 53 nn0red 
 |-  ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
98 97 ltp1d 
 |-  ( a e. NN -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) )
99 20 52 supub 
 |-  ( 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 ) ) )
100 98 99 mt2d 
 |-  ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { k e. NN0 | ( 2 ^ k ) || a } )
101 84 eleq2i 
 |-  ( ( 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 } )
102 100 101 sylnib 
 |-  ( a e. NN -> -. ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) e. { l e. NN0 | ( 2 ^ l ) || a } )
103 oveq2 
 |-  ( l = ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) -> ( 2 ^ l ) = ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) )
104 103 breq1d 
 |-  ( l = ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) -> ( ( 2 ^ l ) || a <-> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a ) )
105 104 elrab 
 |-  ( ( 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 ) )
106 102 105 sylnib 
 |-  ( 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 ) )
107 imnan 
 |-  ( ( ( 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 ) )
108 106 107 sylibr 
 |-  ( 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 ) )
109 96 108 mpd 
 |-  ( a e. NN -> -. ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) || a )
110 expp1 
 |-  ( ( 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 ) )
111 69 53 110 sylancr 
 |-  ( a e. NN -> ( 2 ^ ( sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) + 1 ) ) = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) )
112 111 breq1d 
 |-  ( 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 ) )
113 109 112 mtbid 
 |-  ( a e. NN -> -. ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. 2 ) || a )
114 nncn 
 |-  ( a e. NN -> a e. CC )
115 54 nncnd 
 |-  ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. CC )
116 54 nnne0d 
 |-  ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) =/= 0 )
117 114 115 116 divcan2d 
 |-  ( a e. NN -> ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) = a )
118 117 eqcomd 
 |-  ( a e. NN -> a = ( ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) x. ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
119 118 breq2d 
 |-  ( 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 , < ) ) ) ) ) )
120 15 nnzd 
 |-  ( a e. NN -> 2 e. ZZ )
121 93 nnzd 
 |-  ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
122 54 nnzd 
 |-  ( a e. NN -> ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) e. ZZ )
123 dvdscmulr 
 |-  ( ( 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 , < ) ) ) ) )
124 120 121 122 116 123 syl112anc 
 |-  ( 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 , < ) ) ) ) )
125 119 124 bitrd 
 |-  ( 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 , < ) ) ) ) )
126 113 125 mtbid 
 |-  ( a e. NN -> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) )
127 breq2 
 |-  ( z = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( 2 || z <-> 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
128 127 notbid 
 |-  ( z = ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) -> ( -. 2 || z <-> -. 2 || ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) ) )
129 128 1 elrab2 
 |-  ( ( 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 , < ) ) ) ) )
130 93 126 129 sylanbrc 
 |-  ( a e. NN -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. J )
131 130 53 jca 
 |-  ( 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 ) )
132 131 adantl 
 |-  ( ( 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 ) )
133 simpr 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a = ( ( 2 ^ y ) x. x ) )
134 3 a1i 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> 2 e. NN )
135 simplr 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. NN0 )
136 134 135 nnexpcld 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. NN )
137 8 sseli 
 |-  ( x e. J -> x e. NN )
138 137 ad2antrr 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. NN )
139 136 138 nnmulcld 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) e. NN )
140 133 139 eqeltrd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. NN )
141 simplll 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. J )
142 breq2 
 |-  ( z = x -> ( 2 || z <-> 2 || x ) )
143 142 notbid 
 |-  ( z = x -> ( -. 2 || z <-> -. 2 || x ) )
144 143 1 elrab2 
 |-  ( x e. J <-> ( x e. NN /\ -. 2 || x ) )
145 144 simprbi 
 |-  ( x e. J -> -. 2 || x )
146 2z 
 |-  2 e. ZZ
147 135 adantr 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. NN0 )
148 147 nn0zd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. ZZ )
149 19 a1i 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> < Or NN0 )
150 140 52 syl 
 |-  ( ( ( 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 ) ) )
151 150 adantr 
 |-  ( ( ( ( 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 ) ) )
152 149 151 supcl 
 |-  ( ( ( ( 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 )
153 152 nn0zd 
 |-  ( ( ( ( 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 )
154 simpr 
 |-  ( ( ( ( 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 , < ) )
155 znnsub 
 |-  ( ( 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 ) )
156 155 biimpa 
 |-  ( ( ( 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 )
157 148 153 154 156 syl21anc 
 |-  ( ( ( ( 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 )
158 iddvdsexp 
 |-  ( ( 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 ) ) )
159 146 157 158 sylancr 
 |-  ( ( ( ( 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 ) ) )
160 146 a1i 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 e. ZZ )
161 140 121 syl 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( a / ( 2 ^ sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) ) e. ZZ )
162 161 adantr 
 |-  ( ( ( ( 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 )
163 157 nnnn0d 
 |-  ( ( ( ( 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 )
164 zexpcl 
 |-  ( ( 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 )
165 146 163 164 sylancr 
 |-  ( ( ( ( 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 )
166 dvdsmultr2 
 |-  ( ( 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 ) ) ) ) )
167 160 162 165 166 syl3anc 
 |-  ( ( ( ( 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 ) ) ) ) )
168 159 167 mpd 
 |-  ( ( ( ( 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 ) ) ) )
169 138 adantr 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. NN )
170 169 nncnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. CC )
171 2cnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 e. CC )
172 171 163 expcld 
 |-  ( ( ( ( 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 )
173 140 adantr 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. NN )
174 173 nncnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. CC )
175 173 115 syl 
 |-  ( ( ( ( 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 )
176 2ne0 
 |-  2 =/= 0
177 176 a1i 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 =/= 0 )
178 171 177 153 expne0d 
 |-  ( ( ( ( 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 )
179 174 175 178 divcld 
 |-  ( ( ( ( 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 )
180 172 179 mulcld 
 |-  ( ( ( ( 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 )
181 171 147 expcld 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) e. CC )
182 171 177 148 expne0d 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( 2 ^ y ) =/= 0 )
183 173 118 syl 
 |-  ( ( ( ( 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 , < ) ) ) ) )
184 simplr 
 |-  ( ( ( ( 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 ) )
185 147 nn0cnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> y e. CC )
186 152 nn0cnd 
 |-  ( ( ( ( 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 )
187 185 186 pncan3d 
 |-  ( ( ( ( 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 , < ) )
188 187 oveq2d 
 |-  ( ( ( ( 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 , < ) ) )
189 171 163 147 expaddd 
 |-  ( ( ( ( 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 ) ) ) )
190 188 189 eqtr3d 
 |-  ( ( ( ( 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 ) ) ) )
191 190 oveq1d 
 |-  ( ( ( ( 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 , < ) ) ) ) )
192 183 184 191 3eqtr3d 
 |-  ( ( ( ( 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 , < ) ) ) ) )
193 181 172 179 mulassd 
 |-  ( ( ( ( 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 , < ) ) ) ) ) )
194 192 193 eqtrd 
 |-  ( ( ( ( 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 , < ) ) ) ) ) )
195 170 180 181 182 194 mulcanad 
 |-  ( ( ( ( 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 , < ) ) ) ) )
196 179 172 mulcomd 
 |-  ( ( ( ( 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 , < ) ) ) ) )
197 195 196 eqtr4d 
 |-  ( ( ( ( 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 ) ) ) )
198 168 197 breqtrrd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> 2 || x )
199 145 198 nsyl3 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> -. x e. J )
200 141 199 pm2.65da 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. y < sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
201 138 nnzd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. ZZ )
202 136 nnzd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. ZZ )
203 140 nnzd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> a e. ZZ )
204 136 nncnd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) e. CC )
205 138 nncnd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> x e. CC )
206 204 205 mulcomd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( ( 2 ^ y ) x. x ) = ( x x. ( 2 ^ y ) ) )
207 133 206 eqtr2d 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( x x. ( 2 ^ y ) ) = a )
208 dvds0lem 
 |-  ( ( ( x e. ZZ /\ ( 2 ^ y ) e. ZZ /\ a e. ZZ ) /\ ( x x. ( 2 ^ y ) ) = a ) -> ( 2 ^ y ) || a )
209 201 202 203 207 208 syl31anc 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> ( 2 ^ y ) || a )
210 oveq2 
 |-  ( k = y -> ( 2 ^ k ) = ( 2 ^ y ) )
211 210 breq1d 
 |-  ( k = y -> ( ( 2 ^ k ) || a <-> ( 2 ^ y ) || a ) )
212 211 elrab 
 |-  ( y e. { k e. NN0 | ( 2 ^ k ) || a } <-> ( y e. NN0 /\ ( 2 ^ y ) || a ) )
213 135 209 212 sylanbrc 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. { k e. NN0 | ( 2 ^ k ) || a } )
214 19 a1i 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> < Or NN0 )
215 214 150 supub 
 |-  ( ( ( 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 ) )
216 213 215 mpd 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> -. sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) < y )
217 135 nn0red 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y e. RR )
218 140 97 syl 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) e. RR )
219 217 218 lttri3d 
 |-  ( ( ( 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 ) ) )
220 200 216 219 mpbir2and 
 |-  ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) -> y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) )
221 simplr 
 |-  ( ( ( ( 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 ) )
222 140 adantr 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. NN )
223 222 nncnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> a e. CC )
224 138 adantr 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. NN )
225 224 nncnd 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> x e. CC )
226 nnexpcl 
 |-  ( ( 2 e. NN /\ y e. NN0 ) -> ( 2 ^ y ) e. NN )
227 3 226 mpan 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. NN )
228 227 nncnd 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. CC )
229 227 nnne0d 
 |-  ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
230 228 229 jca 
 |-  ( y e. NN0 -> ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) )
231 230 ad3antlr 
 |-  ( ( ( ( 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 ) )
232 divmul2 
 |-  ( ( a e. CC /\ x e. CC /\ ( ( 2 ^ y ) e. CC /\ ( 2 ^ y ) =/= 0 ) ) -> ( ( a / ( 2 ^ y ) ) = x <-> a = ( ( 2 ^ y ) x. x ) ) )
233 223 225 231 232 syl3anc 
 |-  ( ( ( ( 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 ) ) )
234 221 233 mpbird 
 |-  ( ( ( ( x e. J /\ y e. NN0 ) /\ a = ( ( 2 ^ y ) x. x ) ) /\ y = sup ( { k e. NN0 | ( 2 ^ k ) || a } , NN0 , < ) ) -> ( a / ( 2 ^ y ) ) = x )
235 simpr 
 |-  ( ( ( ( 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 , < ) )
236 235 oveq2d 
 |-  ( ( ( ( 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 , < ) ) )
237 236 oveq2d 
 |-  ( ( ( ( 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 , < ) ) ) )
238 234 237 eqtr3d 
 |-  ( ( ( ( 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 , < ) ) ) )
239 238 ex 
 |-  ( ( ( 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 , < ) ) ) ) )
240 220 239 jcai 
 |-  ( ( ( 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 , < ) ) ) ) )
241 240 ancomd 
 |-  ( ( ( 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 , < ) ) )
242 140 241 jca 
 |-  ( ( ( 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 , < ) ) ) )
243 simprl 
 |-  ( ( 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 , < ) ) ) )
244 130 adantr 
 |-  ( ( 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 )
245 243 244 eqeltrd 
 |-  ( ( 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 )
246 simprr 
 |-  ( ( 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 , < ) )
247 53 adantr 
 |-  ( ( 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 )
248 246 247 eqeltrd 
 |-  ( ( 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 )
249 118 adantr 
 |-  ( ( 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 , < ) ) ) ) )
250 246 oveq2d 
 |-  ( ( 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 , < ) ) )
251 250 243 oveq12d 
 |-  ( ( 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 , < ) ) ) ) )
252 249 251 eqtr4d 
 |-  ( ( 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 ) )
253 245 248 252 jca31 
 |-  ( ( 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 ) ) )
254 242 253 impbii 
 |-  ( ( ( 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 , < ) ) ) )
255 254 a1i 
 |-  ( 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 , < ) ) ) ) )
256 2 13 132 255 f1od2 
 |-  ( T. -> F : ( J X. NN0 ) -1-1-onto-> NN )
257 256 mptru 
 |-  F : ( J X. NN0 ) -1-1-onto-> NN