Metamath Proof Explorer

Theorem nprmmul1

Description: Special factorization of a non-prime integer greater than 3. (Contributed by AV, 5-Apr-2026)

Ref Expression
Assertion nprmmul1 ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 isprm3 ⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ) )
2 1 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ) ) )
3 uzuzle24 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
4 3 biantrurd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ) ) )
5 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℤ )
6 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 2 ..^ 𝑁 ) = ( 2 ... ( 𝑁 − 1 ) ) )
7 5 6 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ..^ 𝑁 ) = ( 2 ... ( 𝑁 − 1 ) ) )
8 7 eqcomd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ... ( 𝑁 − 1 ) ) = ( 2 ..^ 𝑁 ) )
9 8 raleqdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ↔ ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ 𝑎 ∥ 𝑁 ) )
10 eluz4nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℕ )
11 10 anim1ci ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) )
12 nndivides2 ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑎 ∥ 𝑁 ↔ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑏 · 𝑎 ) = 𝑁 ) )
13 11 12 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑎 ∥ 𝑁 ↔ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑏 · 𝑎 ) = 𝑁 ) )
14 eqcom ⊢ ( ( 𝑏 · 𝑎 ) = 𝑁 ↔ 𝑁 = ( 𝑏 · 𝑎 ) )
15 elfzo2nn ⊢ ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → 𝑏 ∈ ℕ )
16 elfzo2nn ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → 𝑎 ∈ ℕ )
17 16 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → 𝑎 ∈ ℕ )
18 nnmulcom ⊢ ( ( 𝑏 ∈ ℕ ∧ 𝑎 ∈ ℕ ) → ( 𝑏 · 𝑎 ) = ( 𝑎 · 𝑏 ) )
19 15 17 18 syl2anr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑏 · 𝑎 ) = ( 𝑎 · 𝑏 ) )
20 19 eqeq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑏 · 𝑎 ) ↔ 𝑁 = ( 𝑎 · 𝑏 ) ) )
21 14 20 bitrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝑏 · 𝑎 ) = 𝑁 ↔ 𝑁 = ( 𝑎 · 𝑏 ) ) )
22 21 rexbidva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑏 · 𝑎 ) = 𝑁 ↔ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
23 13 22 bitrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑎 ∥ 𝑁 ↔ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
24 23 notbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ¬ 𝑎 ∥ 𝑁 ↔ ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
25 24 ralbidva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ 𝑎 ∥ 𝑁 ↔ ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
26 9 25 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∀ 𝑎 ∈ ( 2 ... ( 𝑁 − 1 ) ) ¬ 𝑎 ∥ 𝑁 ↔ ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
27 2 4 26 3bitr2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∈ ℙ ↔ ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
28 nnel ⊢ ( ¬ 𝑁 ∉ ℙ ↔ 𝑁 ∈ ℙ )
29 ralnex ⊢ ( ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ↔ ¬ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) )
30 29 bicomi ⊢ ( ¬ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ↔ ∀ 𝑎 ∈ ( 2 ..^ 𝑁 ) ¬ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) )
31 27 28 30 3bitr4g ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ¬ 𝑁 ∉ ℙ ↔ ¬ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )
32 31 con4bid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 · 𝑏 ) ) )