nprmmul2

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

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

Proof

Step	Hyp	Ref	Expression
1		nprmmul1	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow \exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n)$
2		breq1	$⊢ a = n \to (a \leq b \leftrightarrow n \leq b)$
3		oveq1	$⊢ a = n \to a b = n b$
4	3	eqeq2d	$⊢ a = n \to (N = a b \leftrightarrow N = n b)$
5	2 4	anbi12d	$⊢ a = n \to ((a \leq b \land N = a b) \leftrightarrow (n \leq b \land N = n b))$
6		breq2	$⊢ b = m \to (n \leq b \leftrightarrow n \leq m)$
7		oveq2	$⊢ b = m \to n b = n m$
8	7	eqeq2d	$⊢ b = m \to (N = n b \leftrightarrow N = n m)$
9	6 8	anbi12d	$⊢ b = m \to ((n \leq b \land N = n b) \leftrightarrow (n \leq m \land N = n m))$
10		simp1rr	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to n \in (2 ..^N)$
11		simp1rl	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to m \in (2 ..^N)$
12		simp2	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to n \leq m$
13		elfzo2nn	$⊢ m \in (2 ..^N) \to m \in ℕ$
14		elfzo2nn	$⊢ n \in (2 ..^N) \to n \in ℕ$
15		nnmulcom	$⊢ (m \in ℕ \land n \in ℕ) \to m n = n m$
16	13 14 15	syl2an	$⊢ (m \in (2 ..^N) \land n \in (2 ..^N)) \to m n = n m$
17	16	eqeq2d	$⊢ (m \in (2 ..^N) \land n \in (2 ..^N)) \to (N = m n \leftrightarrow N = n m)$
18	17	biimpd	$⊢ (m \in (2 ..^N) \land n \in (2 ..^N)) \to (N = m n \to N = n m)$
19	18	adantl	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (N = m n \to N = n m)$
20	19	imp	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land N = m n) \to N = n m$
21	20	3adant2	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to N = n m$
22	12 21	jca	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to (n \leq m \land N = n m)$
23	5 9 10 11 22	2rspcedvdw	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land n \leq m \land N = m n) \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b)$
24	23	3exp	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (n \leq m \to (N = m n \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b)))$
25		breq1	$⊢ a = m \to (a \leq b \leftrightarrow m \leq b)$
26		oveq1	$⊢ a = m \to a b = m b$
27	26	eqeq2d	$⊢ a = m \to (N = a b \leftrightarrow N = m b)$
28	25 27	anbi12d	$⊢ a = m \to ((a \leq b \land N = a b) \leftrightarrow (m \leq b \land N = m b))$
29		breq2	$⊢ b = n \to (m \leq b \leftrightarrow m \leq n)$
30		oveq2	$⊢ b = n \to m b = m n$
31	30	eqeq2d	$⊢ b = n \to (N = m b \leftrightarrow N = m n)$
32	29 31	anbi12d	$⊢ b = n \to ((m \leq b \land N = m b) \leftrightarrow (m \leq n \land N = m n))$
33		simp1rl	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land m \leq n \land N = m n) \to m \in (2 ..^N)$
34		simp1rr	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land m \leq n \land N = m n) \to n \in (2 ..^N)$
35		3simpc	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land m \leq n \land N = m n) \to (m \leq n \land N = m n)$
36	28 32 33 34 35	2rspcedvdw	$⊢ ((N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \land m \leq n \land N = m n) \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b)$
37	36	3exp	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (m \leq n \to (N = m n \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b)))$
38		elfzoelz	$⊢ m \in (2 ..^N) \to m \in ℤ$
39	38	zred	$⊢ m \in (2 ..^N) \to m \in ℝ$
40		elfzoelz	$⊢ n \in (2 ..^N) \to n \in ℤ$
41	40	zred	$⊢ n \in (2 ..^N) \to n \in ℝ$
42	39 41	anim12ci	$⊢ (m \in (2 ..^N) \land n \in (2 ..^N)) \to (n \in ℝ \land m \in ℝ)$
43	42	adantl	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (n \in ℝ \land m \in ℝ)$
44		letric	$⊢ (n \in ℝ \land m \in ℝ) \to (n \leq m \lor m \leq n)$
45	43 44	syl	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (n \leq m \lor m \leq n)$
46	24 37 45	mpjaod	$⊢ (N \in ℤ_{\geq 4} \land (m \in (2 ..^N) \land n \in (2 ..^N))) \to (N = m n \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b))$
47	46	rexlimdvva	$⊢ N \in ℤ_{\geq 4} \to (\exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n \to \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b))$
48		oveq1	$⊢ m = a \to m n = a n$
49	48	eqeq2d	$⊢ m = a \to (N = m n \leftrightarrow N = a n)$
50		oveq2	$⊢ n = b \to a n = a b$
51	50	eqeq2d	$⊢ n = b \to (N = a n \leftrightarrow N = a b)$
52		simplrl	$⊢ ((N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land N = a b) \to a \in (2 ..^N)$
53		simplrr	$⊢ ((N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land N = a b) \to b \in (2 ..^N)$
54		simpr	$⊢ ((N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land N = a b) \to N = a b$
55	49 51 52 53 54	2rspcedvdw	$⊢ ((N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \land N = a b) \to \exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n$
56	55	ex	$⊢ (N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to (N = a b \to \exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n)$
57	56	adantld	$⊢ (N \in ℤ_{\geq 4} \land (a \in (2 ..^N) \land b \in (2 ..^N))) \to ((a \leq b \land N = a b) \to \exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n)$
58	57	rexlimdvva	$⊢ N \in ℤ_{\geq 4} \to (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b) \to \exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n)$
59	47 58	impbid	$⊢ N \in ℤ_{\geq 4} \to (\exists m \in (2 ..^N) \exists n \in (2 ..^N) N = m n \leftrightarrow \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b))$
60	1 59	bitrd	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow \exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b))$

Metamath Proof Explorer

Theorem nprmmul2

Proof