This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2exple2exp

Description: If a nonnegative integer X is a multiple of a power of two, but less than the next power of two, it is itself a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025)

Ref Expression
Hypotheses 2exple2exp.1 
|- ( ph -> X e. NN )
2exple2exp.2 
|- ( ph -> K e. NN0 )
2exple2exp.3 
|- ( ph -> ( 2 ^ K ) || X )
2exple2exp.4 
|- ( ph -> X <_ ( 2 ^ ( K + 1 ) ) )
Assertion 2exple2exp 
|- ( ph -> E. n e. NN0 X = ( 2 ^ n ) )

Proof

Step Hyp Ref Expression
1 2exple2exp.1 
 |-  ( ph -> X e. NN )
2 2exple2exp.2 
 |-  ( ph -> K e. NN0 )
3 2exple2exp.3 
 |-  ( ph -> ( 2 ^ K ) || X )
4 2exple2exp.4 
 |-  ( ph -> X <_ ( 2 ^ ( K + 1 ) ) )
5 oveq2 
 |-  ( n = K -> ( 2 ^ n ) = ( 2 ^ K ) )
6 5 eqeq2d 
 |-  ( n = K -> ( X = ( 2 ^ n ) <-> X = ( 2 ^ K ) ) )
7 2 adantr 
 |-  ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) -> K e. NN0 )
8 simplr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m e. NN )
9 8 nnnn0d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m e. NN0 )
10 2nn 
 |-  2 e. NN
11 10 a1i 
 |-  ( ph -> 2 e. NN )
12 11 2 nnexpcld 
 |-  ( ph -> ( 2 ^ K ) e. NN )
13 12 nncnd 
 |-  ( ph -> ( 2 ^ K ) e. CC )
14 13 ad3antrrr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( 2 ^ K ) e. CC )
15 8 nncnd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m e. CC )
16 14 15 mulcomd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( ( 2 ^ K ) x. m ) = ( m x. ( 2 ^ K ) ) )
17 simpr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( m x. ( 2 ^ K ) ) = X )
18 simpllr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> X < ( 2 ^ ( K + 1 ) ) )
19 2cnd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> 2 e. CC )
20 2 ad3antrrr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> K e. NN0 )
21 19 20 expp1d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( 2 ^ ( K + 1 ) ) = ( ( 2 ^ K ) x. 2 ) )
22 18 21 breqtrd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> X < ( ( 2 ^ K ) x. 2 ) )
23 17 22 eqbrtrd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( m x. ( 2 ^ K ) ) < ( ( 2 ^ K ) x. 2 ) )
24 16 23 eqbrtrd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( ( 2 ^ K ) x. m ) < ( ( 2 ^ K ) x. 2 ) )
25 8 nnred 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m e. RR )
26 2re 
 |-  2 e. RR
27 26 a1i 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> 2 e. RR )
28 12 ad3antrrr 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( 2 ^ K ) e. NN )
29 28 nnrpd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( 2 ^ K ) e. RR+ )
30 25 27 29 ltmul2d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( m < 2 <-> ( ( 2 ^ K ) x. m ) < ( ( 2 ^ K ) x. 2 ) ) )
31 24 30 mpbird 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m < 2 )
32 8 nnne0d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m =/= 0 )
33 32 neneqd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> -. m = 0 )
34 nn0lt2 
 |-  ( ( m e. NN0 /\ m < 2 ) -> ( m = 0 \/ m = 1 ) )
35 34 orcanai 
 |-  ( ( ( m e. NN0 /\ m < 2 ) /\ -. m = 0 ) -> m = 1 )
36 9 31 33 35 syl21anc 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> m = 1 )
37 36 oveq1d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( m x. ( 2 ^ K ) ) = ( 1 x. ( 2 ^ K ) ) )
38 14 mullidd 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> ( 1 x. ( 2 ^ K ) ) = ( 2 ^ K ) )
39 37 17 38 3eqtr3d 
 |-  ( ( ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) /\ m e. NN ) /\ ( m x. ( 2 ^ K ) ) = X ) -> X = ( 2 ^ K ) )
40 nndivides 
 |-  ( ( ( 2 ^ K ) e. NN /\ X e. NN ) -> ( ( 2 ^ K ) || X <-> E. m e. NN ( m x. ( 2 ^ K ) ) = X ) )
41 40 biimpa 
 |-  ( ( ( ( 2 ^ K ) e. NN /\ X e. NN ) /\ ( 2 ^ K ) || X ) -> E. m e. NN ( m x. ( 2 ^ K ) ) = X )
42 12 1 3 41 syl21anc 
 |-  ( ph -> E. m e. NN ( m x. ( 2 ^ K ) ) = X )
43 42 adantr 
 |-  ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) -> E. m e. NN ( m x. ( 2 ^ K ) ) = X )
44 39 43 r19.29a 
 |-  ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) -> X = ( 2 ^ K ) )
45 6 7 44 rspcedvdw 
 |-  ( ( ph /\ X < ( 2 ^ ( K + 1 ) ) ) -> E. n e. NN0 X = ( 2 ^ n ) )
46 oveq2 
 |-  ( n = ( K + 1 ) -> ( 2 ^ n ) = ( 2 ^ ( K + 1 ) ) )
47 46 eqeq2d 
 |-  ( n = ( K + 1 ) -> ( X = ( 2 ^ n ) <-> X = ( 2 ^ ( K + 1 ) ) ) )
48 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
49 2 48 syl 
 |-  ( ph -> ( K + 1 ) e. NN0 )
50 49 adantr 
 |-  ( ( ph /\ X = ( 2 ^ ( K + 1 ) ) ) -> ( K + 1 ) e. NN0 )
51 simpr 
 |-  ( ( ph /\ X = ( 2 ^ ( K + 1 ) ) ) -> X = ( 2 ^ ( K + 1 ) ) )
52 47 50 51 rspcedvdw 
 |-  ( ( ph /\ X = ( 2 ^ ( K + 1 ) ) ) -> E. n e. NN0 X = ( 2 ^ n ) )
53 1 nnred 
 |-  ( ph -> X e. RR )
54 26 a1i 
 |-  ( ph -> 2 e. RR )
55 54 49 reexpcld 
 |-  ( ph -> ( 2 ^ ( K + 1 ) ) e. RR )
56 leloe 
 |-  ( ( X e. RR /\ ( 2 ^ ( K + 1 ) ) e. RR ) -> ( X <_ ( 2 ^ ( K + 1 ) ) <-> ( X < ( 2 ^ ( K + 1 ) ) \/ X = ( 2 ^ ( K + 1 ) ) ) ) )
57 56 biimpa 
 |-  ( ( ( X e. RR /\ ( 2 ^ ( K + 1 ) ) e. RR ) /\ X <_ ( 2 ^ ( K + 1 ) ) ) -> ( X < ( 2 ^ ( K + 1 ) ) \/ X = ( 2 ^ ( K + 1 ) ) ) )
58 53 55 4 57 syl21anc 
 |-  ( ph -> ( X < ( 2 ^ ( K + 1 ) ) \/ X = ( 2 ^ ( K + 1 ) ) ) )
59 45 52 58 mpjaodan 
 |-  ( ph -> E. n e. NN0 X = ( 2 ^ n ) )