Theorem fltoprmlem2

Description: Lemma 2 for fltoprm : If an integer greater than or equal to 3 is a power of 2, it is a multiple of 4. (Contributed by AV, 15-Sep-2026)

	Ref	Expression
Assertion	fltoprmlem2	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in {\mathbb{N}}_0\wedge N=2^K\right)\to 4\parallel N$$

Proof

Step	Hyp	Ref	Expression
1		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge 3}\leftrightarrow \left(3\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 3\le N\right)$$
2		zlem1lt	$$⊢\left(3\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(3\le N\leftrightarrow 3-1<N\right)$$
3		3m1e2	$$⊢3-1=2$$
4		2cn	$$⊢2\in ℂ$$
5		exp1	$$⊢2\in ℂ\to 2^1=2$$
6	4 5	ax-mp	$$⊢2^1=2$$
7	3 6	eqtr4i	$$⊢3-1=2^1$$
8	7	breq1i	$$⊢3-1<N\leftrightarrow 2^1<N$$
9		2re	$$⊢2\in ℝ$$
10	9	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in ℝ$$
11		1zzd	$$⊢K\in {\mathbb{N}}_0\to 1\in \mathbb{Z}$$
12		nn0z	$$⊢K\in {\mathbb{N}}_0\to K\in \mathbb{Z}$$
13		1lt2	$$⊢1<2$$
14	13	a1i	$$⊢K\in {\mathbb{N}}_0\to 1<2$$
15	10 11 12 14	ltexp2d	$$⊢K\in {\mathbb{N}}_0\to \left(1<K\leftrightarrow 2^1<2^K\right)$$
16		sq2	$$⊢2^2=4$$
17		2z	$$⊢2\in \mathbb{Z}$$
18		2nn0	$$⊢2\in {\mathbb{N}}_0$$
19	17	a1i	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to 2\in \mathbb{Z}$$
20	12	adantr	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to K\in \mathbb{Z}$$
21		df-2	$$⊢2=1+1$$
22	11 12	zltp1led	$$⊢K\in {\mathbb{N}}_0\to \left(1<K\leftrightarrow 1+1\le K\right)$$
23	22	biimpa	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to 1+1\le K$$
24	21 23	eqbrtrid	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to 2\le K$$
25		eluz2	$$⊢K\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{Z}\wedge K\in \mathbb{Z}\wedge 2\le K\right)$$
26	19 20 24 25	syl3anbrc	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to K\in {\mathbb{Z}}_{\ge 2}$$
27		dvdsexp	$$⊢\left(2\in \mathbb{Z}\wedge 2\in {\mathbb{N}}_0\wedge K\in {\mathbb{Z}}_{\ge 2}\right)\to 2^2\parallel 2^K$$
28	17 18 26 27	mp3an12i	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to 2^2\parallel 2^K$$
29	16 28	eqbrtrrid	$$⊢\left(K\in {\mathbb{N}}_0\wedge 1<K\right)\to 4\parallel 2^K$$
30	29	ex	$$⊢K\in {\mathbb{N}}_0\to \left(1<K\to 4\parallel 2^K\right)$$
31	15 30	sylbird	$$⊢K\in {\mathbb{N}}_0\to \left(2^1<2^K\to 4\parallel 2^K\right)$$
32		breq2	$$⊢N=2^K\to \left(2^1<N\leftrightarrow 2^1<2^K\right)$$
33		breq2	$$⊢N=2^K\to \left(4\parallel N\leftrightarrow 4\parallel 2^K\right)$$
34	32 33	imbi12d	$$⊢N=2^K\to \left(\left(2^1<N\to 4\parallel N\right)\leftrightarrow \left(2^1<2^K\to 4\parallel 2^K\right)\right)$$
35	31 34	imbitrrid	$$⊢N=2^K\to \left(K\in {\mathbb{N}}_0\to \left(2^1<N\to 4\parallel N\right)\right)$$
36	35	com13	$$⊢2^1<N\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)$$
37	36	a1i	$$⊢N\in \mathbb{Z}\to \left(2^1<N\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)\right)$$
38	8 37	biimtrid	$$⊢N\in \mathbb{Z}\to \left(3-1<N\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)\right)$$
39	38	adantl	$$⊢\left(3\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(3-1<N\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)\right)$$
40	2 39	sylbid	$$⊢\left(3\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(3\le N\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)\right)$$
41	40	3impia	$$⊢\left(3\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 3\le N\right)\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)$$
42	1 41	sylbi	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(K\in {\mathbb{N}}_0\to \left(N=2^K\to 4\parallel N\right)\right)$$
43	42	3imp	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge K\in {\mathbb{N}}_0\wedge N=2^K\right)\to 4\parallel N$$