Metamath Proof Explorer

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 
|- ( ( N e. ( ZZ>= ` 3 ) /\ K e. NN0 /\ N = ( 2 ^ K ) ) -> 4 || N )

Proof

Step Hyp Ref Expression
1 eluz2 
 |-  ( N e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) )
2 zlem1lt 
 |-  ( ( 3 e. ZZ /\ N e. ZZ ) -> ( 3 <_ N <-> ( 3 - 1 ) < N ) )
3 3m1e2 
 |-  ( 3 - 1 ) = 2
4 2cn 
 |-  2 e. CC
5 exp1 
 |-  ( 2 e. CC -> ( 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 <-> ( 2 ^ 1 ) < N )
9 2re 
 |-  2 e. RR
10 9 a1i 
 |-  ( K e. NN0 -> 2 e. RR )
11 1zzd 
 |-  ( K e. NN0 -> 1 e. ZZ )
12 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
13 1lt2 
 |-  1 < 2
14 13 a1i 
 |-  ( K e. NN0 -> 1 < 2 )
15 10 11 12 14 ltexp2d 
 |-  ( K e. NN0 -> ( 1 < K <-> ( 2 ^ 1 ) < ( 2 ^ K ) ) )
16 sq2 
 |-  ( 2 ^ 2 ) = 4
17 2z 
 |-  2 e. ZZ
18 2nn0 
 |-  2 e. NN0
19 17 a1i 
 |-  ( ( K e. NN0 /\ 1 < K ) -> 2 e. ZZ )
20 12 adantr 
 |-  ( ( K e. NN0 /\ 1 < K ) -> K e. ZZ )
21 df-2 
 |-  2 = ( 1 + 1 )
22 11 12 zltp1led 
 |-  ( K e. NN0 -> ( 1 < K <-> ( 1 + 1 ) <_ K ) )
23 22 biimpa 
 |-  ( ( K e. NN0 /\ 1 < K ) -> ( 1 + 1 ) <_ K )
24 21 23 eqbrtrid 
 |-  ( ( K e. NN0 /\ 1 < K ) -> 2 <_ K )
25 eluz2 
 |-  ( K e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ K e. ZZ /\ 2 <_ K ) )
26 19 20 24 25 syl3anbrc 
 |-  ( ( K e. NN0 /\ 1 < K ) -> K e. ( ZZ>= ` 2 ) )
27 dvdsexp 
 |-  ( ( 2 e. ZZ /\ 2 e. NN0 /\ K e. ( ZZ>= ` 2 ) ) -> ( 2 ^ 2 ) || ( 2 ^ K ) )
28 17 18 26 27 mp3an12i 
 |-  ( ( K e. NN0 /\ 1 < K ) -> ( 2 ^ 2 ) || ( 2 ^ K ) )
29 16 28 eqbrtrrid 
 |-  ( ( K e. NN0 /\ 1 < K ) -> 4 || ( 2 ^ K ) )
30 29 ex 
 |-  ( K e. NN0 -> ( 1 < K -> 4 || ( 2 ^ K ) ) )
31 15 30 sylbird 
 |-  ( K e. NN0 -> ( ( 2 ^ 1 ) < ( 2 ^ K ) -> 4 || ( 2 ^ K ) ) )
32 breq2 
 |-  ( N = ( 2 ^ K ) -> ( ( 2 ^ 1 ) < N <-> ( 2 ^ 1 ) < ( 2 ^ K ) ) )
33 breq2 
 |-  ( N = ( 2 ^ K ) -> ( 4 || N <-> 4 || ( 2 ^ K ) ) )
34 32 33 imbi12d 
 |-  ( N = ( 2 ^ K ) -> ( ( ( 2 ^ 1 ) < N -> 4 || N ) <-> ( ( 2 ^ 1 ) < ( 2 ^ K ) -> 4 || ( 2 ^ K ) ) ) )
35 31 34 imbitrrid 
 |-  ( N = ( 2 ^ K ) -> ( K e. NN0 -> ( ( 2 ^ 1 ) < N -> 4 || N ) ) )
36 35 com13 
 |-  ( ( 2 ^ 1 ) < N -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) )
37 36 a1i 
 |-  ( N e. ZZ -> ( ( 2 ^ 1 ) < N -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) ) )
38 8 37 biimtrid 
 |-  ( N e. ZZ -> ( ( 3 - 1 ) < N -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) ) )
39 38 adantl 
 |-  ( ( 3 e. ZZ /\ N e. ZZ ) -> ( ( 3 - 1 ) < N -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) ) )
40 2 39 sylbid 
 |-  ( ( 3 e. ZZ /\ N e. ZZ ) -> ( 3 <_ N -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) ) )
41 40 3impia 
 |-  ( ( 3 e. ZZ /\ N e. ZZ /\ 3 <_ N ) -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) )
42 1 41 sylbi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( K e. NN0 -> ( N = ( 2 ^ K ) -> 4 || N ) ) )
43 42 3imp 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. NN0 /\ N = ( 2 ^ K ) ) -> 4 || N )