Theorem fltoprmlem1

Description: Lemma 1 for fltoprm : Every positive integer is either a power of 2 or has an odd prime factor. (Contributed by AV, 15-Sep-2026)

	Ref	Expression
Assertion	fltoprmlem1	|- ( N e. NN -> ( E. p e. Prime ( 2 < p /\ p || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )

Proof

Step	Hyp	Ref	Expression
1		oddprmdvds	|- ( ( N e. NN /\ -. E. n e. NN0 N = ( 2 ^ n ) ) -> E. p e. ( Prime \ { 2 } ) p || N )
2		rexdifsn	|- ( E. p e. ( Prime \ { 2 } ) p || N <-> E. p e. Prime ( p =/= 2 /\ p || N ) )
3		simpr	|- ( ( N e. NN /\ p e. Prime ) -> p e. Prime )
4	3	anim1i	|- ( ( ( N e. NN /\ p e. Prime ) /\ p =/= 2 ) -> ( p e. Prime /\ p =/= 2 ) )
5		eldifsn	|- ( p e. ( Prime \ { 2 } ) <-> ( p e. Prime /\ p =/= 2 ) )
6	4 5	sylibr	|- ( ( ( N e. NN /\ p e. Prime ) /\ p =/= 2 ) -> p e. ( Prime \ { 2 } ) )
7		oddprmgt2	|- ( p e. ( Prime \ { 2 } ) -> 2 < p )
8	6 7	syl	|- ( ( ( N e. NN /\ p e. Prime ) /\ p =/= 2 ) -> 2 < p )
9	8	ex	|- ( ( N e. NN /\ p e. Prime ) -> ( p =/= 2 -> 2 < p ) )
10	9	anim1d	|- ( ( N e. NN /\ p e. Prime ) -> ( ( p =/= 2 /\ p || N ) -> ( 2 < p /\ p || N ) ) )
11	10	reximdva	|- ( N e. NN -> ( E. p e. Prime ( p =/= 2 /\ p || N ) -> E. p e. Prime ( 2 < p /\ p || N ) ) )
12	2 11	biimtrid	|- ( N e. NN -> ( E. p e. ( Prime \ { 2 } ) p || N -> E. p e. Prime ( 2 < p /\ p || N ) ) )
13	12	adantr	|- ( ( N e. NN /\ -. E. n e. NN0 N = ( 2 ^ n ) ) -> ( E. p e. ( Prime \ { 2 } ) p || N -> E. p e. Prime ( 2 < p /\ p || N ) ) )
14	1 13	mpd	|- ( ( N e. NN /\ -. E. n e. NN0 N = ( 2 ^ n ) ) -> E. p e. Prime ( 2 < p /\ p || N ) )
15	14	orcd	|- ( ( N e. NN /\ -. E. n e. NN0 N = ( 2 ^ n ) ) -> ( E. p e. Prime ( 2 < p /\ p || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )
16	15	ex	|- ( N e. NN -> ( -. E. n e. NN0 N = ( 2 ^ n ) -> ( E. p e. Prime ( 2 < p /\ p || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) ) )
17		olc	|- ( E. n e. NN0 N = ( 2 ^ n ) -> ( E. p e. Prime ( 2 < p /\ p || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )
18	16 17	pm2.61d2	|- ( N e. NN -> ( E. p e. Prime ( 2 < p /\ p || N ) \/ E. n e. NN0 N = ( 2 ^ n ) ) )