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 ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
2exple2exp.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
2exple2exp.3 ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∥ 𝑋 )
2exple2exp.4 ⊢ ( 𝜑 → 𝑋 ≤ ( 2 ↑ ( 𝐾 + 1 ) ) )
Assertion 2exple2exp ( 𝜑 → ∃ 𝑛 ∈ ℕ0 𝑋 = ( 2 ↑ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 2exple2exp.1 ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
2 2exple2exp.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 2exple2exp.3 ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∥ 𝑋 )
4 2exple2exp.4 ⊢ ( 𝜑 → 𝑋 ≤ ( 2 ↑ ( 𝐾 + 1 ) ) )
5 oveq2 ⊢ ( 𝑛 = 𝐾 → ( 2 ↑ 𝑛 ) = ( 2 ↑ 𝐾 ) )
6 5 eqeq2d ⊢ ( 𝑛 = 𝐾 → ( 𝑋 = ( 2 ↑ 𝑛 ) ↔ 𝑋 = ( 2 ↑ 𝐾 ) ) )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) → 𝐾 ∈ ℕ0 )
8 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 ∈ ℕ )
9 8 nnnn0d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 ∈ ℕ0 )
10 2nn ⊢ 2 ∈ ℕ
11 10 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
12 11 2 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ )
13 12 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℂ )
14 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 2 ↑ 𝐾 ) ∈ ℂ )
15 8 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 ∈ ℂ )
16 14 15 mulcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( ( 2 ↑ 𝐾 ) · 𝑚 ) = ( 𝑚 · ( 2 ↑ 𝐾 ) ) )
17 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) )
19 2cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 2 ∈ ℂ )
20 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝐾 ∈ ℕ0 )
21 19 20 expp1d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 2 ↑ ( 𝐾 + 1 ) ) = ( ( 2 ↑ 𝐾 ) · 2 ) )
22 18 21 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑋 < ( ( 2 ↑ 𝐾 ) · 2 ) )
23 17 22 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 𝑚 · ( 2 ↑ 𝐾 ) ) < ( ( 2 ↑ 𝐾 ) · 2 ) )
24 16 23 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( ( 2 ↑ 𝐾 ) · 𝑚 ) < ( ( 2 ↑ 𝐾 ) · 2 ) )
25 8 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 ∈ ℝ )
26 2re ⊢ 2 ∈ ℝ
27 26 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 2 ∈ ℝ )
28 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 2 ↑ 𝐾 ) ∈ ℕ )
29 28 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 2 ↑ 𝐾 ) ∈ ℝ+ )
30 25 27 29 ltmul2d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 𝑚 < 2 ↔ ( ( 2 ↑ 𝐾 ) · 𝑚 ) < ( ( 2 ↑ 𝐾 ) · 2 ) ) )
31 24 30 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 < 2 )
32 8 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 ≠ 0 )
33 32 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ¬ 𝑚 = 0 )
34 nn0lt2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 < 2 ) → ( 𝑚 = 0 ∨ 𝑚 = 1 ) )
35 34 orcanai ⊢ ( ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 < 2 ) ∧ ¬ 𝑚 = 0 ) → 𝑚 = 1 )
36 9 31 33 35 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑚 = 1 )
37 36 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 𝑚 · ( 2 ↑ 𝐾 ) ) = ( 1 · ( 2 ↑ 𝐾 ) ) )
38 14 mullidd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → ( 1 · ( 2 ↑ 𝐾 ) ) = ( 2 ↑ 𝐾 ) )
39 37 17 38 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) → 𝑋 = ( 2 ↑ 𝐾 ) )
40 nndivides ⊢ ( ( ( 2 ↑ 𝐾 ) ∈ ℕ ∧ 𝑋 ∈ ℕ ) → ( ( 2 ↑ 𝐾 ) ∥ 𝑋 ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 ) )
41 40 biimpa ⊢ ( ( ( ( 2 ↑ 𝐾 ) ∈ ℕ ∧ 𝑋 ∈ ℕ ) ∧ ( 2 ↑ 𝐾 ) ∥ 𝑋 ) → ∃ 𝑚 ∈ ℕ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 )
42 12 1 3 41 syl21anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) → ∃ 𝑚 ∈ ℕ ( 𝑚 · ( 2 ↑ 𝐾 ) ) = 𝑋 )
44 39 43 r19.29a ⊢ ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) → 𝑋 = ( 2 ↑ 𝐾 ) )
45 6 7 44 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ0 𝑋 = ( 2 ↑ 𝑛 ) )
46 oveq2 ⊢ ( 𝑛 = ( 𝐾 + 1 ) → ( 2 ↑ 𝑛 ) = ( 2 ↑ ( 𝐾 + 1 ) ) )
47 46 eqeq2d ⊢ ( 𝑛 = ( 𝐾 + 1 ) → ( 𝑋 = ( 2 ↑ 𝑛 ) ↔ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) )
48 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
49 2 48 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) → ( 𝐾 + 1 ) ∈ ℕ0 )
51 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) → 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) )
52 47 50 51 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ0 𝑋 = ( 2 ↑ 𝑛 ) )
53 1 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
54 26 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
55 54 49 reexpcld ⊢ ( 𝜑 → ( 2 ↑ ( 𝐾 + 1 ) ) ∈ ℝ )
56 leloe ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 2 ↑ ( 𝐾 + 1 ) ) ∈ ℝ ) → ( 𝑋 ≤ ( 2 ↑ ( 𝐾 + 1 ) ) ↔ ( 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ∨ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) ) )
57 56 biimpa ⊢ ( ( ( 𝑋 ∈ ℝ ∧ ( 2 ↑ ( 𝐾 + 1 ) ) ∈ ℝ ) ∧ 𝑋 ≤ ( 2 ↑ ( 𝐾 + 1 ) ) ) → ( 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ∨ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) )
58 53 55 4 57 syl21anc ⊢ ( 𝜑 → ( 𝑋 < ( 2 ↑ ( 𝐾 + 1 ) ) ∨ 𝑋 = ( 2 ↑ ( 𝐾 + 1 ) ) ) )
59 45 52 58 mpjaodan ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ0 𝑋 = ( 2 ↑ 𝑛 ) )