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	⊢ ( 𝑁 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ∨ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oddprmdvds	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝑁 )
2		rexdifsn	⊢ ( ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝑁 ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ≠ 2 ∧ 𝑝 ∥ 𝑁 ) )
3		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
4	3	anim1i	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 2 ) → ( 𝑝 ∈ ℙ ∧ 𝑝 ≠ 2 ) )
5		eldifsn	⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑝 ∈ ℙ ∧ 𝑝 ≠ 2 ) )
6	4 5	sylibr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 2 ) → 𝑝 ∈ ( ℙ ∖ { 2 } ) )
7		oddprmgt2	⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 2 < 𝑝 )
8	6 7	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ≠ 2 ) → 2 < 𝑝 )
9	8	ex	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ≠ 2 → 2 < 𝑝 ) )
10	9	anim1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 ≠ 2 ∧ 𝑝 ∥ 𝑁 ) → ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ) )
11	10	reximdva	⊢ ( 𝑁 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ ( 𝑝 ≠ 2 ∧ 𝑝 ∥ 𝑁 ) → ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ) )
12	2 11	biimtrid	⊢ ( 𝑁 ∈ ℕ → ( ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝑁 → ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ) )
13	12	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) → ( ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝑁 → ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ) )
14	1 13	mpd	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) )
15	14	orcd	⊢ ( ( 𝑁 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) → ( ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ∨ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) )
16	15	ex	⊢ ( 𝑁 ∈ ℕ → ( ¬ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ∨ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) ) )
17		olc	⊢ ( ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ∨ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) )
18	16 17	pm2.61d2	⊢ ( 𝑁 ∈ ℕ → ( ∃ 𝑝 ∈ ℙ ( 2 < 𝑝 ∧ 𝑝 ∥ 𝑁 ) ∨ ∃ 𝑛 ∈ ℕ0 𝑁 = ( 2 ↑ 𝑛 ) ) )