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	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 = ( 2 ↑ 𝐾 ) ) → 4 ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		eluz2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) )
2		zlem1lt	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 ≤ 𝑁 ↔ ( 3 − 1 ) < 𝑁 ) )
3		3m1e2	⊢ ( 3 − 1 ) = 2
4		2cn	⊢ 2 ∈ ℂ
5		exp1	⊢ ( 2 ∈ ℂ → ( 2 ↑ 1 ) = 2 )
6	4 5	ax-mp	⊢ ( 2 ↑ 1 ) = 2
7	3 6	eqtr4i	⊢ ( 3 − 1 ) = ( 2 ↑ 1 )
8	7	breq1i	⊢ ( ( 3 − 1 ) < 𝑁 ↔ ( 2 ↑ 1 ) < 𝑁 )
9		2re	⊢ 2 ∈ ℝ
10	9	a1i	⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℝ )
11		1zzd	⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℤ )
12		nn0z	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℤ )
13		1lt2	⊢ 1 < 2
14	13	a1i	⊢ ( 𝐾 ∈ ℕ0 → 1 < 2 )
15	10 11 12 14	ltexp2d	⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 ↔ ( 2 ↑ 1 ) < ( 2 ↑ 𝐾 ) ) )
16		sq2	⊢ ( 2 ↑ 2 ) = 4
17		2z	⊢ 2 ∈ ℤ
18		2nn0	⊢ 2 ∈ ℕ0
19	17	a1i	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → 2 ∈ ℤ )
20	12	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → 𝐾 ∈ ℤ )
21		df-2	⊢ 2 = ( 1 + 1 )
22	11 12	zltp1led	⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 ↔ ( 1 + 1 ) ≤ 𝐾 ) )
23	22	biimpa	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → ( 1 + 1 ) ≤ 𝐾 )
24	21 23	eqbrtrid	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → 2 ≤ 𝐾 )
25		eluz2	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 2 ≤ 𝐾 ) )
26	19 20 24 25	syl3anbrc	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
27		dvdsexp	⊢ ( ( 2 ∈ ℤ ∧ 2 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ 2 ) ∥ ( 2 ↑ 𝐾 ) )
28	17 18 26 27	mp3an12i	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → ( 2 ↑ 2 ) ∥ ( 2 ↑ 𝐾 ) )
29	16 28	eqbrtrrid	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 1 < 𝐾 ) → 4 ∥ ( 2 ↑ 𝐾 ) )
30	29	ex	⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 𝐾 → 4 ∥ ( 2 ↑ 𝐾 ) ) )
31	15 30	sylbird	⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 ↑ 1 ) < ( 2 ↑ 𝐾 ) → 4 ∥ ( 2 ↑ 𝐾 ) ) )
32		breq2	⊢ ( 𝑁 = ( 2 ↑ 𝐾 ) → ( ( 2 ↑ 1 ) < 𝑁 ↔ ( 2 ↑ 1 ) < ( 2 ↑ 𝐾 ) ) )
33		breq2	⊢ ( 𝑁 = ( 2 ↑ 𝐾 ) → ( 4 ∥ 𝑁 ↔ 4 ∥ ( 2 ↑ 𝐾 ) ) )
34	32 33	imbi12d	⊢ ( 𝑁 = ( 2 ↑ 𝐾 ) → ( ( ( 2 ↑ 1 ) < 𝑁 → 4 ∥ 𝑁 ) ↔ ( ( 2 ↑ 1 ) < ( 2 ↑ 𝐾 ) → 4 ∥ ( 2 ↑ 𝐾 ) ) ) )
35	31 34	imbitrrid	⊢ ( 𝑁 = ( 2 ↑ 𝐾 ) → ( 𝐾 ∈ ℕ0 → ( ( 2 ↑ 1 ) < 𝑁 → 4 ∥ 𝑁 ) ) )
36	35	com13	⊢ ( ( 2 ↑ 1 ) < 𝑁 → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) )
37	36	a1i	⊢ ( 𝑁 ∈ ℤ → ( ( 2 ↑ 1 ) < 𝑁 → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) ) )
38	8 37	biimtrid	⊢ ( 𝑁 ∈ ℤ → ( ( 3 − 1 ) < 𝑁 → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) ) )
39	38	adantl	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 3 − 1 ) < 𝑁 → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) ) )
40	2 39	sylbid	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 ≤ 𝑁 → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) ) )
41	40	3impia	⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) )
42	1 41	sylbi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐾 ∈ ℕ0 → ( 𝑁 = ( 2 ↑ 𝐾 ) → 4 ∥ 𝑁 ) ) )
43	42	3imp	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 = ( 2 ↑ 𝐾 ) ) → 4 ∥ 𝑁 )