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\in \mathbb{N}\to \left(\exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\vee \exists n\in {\mathbb{N}}_{0}N=2^n\right)$$

Proof

Step	Hyp	Ref	Expression
1		oddprmdvds	$$⊢\left(N\in \mathbb{N}\wedge \neg \exists n\in {\mathbb{N}}_{0}N=2^n\right)\to \exists p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)p\parallel N$$
2		rexdifsn	$$⊢\exists p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)p\parallel N\leftrightarrow \exists p\in \mathbb{P}\left(p\ne 2\wedge p\parallel N\right)$$
3		simpr	$$⊢\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\to p\in \mathbb{P}$$
4	3	anim1i	$$⊢\left(\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\wedge p\ne 2\right)\to \left(p\in \mathbb{P}\wedge p\ne 2\right)$$
5		eldifsn	$$⊢p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(p\in \mathbb{P}\wedge p\ne 2\right)$$
6	4 5	sylibr	$$⊢\left(\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\wedge p\ne 2\right)\to p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
7		oddprmgt2	$$⊢p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to 2<p$$
8	6 7	syl	$$⊢\left(\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\wedge p\ne 2\right)\to 2<p$$
9	8	ex	$$⊢\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\to \left(p\ne 2\to 2<p\right)$$
10	9	anim1d	$$⊢\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\to \left(\left(p\ne 2\wedge p\parallel N\right)\to \left(2<p\wedge p\parallel N\right)\right)$$
11	10	reximdva	$$⊢N\in \mathbb{N}\to \left(\exists p\in \mathbb{P}\left(p\ne 2\wedge p\parallel N\right)\to \exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\right)$$
12	2 11	biimtrid	$$⊢N\in \mathbb{N}\to \left(\exists p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)p\parallel N\to \exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\right)$$
13	12	adantr	$$⊢\left(N\in \mathbb{N}\wedge \neg \exists n\in {\mathbb{N}}_{0}N=2^n\right)\to \left(\exists p\in \left(\mathbb{P}\setminus \left\{2\right\}\right)p\parallel N\to \exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\right)$$
14	1 13	mpd	$$⊢\left(N\in \mathbb{N}\wedge \neg \exists n\in {\mathbb{N}}_{0}N=2^n\right)\to \exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)$$
15	14	orcd	$$⊢\left(N\in \mathbb{N}\wedge \neg \exists n\in {\mathbb{N}}_{0}N=2^n\right)\to \left(\exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\vee \exists n\in {\mathbb{N}}_{0}N=2^n\right)$$
16	15	ex	$$⊢N\in \mathbb{N}\to \left(\neg \exists n\in {\mathbb{N}}_{0}N=2^n\to \left(\exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\vee \exists n\in {\mathbb{N}}_{0}N=2^n\right)\right)$$
17		olc	$$⊢\exists n\in {\mathbb{N}}_{0}N=2^n\to \left(\exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\vee \exists n\in {\mathbb{N}}_{0}N=2^n\right)$$
18	16 17	pm2.61d2	$$⊢N\in \mathbb{N}\to \left(\exists p\in \mathbb{P}\left(2<p\wedge p\parallel N\right)\vee \exists n\in {\mathbb{N}}_{0}N=2^n\right)$$