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	$⊢ φ \to X \in ℕ$
	2exple2exp.2	$⊢ φ \to K \in ℕ_{0}$
	2exple2exp.3	$⊢ φ \to 2^{K} ∥ X$
	2exple2exp.4	$⊢ φ \to X \leq 2^{K + 1}$
Assertion	2exple2exp	$⊢ φ \to \exists n \in ℕ_{0} X = 2^{n}$

Proof

Step	Hyp	Ref	Expression
1		2exple2exp.1	$⊢ φ \to X \in ℕ$
2		2exple2exp.2	$⊢ φ \to K \in ℕ_{0}$
3		2exple2exp.3	$⊢ φ \to 2^{K} ∥ X$
4		2exple2exp.4	$⊢ φ \to X \leq 2^{K + 1}$
5		oveq2	$⊢ n = K \to 2^{n} = 2^{K}$
6	5	eqeq2d	$⊢ n = K \to (X = 2^{n} \leftrightarrow X = 2^{K})$
7	2	adantr	$⊢ (φ \land X < 2^{K + 1}) \to K \in ℕ_{0}$
8		simplr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m \in ℕ$
9	8	nnnn0d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m \in ℕ_{0}$
10		2nn	$⊢ 2 \in ℕ$
11	10	a1i	$⊢ φ \to 2 \in ℕ$
12	11 2	nnexpcld	$⊢ φ \to 2^{K} \in ℕ$
13	12	nncnd	$⊢ φ \to 2^{K} \in ℂ$
14	13	ad3antrrr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K} \in ℂ$
15	8	nncnd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m \in ℂ$
16	14 15	mulcomd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K} m = m 2^{K}$
17		simpr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m 2^{K} = X$
18		simpllr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to X < 2^{K + 1}$
19		2cnd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2 \in ℂ$
20	2	ad3antrrr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to K \in ℕ_{0}$
21	19 20	expp1d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K + 1} = 2^{K} \cdot 2$
22	18 21	breqtrd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to X < 2^{K} \cdot 2$
23	17 22	eqbrtrd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m 2^{K} < 2^{K} \cdot 2$
24	16 23	eqbrtrd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K} m < 2^{K} \cdot 2$
25	8	nnred	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m \in ℝ$
26		2re	$⊢ 2 \in ℝ$
27	26	a1i	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2 \in ℝ$
28	12	ad3antrrr	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K} \in ℕ$
29	28	nnrpd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 2^{K} \in ℝ^{+}$
30	25 27 29	ltmul2d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to (m < 2 \leftrightarrow 2^{K} m < 2^{K} \cdot 2)$
31	24 30	mpbird	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m < 2$
32	8	nnne0d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m \neq 0$
33	32	neneqd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to \neg m = 0$
34		nn0lt2	$⊢ (m \in ℕ_{0} \land m < 2) \to (m = 0 \lor m = 1)$
35	34	orcanai	$⊢ ((m \in ℕ_{0} \land m < 2) \land \neg m = 0) \to m = 1$
36	9 31 33 35	syl21anc	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m = 1$
37	36	oveq1d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to m 2^{K} = 1 2^{K}$
38	14	mullidd	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to 1 2^{K} = 2^{K}$
39	37 17 38	3eqtr3d	$⊢ (((φ \land X < 2^{K + 1}) \land m \in ℕ) \land m 2^{K} = X) \to X = 2^{K}$
40		nndivides	$⊢ (2^{K} \in ℕ \land X \in ℕ) \to (2^{K} ∥ X \leftrightarrow \exists m \in ℕ m 2^{K} = X)$
41	40	biimpa	$⊢ ((2^{K} \in ℕ \land X \in ℕ) \land 2^{K} ∥ X) \to \exists m \in ℕ m 2^{K} = X$
42	12 1 3 41	syl21anc	$⊢ φ \to \exists m \in ℕ m 2^{K} = X$
43	42	adantr	$⊢ (φ \land X < 2^{K + 1}) \to \exists m \in ℕ m 2^{K} = X$
44	39 43	r19.29a	$⊢ (φ \land X < 2^{K + 1}) \to X = 2^{K}$
45	6 7 44	rspcedvdw	$⊢ (φ \land X < 2^{K + 1}) \to \exists n \in ℕ_{0} X = 2^{n}$
46		oveq2	$⊢ n = K + 1 \to 2^{n} = 2^{K + 1}$
47	46	eqeq2d	$⊢ n = K + 1 \to (X = 2^{n} \leftrightarrow X = 2^{K + 1})$
48		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
49	2 48	syl	$⊢ φ \to K + 1 \in ℕ_{0}$
50	49	adantr	$⊢ (φ \land X = 2^{K + 1}) \to K + 1 \in ℕ_{0}$
51		simpr	$⊢ (φ \land X = 2^{K + 1}) \to X = 2^{K + 1}$
52	47 50 51	rspcedvdw	$⊢ (φ \land X = 2^{K + 1}) \to \exists n \in ℕ_{0} X = 2^{n}$
53	1	nnred	$⊢ φ \to X \in ℝ$
54	26	a1i	$⊢ φ \to 2 \in ℝ$
55	54 49	reexpcld	$⊢ φ \to 2^{K + 1} \in ℝ$
56		leloe	$⊢ (X \in ℝ \land 2^{K + 1} \in ℝ) \to (X \leq 2^{K + 1} \leftrightarrow (X < 2^{K + 1} \lor X = 2^{K + 1}))$
57	56	biimpa	$⊢ ((X \in ℝ \land 2^{K + 1} \in ℝ) \land X \leq 2^{K + 1}) \to (X < 2^{K + 1} \lor X = 2^{K + 1})$
58	53 55 4 57	syl21anc	$⊢ φ \to (X < 2^{K + 1} \lor X = 2^{K + 1})$
59	45 52 58	mpjaodan	$⊢ φ \to \exists n \in ℕ_{0} X = 2^{n}$

Metamath Proof Explorer

Theorem 2exple2exp

Proof