nprmmul3

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

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

Proof

Step	Hyp	Ref	Expression
1		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))$
2		elfzoelz	$⊢ a \in (2 ..^N) \to a \in ℤ$
3	2	zred	$⊢ a \in (2 ..^N) \to a \in ℝ$
4	3	adantl	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to a \in ℝ$
5		elfzoelz	$⊢ b \in (2 ..^N) \to b \in ℤ$
6	5	zred	$⊢ b \in (2 ..^N) \to b \in ℝ$
7		leloe	$⊢ (a \in ℝ \land b \in ℝ) \to (a \leq b \leftrightarrow (a < b \lor a = b))$
8	4 6 7	syl2an	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to (a \leq b \leftrightarrow (a < b \lor a = b))$
9	8	anbi1d	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to ((a \leq b \land N = a b) \leftrightarrow ((a < b \lor a = b) \land N = a b))$
10		andir	$⊢ ((a < b \lor a = b) \land N = a b) \leftrightarrow ((a < b \land N = a b) \lor (a = b \land N = a b))$
11	9 10	bitrdi	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land b \in (2 ..^N)) \to ((a \leq b \land N = a b) \leftrightarrow ((a < b \land N = a b) \lor (a = b \land N = a b)))$
12	11	rexbidva	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) (a \leq b \land N = a b) \leftrightarrow \exists b \in (2 ..^N) ((a < b \land N = a b) \lor (a = b \land N = a b)))$
13		r19.43	$⊢ \exists b \in (2 ..^N) ((a < b \land N = a b) \lor (a = b \land N = a b)) \leftrightarrow (\exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists b \in (2 ..^N) (a = b \land N = a b))$
14		oveq2	$⊢ b = a \to a b = a a$
15	14	equcoms	$⊢ a = b \to a b = a a$
16	15	adantl	$⊢ (a \in (2 ..^N) \land a = b) \to a b = a a$
17	2	zcnd	$⊢ a \in (2 ..^N) \to a \in ℂ$
18	17	sqvald	$⊢ a \in (2 ..^N) \to a^{2} = a a$
19	18	adantr	$⊢ (a \in (2 ..^N) \land a = b) \to a^{2} = a a$
20	16 19	eqtr4d	$⊢ (a \in (2 ..^N) \land a = b) \to a b = a^{2}$
21	20	eqeq2d	$⊢ (a \in (2 ..^N) \land a = b) \to (N = a b \leftrightarrow N = a^{2})$
22	21	biimpd	$⊢ (a \in (2 ..^N) \land a = b) \to (N = a b \to N = a^{2})$
23	22	ex	$⊢ a \in (2 ..^N) \to (a = b \to (N = a b \to N = a^{2}))$
24	23	adantl	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (a = b \to (N = a b \to N = a^{2}))$
25	24	impd	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to ((a = b \land N = a b) \to N = a^{2})$
26	25	a1d	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (b \in (2 ..^N) \to ((a = b \land N = a b) \to N = a^{2}))$
27	26	rexlimdv	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) (a = b \land N = a b) \to N = a^{2})$
28		simplr	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land N = a^{2}) \to a \in (2 ..^N)$
29		equequ2	$⊢ b = a \to (a = b \leftrightarrow a = a)$
30	14	eqeq2d	$⊢ b = a \to (N = a b \leftrightarrow N = a a)$
31	29 30	anbi12d	$⊢ b = a \to ((a = b \land N = a b) \leftrightarrow (a = a \land N = a a))$
32	31	adantl	$⊢ (((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land N = a^{2}) \land b = a) \to ((a = b \land N = a b) \leftrightarrow (a = a \land N = a a))$
33	18	eqeq2d	$⊢ a \in (2 ..^N) \to (N = a^{2} \leftrightarrow N = a a)$
34	33	biimpd	$⊢ a \in (2 ..^N) \to (N = a^{2} \to N = a a)$
35	34	adantl	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (N = a^{2} \to N = a a)$
36	35	imp	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land N = a^{2}) \to N = a a$
37		equid	$⊢ a = a$
38	36 37	jctil	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land N = a^{2}) \to (a = a \land N = a a)$
39	28 32 38	rspcedvd	$⊢ ((N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \land N = a^{2}) \to \exists b \in (2 ..^N) (a = b \land N = a b)$
40	39	ex	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (N = a^{2} \to \exists b \in (2 ..^N) (a = b \land N = a b))$
41	27 40	impbid	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) (a = b \land N = a b) \leftrightarrow N = a^{2})$
42	41	orbi2d	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to ((\exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists b \in (2 ..^N) (a = b \land N = a b)) \leftrightarrow (\exists b \in (2 ..^N) (a < b \land N = a b) \lor N = a^{2}))$
43	13 42	bitrid	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) ((a < b \land N = a b) \lor (a = b \land N = a b)) \leftrightarrow (\exists b \in (2 ..^N) (a < b \land N = a b) \lor N = a^{2}))$
44	12 43	bitrd	$⊢ (N \in ℤ_{\geq 4} \land a \in (2 ..^N)) \to (\exists b \in (2 ..^N) (a \leq b \land N = a b) \leftrightarrow (\exists b \in (2 ..^N) (a < b \land N = a b) \lor N = a^{2}))$
45	44	rexbidva	$⊢ N \in ℤ_{\geq 4} \to (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b) \leftrightarrow \exists a \in (2 ..^N) (\exists b \in (2 ..^N) (a < b \land N = a b) \lor N = a^{2}))$
46		r19.43	$⊢ \exists a \in (2 ..^N) (\exists b \in (2 ..^N) (a < b \land N = a b) \lor N = a^{2}) \leftrightarrow (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2})$
47	45 46	bitrdi	$⊢ N \in ℤ_{\geq 4} \to (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a \leq b \land N = a b) \leftrightarrow (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2}))$
48	1 47	bitrd	$⊢ N \in ℤ_{\geq 4} \to (N \notin ℙ \leftrightarrow (\exists a \in (2 ..^N) \exists b \in (2 ..^N) (a < b \land N = a b) \lor \exists a \in (2 ..^N) N = a^{2}))$

Metamath Proof Explorer

Theorem nprmmul3

Proof