nprmmul1

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

		Ref	Expression
	Assertion	nprmmul1	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow \exists a \in (2 ..^N) \exists b \in (2 ..^N) N = a b)$

Proof

Step	Hyp	Ref	Expression
1		isprm3	$⊢ N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land \forall a \in (2 \dots N - 1) \neg a ∥ N)$
2	1	a1i	$⊢ N \in ℤ_{\geq 4} \to (N \in ℙ \leftrightarrow (N \in ℤ_{\geq 2} \land \forall a \in (2 \dots N - 1) \neg a ∥ N))$
3		uzuzle24	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ_{\geq 2}$
4	3	biantrurd	$⊢ N \in ℤ_{\geq 4} \to (\forall a \in (2 \dots N - 1) \neg a ∥ N \leftrightarrow (N \in ℤ_{\geq 2} \land \forall a \in (2 \dots N - 1) \neg a ∥ N))$
5		eluzelz	$⊢ N \in ℤ_{\geq 4} \to N \in ℤ$
6		fzoval	$⊢ N \in ℤ \to (2 ..^N) = (2 \dots N - 1)$
7	5 6	syl	$⊢ N \in ℤ_{\geq 4} \to (2 ..^N) = (2 \dots N - 1)$
8	7	eqcomd	$⊢ N \in ℤ_{\geq 4} \to (2 \dots N - 1) = (2 ..^N)$
9	8	raleqdv	$⊢ N \in ℤ_{\geq 4} \to (\forall a \in (2 \dots N - 1) \neg a ∥ N \leftrightarrow \forall a \in (2 ..^N) \neg a ∥ N)$
10		eluz4nn	$⊢ N \in ℤ_{\geq 4} \to N \in ℕ$
11	10	anim1ci	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (a \in (2 ..^N) \land N \in ℕ)$
12		nndivides2	$⊢ (a \in (2 ..^N) \land N \in ℕ) \to (a ∥ N \leftrightarrow \exists b \in (2 ..^N) b a = N)$
13	11 12	syl	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (a ∥ N \leftrightarrow \exists b \in (2 ..^N) b a = N)$
14		eqcom	$⊢ b a = N \leftrightarrow N = b a$
15		elfzo2nn	$⊢ b \in (2 ..^N) \to b \in ℕ$
16		elfzo2nn	$⊢ a \in (2 ..^N) \to a \in ℕ$
17	16	adantl	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to a \in ℕ$
18		nnmulcom	$⊢ (b \in ℕ \land a \in ℕ) \to b a = a b$
19	15 17 18	syl2anr	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to b a = a b$
20	19	eqeq2d	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to (N = b a \leftrightarrow N = a b)$
21	14 20	bitrid	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to (b a = N \leftrightarrow N = a b)$
22	21	rexbidva	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) b a = N \leftrightarrow \exists b \in (2 ..^N) N = a b)$
23	13 22	bitrd	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (a ∥ N \leftrightarrow \exists b \in (2 ..^N) N = a b)$
24	23	notbid	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\neg a ∥ N \leftrightarrow \neg \exists b \in (2 ..^N) N = a b)$
25	24	ralbidva	$⊢ N \in ℤ_{\geq 4} \to (\forall a \in (2 ..^N) \neg a ∥ N \leftrightarrow \forall a \in (2 ..^N) \neg \exists b \in (2 ..^N) N = a b)$
26	9 25	bitrd	$⊢ N \in ℤ_{\geq 4} \to (\forall a \in (2 \dots N - 1) \neg a ∥ N \leftrightarrow \forall a \in (2 ..^N) \neg \exists b \in (2 ..^N) N = a b)$
27	2 4 26	3bitr2d	$⊢ N \in ℤ_{\geq 4} \to (N \in ℙ \leftrightarrow \forall a \in (2 ..^N) \neg \exists b \in (2 ..^N) N = a b)$
28		nnel	$⊢ \neg N \notin ℙ \leftrightarrow N \in ℙ$
29		ralnex	$⊢ \forall a \in (2 ..^N) \neg \exists b \in (2 ..^N) N = a b \leftrightarrow \neg \exists a \in (2 ..^N) \exists b \in (2 ..^N) N = a b$
30	29	bicomi	$⊢ \neg \exists a \in (2 ..^N) \exists b \in (2 ..^N) N = a b \leftrightarrow \forall a \in (2 ..^N) \neg \exists b \in (2 ..^N) N = a b$
31	27 28 30	3bitr4g	$⊢ N \in ℤ_{\geq 4} \to (\neg N \notin ℙ \leftrightarrow \neg \exists a \in (2 ..^N) \exists b \in (2 ..^N) N = a b)$
32	31	con4bid	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow \exists a \in (2 ..^N) \exists b \in (2 ..^N) N = a b)$

Metamath Proof Explorer

Theorem nprmmul1

Proof