Metamath Proof Explorer

Theorem nprmmul2

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

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

Proof

Step Hyp Ref Expression
1 nprmmul1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) ) )
2 breq1 ⊢ ( 𝑎 = 𝑛 → ( 𝑎 ≤ 𝑏 ↔ 𝑛 ≤ 𝑏 ) )
3 oveq1 ⊢ ( 𝑎 = 𝑛 → ( 𝑎 · 𝑏 ) = ( 𝑛 · 𝑏 ) )
4 3 eqeq2d ⊢ ( 𝑎 = 𝑛 → ( 𝑁 = ( 𝑎 · 𝑏 ) ↔ 𝑁 = ( 𝑛 · 𝑏 ) ) )
5 2 4 anbi12d ⊢ ( 𝑎 = 𝑛 → ( ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( 𝑛 ≤ 𝑏 ∧ 𝑁 = ( 𝑛 · 𝑏 ) ) ) )
6 breq2 ⊢ ( 𝑏 = 𝑚 → ( 𝑛 ≤ 𝑏 ↔ 𝑛 ≤ 𝑚 ) )
7 oveq2 ⊢ ( 𝑏 = 𝑚 → ( 𝑛 · 𝑏 ) = ( 𝑛 · 𝑚 ) )
8 7 eqeq2d ⊢ ( 𝑏 = 𝑚 → ( 𝑁 = ( 𝑛 · 𝑏 ) ↔ 𝑁 = ( 𝑛 · 𝑚 ) ) )
9 6 8 anbi12d ⊢ ( 𝑏 = 𝑚 → ( ( 𝑛 ≤ 𝑏 ∧ 𝑁 = ( 𝑛 · 𝑏 ) ) ↔ ( 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑛 · 𝑚 ) ) ) )
10 simp1rr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑛 ∈ ( 2 ..^ 𝑁 ) )
11 simp1rl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑚 ∈ ( 2 ..^ 𝑁 ) )
12 simp2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑛 ≤ 𝑚 )
13 elfzo2nn ⊢ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) → 𝑚 ∈ ℕ )
14 elfzo2nn ⊢ ( 𝑛 ∈ ( 2 ..^ 𝑁 ) → 𝑛 ∈ ℕ )
15 nnmulcom ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑚 · 𝑛 ) = ( 𝑛 · 𝑚 ) )
16 13 14 15 syl2an ⊢ ( ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑚 · 𝑛 ) = ( 𝑛 · 𝑚 ) )
17 16 eqeq2d ⊢ ( ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑚 · 𝑛 ) ↔ 𝑁 = ( 𝑛 · 𝑚 ) ) )
18 17 biimpd ⊢ ( ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑚 · 𝑛 ) → 𝑁 = ( 𝑛 · 𝑚 ) ) )
19 18 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑁 = ( 𝑚 · 𝑛 ) → 𝑁 = ( 𝑛 · 𝑚 ) ) )
20 19 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑁 = ( 𝑛 · 𝑚 ) )
21 20 3adant2 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑁 = ( 𝑛 · 𝑚 ) )
22 12 21 jca ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → ( 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑛 · 𝑚 ) ) )
23 5 9 10 11 22 2rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑛 ≤ 𝑚 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) )
24 23 3exp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑛 ≤ 𝑚 → ( 𝑁 = ( 𝑚 · 𝑛 ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ) )
25 breq1 ⊢ ( 𝑎 = 𝑚 → ( 𝑎 ≤ 𝑏 ↔ 𝑚 ≤ 𝑏 ) )
26 oveq1 ⊢ ( 𝑎 = 𝑚 → ( 𝑎 · 𝑏 ) = ( 𝑚 · 𝑏 ) )
27 26 eqeq2d ⊢ ( 𝑎 = 𝑚 → ( 𝑁 = ( 𝑎 · 𝑏 ) ↔ 𝑁 = ( 𝑚 · 𝑏 ) ) )
28 25 27 anbi12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( 𝑚 ≤ 𝑏 ∧ 𝑁 = ( 𝑚 · 𝑏 ) ) ) )
29 breq2 ⊢ ( 𝑏 = 𝑛 → ( 𝑚 ≤ 𝑏 ↔ 𝑚 ≤ 𝑛 ) )
30 oveq2 ⊢ ( 𝑏 = 𝑛 → ( 𝑚 · 𝑏 ) = ( 𝑚 · 𝑛 ) )
31 30 eqeq2d ⊢ ( 𝑏 = 𝑛 → ( 𝑁 = ( 𝑚 · 𝑏 ) ↔ 𝑁 = ( 𝑚 · 𝑛 ) ) )
32 29 31 anbi12d ⊢ ( 𝑏 = 𝑛 → ( ( 𝑚 ≤ 𝑏 ∧ 𝑁 = ( 𝑚 · 𝑏 ) ) ↔ ( 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) ) )
33 simp1rl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑚 ∈ ( 2 ..^ 𝑁 ) )
34 simp1rr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → 𝑛 ∈ ( 2 ..^ 𝑁 ) )
35 3simpc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → ( 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) )
36 28 32 33 34 35 2rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑚 ≤ 𝑛 ∧ 𝑁 = ( 𝑚 · 𝑛 ) ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) )
37 36 3exp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑚 ≤ 𝑛 → ( 𝑁 = ( 𝑚 · 𝑛 ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ) )
38 elfzoelz ⊢ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) → 𝑚 ∈ ℤ )
39 38 zred ⊢ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) → 𝑚 ∈ ℝ )
40 elfzoelz ⊢ ( 𝑛 ∈ ( 2 ..^ 𝑁 ) → 𝑛 ∈ ℤ )
41 40 zred ⊢ ( 𝑛 ∈ ( 2 ..^ 𝑁 ) → 𝑛 ∈ ℝ )
42 39 41 anim12ci ⊢ ( ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ ) )
43 42 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ ) )
44 letric ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( 𝑛 ≤ 𝑚 ∨ 𝑚 ≤ 𝑛 ) )
45 43 44 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑛 ≤ 𝑚 ∨ 𝑚 ≤ 𝑛 ) )
46 24 37 45 mpjaod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑚 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑛 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑁 = ( 𝑚 · 𝑛 ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
47 46 rexlimdvva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) → ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
48 oveq1 ⊢ ( 𝑚 = 𝑎 → ( 𝑚 · 𝑛 ) = ( 𝑎 · 𝑛 ) )
49 48 eqeq2d ⊢ ( 𝑚 = 𝑎 → ( 𝑁 = ( 𝑚 · 𝑛 ) ↔ 𝑁 = ( 𝑎 · 𝑛 ) ) )
50 oveq2 ⊢ ( 𝑛 = 𝑏 → ( 𝑎 · 𝑛 ) = ( 𝑎 · 𝑏 ) )
51 50 eqeq2d ⊢ ( 𝑛 = 𝑏 → ( 𝑁 = ( 𝑎 · 𝑛 ) ↔ 𝑁 = ( 𝑎 · 𝑏 ) ) )
52 simplrl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑎 ∈ ( 2 ..^ 𝑁 ) )
53 simplrr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑏 ∈ ( 2 ..^ 𝑁 ) )
54 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 = ( 𝑎 · 𝑏 ) )
55 49 51 52 53 54 2rspcedvdw ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) )
56 55 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → ( 𝑁 = ( 𝑎 · 𝑏 ) → ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) ) )
57 56 adantld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) ) → ( ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) ) )
58 57 rexlimdvva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) ) )
59 47 58 impbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑚 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑚 · 𝑛 ) ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
60 1 59 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )