nndivides2

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

		Ref	Expression
	Assertion	nndivides2	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (M ∥ N \leftrightarrow \exists n \in (2 ..^N) n \cdot M = N)$

Proof

Step	Hyp	Ref	Expression
1		elfzo2nn	$⊢ M \in (2 ..^N) \to M \in ℕ$
2		nndivides	$⊢ (M \in ℕ \land N \in ℕ) \to (M ∥ N \leftrightarrow \exists n \in ℕ n \cdot M = N)$
3	1 2	sylan	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (M ∥ N \leftrightarrow \exists n \in ℕ n \cdot M = N)$
4		oveq1	$⊢ n = m \to n \cdot M = m \cdot M$
5	4	eqeq1d	$⊢ n = m \to (n \cdot M = N \leftrightarrow m \cdot M = N)$
6	5	cbvrexvw	$⊢ \exists n \in ℕ n \cdot M = N \leftrightarrow \exists m \in ℕ m \cdot M = N$
7		simplll	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to M \in (2 ..^N)$
8		simpr	$⊢ ((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \to m \in ℕ$
9	8	adantr	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to m \in ℕ$
10	1	adantr	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to M \in ℕ$
11	10	anim1i	$⊢ ((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \to (M \in ℕ \land m \in ℕ)$
12	11	adantr	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to (M \in ℕ \land m \in ℕ)$
13		nnmulcom	$⊢ (M \in ℕ \land m \in ℕ) \to M m = m \cdot M$
14	12 13	syl	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to M m = m \cdot M$
15		simpr	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to m \cdot M = N$
16	14 15	eqtrd	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to M m = N$
17		nnmul2	$⊢ (M \in (2 ..^N) \land m \in ℕ \land M m = N) \to m \in (2 ..^N)$
18	7 9 16 17	syl3anc	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to m \in (2 ..^N)$
19		simpr	$⊢ ((((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \land m \in (2 ..^N)) \to m \in (2 ..^N)$
20	5	adantl	$⊢ (((((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \land m \in (2 ..^N)) \land n = m) \to (n \cdot M = N \leftrightarrow m \cdot M = N)$
21	15	adantr	$⊢ ((((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \land m \in (2 ..^N)) \to m \cdot M = N$
22	19 20 21	rspcedvd	$⊢ ((((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \land m \in (2 ..^N)) \to \exists n \in (2 ..^N) n \cdot M = N$
23	18 22	mpdan	$⊢ (((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \land m \cdot M = N) \to \exists n \in (2 ..^N) n \cdot M = N$
24	23	ex	$⊢ ((M \in (2 ..^N) \land N \in ℕ) \land m \in ℕ) \to (m \cdot M = N \to \exists n \in (2 ..^N) n \cdot M = N)$
25	24	rexlimdva	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (\exists m \in ℕ m \cdot M = N \to \exists n \in (2 ..^N) n \cdot M = N)$
26	6 25	biimtrid	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (\exists n \in ℕ n \cdot M = N \to \exists n \in (2 ..^N) n \cdot M = N)$
27		fzossnn	$⊢ (1 ..^N) \subseteq ℕ$
28		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
29		fzoss1	$⊢ 2 \in ℤ_{\geq 1} \to (2 ..^N) \subseteq (1 ..^N)$
30	28 29	mp1i	$⊢ (1 ..^N) \subseteq ℕ \to (2 ..^N) \subseteq (1 ..^N)$
31		id	$⊢ (1 ..^N) \subseteq ℕ \to (1 ..^N) \subseteq ℕ$
32	30 31	sstrd	$⊢ (1 ..^N) \subseteq ℕ \to (2 ..^N) \subseteq ℕ$
33	27 32	ax-mp	$⊢ (2 ..^N) \subseteq ℕ$
34		ssrexv	$⊢ (2 ..^N) \subseteq ℕ \to (\exists n \in (2 ..^N) n \cdot M = N \to \exists n \in ℕ n \cdot M = N)$
35	33 34	mp1i	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (\exists n \in (2 ..^N) n \cdot M = N \to \exists n \in ℕ n \cdot M = N)$
36	26 35	impbid	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (\exists n \in ℕ n \cdot M = N \leftrightarrow \exists n \in (2 ..^N) n \cdot M = N)$
37	3 36	bitrd	$⊢ (M \in (2 ..^N) \land N \in ℕ) \to (M ∥ N \leftrightarrow \exists n \in (2 ..^N) n \cdot M = N)$

Metamath Proof Explorer

Theorem nndivides2

Proof