Metamath Proof Explorer

Theorem nndivides2

Description: Definition of the divides relation for divisors greater than 1. (Contributed by AV, 5-Apr-2026)

Ref Expression
Assertion nndivides2 ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfzo2nn ⊢ ( 𝑀 ∈ ( 2 ..^ 𝑁 ) → 𝑀 ∈ ℕ )
2 nndivides ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )
3 1 2 sylan ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )
4 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · 𝑀 ) = ( 𝑚 · 𝑀 ) )
5 4 eqeq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 · 𝑀 ) = 𝑁 ↔ ( 𝑚 · 𝑀 ) = 𝑁 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑀 ) = 𝑁 )
7 simplll ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → 𝑀 ∈ ( 2 ..^ 𝑁 ) )
8 simpr ⊢ ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
9 8 adantr ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → 𝑚 ∈ ℕ )
10 1 adantr ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → 𝑀 ∈ ℕ )
11 10 anim1i ⊢ ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑀 ∈ ℕ ∧ 𝑚 ∈ ℕ ) )
12 11 adantr ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → ( 𝑀 ∈ ℕ ∧ 𝑚 ∈ ℕ ) )
13 nnmulcom ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑀 · 𝑚 ) = ( 𝑚 · 𝑀 ) )
14 12 13 syl ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → ( 𝑀 · 𝑚 ) = ( 𝑚 · 𝑀 ) )
15 simpr ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → ( 𝑚 · 𝑀 ) = 𝑁 )
16 14 15 eqtrd ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → ( 𝑀 · 𝑚 ) = 𝑁 )
17 nnmul2 ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑚 ∈ ℕ ∧ ( 𝑀 · 𝑚 ) = 𝑁 ) → 𝑚 ∈ ( 2 ..^ 𝑁 ) )
18 7 9 16 17 syl3anc ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → 𝑚 ∈ ( 2 ..^ 𝑁 ) )
19 simpr ⊢ ( ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) ∧ 𝑚 ∈ ( 2 ..^ 𝑁 ) ) → 𝑚 ∈ ( 2 ..^ 𝑁 ) )
20 5 adantl ⊢ ( ( ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) ∧ 𝑚 ∈ ( 2 ..^ 𝑁 ) ) ∧ 𝑛 = 𝑚 ) → ( ( 𝑛 · 𝑀 ) = 𝑁 ↔ ( 𝑚 · 𝑀 ) = 𝑁 ) )
21 15 adantr ⊢ ( ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) ∧ 𝑚 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝑚 · 𝑀 ) = 𝑁 )
22 19 20 21 rspcedvd ⊢ ( ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) ∧ 𝑚 ∈ ( 2 ..^ 𝑁 ) ) → ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 )
23 18 22 mpdan ⊢ ( ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑚 · 𝑀 ) = 𝑁 ) → ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 )
24 23 ex ⊢ ( ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑀 ) = 𝑁 → ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )
25 24 rexlimdva ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑀 ) = 𝑁 → ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )
26 6 25 biimtrid ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 → ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )
27 fzossnn ⊢ ( 1 ..^ 𝑁 ) ⊆ ℕ
28 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
29 fzoss1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑁 ) )
30 28 29 mp1i ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ℕ → ( 2 ..^ 𝑁 ) ⊆ ( 1 ..^ 𝑁 ) )
31 id ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ℕ → ( 1 ..^ 𝑁 ) ⊆ ℕ )
32 30 31 sstrd ⊢ ( ( 1 ..^ 𝑁 ) ⊆ ℕ → ( 2 ..^ 𝑁 ) ⊆ ℕ )
33 27 32 ax-mp ⊢ ( 2 ..^ 𝑁 ) ⊆ ℕ
34 ssrexv ⊢ ( ( 2 ..^ 𝑁 ) ⊆ ℕ → ( ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 → ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )
35 33 34 mp1i ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 → ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ) )
36 26 35 impbid ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ( 𝑛 · 𝑀 ) = 𝑁 ↔ ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )
37 3 36 bitrd ⊢ ( ( 𝑀 ∈ ( 2 ..^ 𝑁 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑀 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ( 2 ..^ 𝑁 ) ( 𝑛 · 𝑀 ) = 𝑁 ) )