Metamath Proof Explorer

Theorem nprmmul3

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

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

Proof

Step Hyp Ref Expression
1 nprmmul2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
2 elfzoelz ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → 𝑎 ∈ ℤ )
3 2 zred ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → 𝑎 ∈ ℝ )
4 3 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → 𝑎 ∈ ℝ )
5 elfzoelz ⊢ ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → 𝑏 ∈ ℤ )
6 5 zred ⊢ ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → 𝑏 ∈ ℝ )
7 leloe ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) ) )
8 4 6 7 syl2an ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑎 ≤ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) ) )
9 8 anbi1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
10 andir ⊢ ( ( ( 𝑎 < 𝑏 ∨ 𝑎 = 𝑏 ) ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
11 9 10 bitrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑏 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ) )
12 11 rexbidva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ) )
13 r19.43 ⊢ ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ↔ ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
14 oveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑎 ) )
15 14 equcoms ⊢ ( 𝑎 = 𝑏 → ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑎 ) )
16 15 adantl ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 · 𝑏 ) = ( 𝑎 · 𝑎 ) )
17 2 zcnd ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → 𝑎 ∈ ℂ )
18 17 sqvald ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → ( 𝑎 ↑ 2 ) = ( 𝑎 · 𝑎 ) )
19 18 adantr ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 ↑ 2 ) = ( 𝑎 · 𝑎 ) )
20 16 19 eqtr4d ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 · 𝑏 ) = ( 𝑎 ↑ 2 ) )
21 20 eqeq2d ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝑁 = ( 𝑎 · 𝑏 ) ↔ 𝑁 = ( 𝑎 ↑ 2 ) ) )
22 21 biimpd ⊢ ( ( 𝑎 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑎 = 𝑏 ) → ( 𝑁 = ( 𝑎 · 𝑏 ) → 𝑁 = ( 𝑎 ↑ 2 ) ) )
23 22 ex ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → ( 𝑎 = 𝑏 → ( 𝑁 = ( 𝑎 · 𝑏 ) → 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
24 23 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑎 = 𝑏 → ( 𝑁 = ( 𝑎 · 𝑏 ) → 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
25 24 impd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 = ( 𝑎 ↑ 2 ) ) )
26 25 a1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑏 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
27 26 rexlimdv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) → 𝑁 = ( 𝑎 ↑ 2 ) ) )
28 simplr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) → 𝑎 ∈ ( 2 ..^ 𝑁 ) )
29 equequ2 ⊢ ( 𝑏 = 𝑎 → ( 𝑎 = 𝑏 ↔ 𝑎 = 𝑎 ) )
30 14 eqeq2d ⊢ ( 𝑏 = 𝑎 → ( 𝑁 = ( 𝑎 · 𝑏 ) ↔ 𝑁 = ( 𝑎 · 𝑎 ) ) )
31 29 30 anbi12d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( 𝑎 = 𝑎 ∧ 𝑁 = ( 𝑎 · 𝑎 ) ) ) )
32 31 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) ∧ 𝑏 = 𝑎 ) → ( ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( 𝑎 = 𝑎 ∧ 𝑁 = ( 𝑎 · 𝑎 ) ) ) )
33 18 eqeq2d ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → ( 𝑁 = ( 𝑎 ↑ 2 ) ↔ 𝑁 = ( 𝑎 · 𝑎 ) ) )
34 33 biimpd ⊢ ( 𝑎 ∈ ( 2 ..^ 𝑁 ) → ( 𝑁 = ( 𝑎 ↑ 2 ) → 𝑁 = ( 𝑎 · 𝑎 ) ) )
35 34 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑎 ↑ 2 ) → 𝑁 = ( 𝑎 · 𝑎 ) ) )
36 35 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) → 𝑁 = ( 𝑎 · 𝑎 ) )
37 equid ⊢ 𝑎 = 𝑎
38 36 37 jctil ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) → ( 𝑎 = 𝑎 ∧ 𝑁 = ( 𝑎 · 𝑎 ) ) )
39 28 32 38 rspcedvd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑁 = ( 𝑎 ↑ 2 ) ) → ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) )
40 39 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑁 = ( 𝑎 ↑ 2 ) → ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) )
41 27 40 impbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ 𝑁 = ( 𝑎 ↑ 2 ) ) )
42 41 orbi2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ↔ ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
43 13 42 bitrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ( 𝑎 = 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ) ↔ ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
44 12 43 bitrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑎 ∈ ( 2 ..^ 𝑁 ) ) → ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
45 44 rexbidva ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
46 r19.43 ⊢ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ( ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ 𝑁 = ( 𝑎 ↑ 2 ) ) ↔ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) )
47 45 46 bitrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 ≤ 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ↔ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) ) )
48 1 47 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 𝑁 ∉ ℙ ↔ ( ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) ∃ 𝑏 ∈ ( 2 ..^ 𝑁 ) ( 𝑎 < 𝑏 ∧ 𝑁 = ( 𝑎 · 𝑏 ) ) ∨ ∃ 𝑎 ∈ ( 2 ..^ 𝑁 ) 𝑁 = ( 𝑎 ↑ 2 ) ) ) )