Metamath Proof Explorer

Theorem nnmul2b

Description: A factor of a product of integers is at least 2 and less then the product iff the second factor is at least 2 and less then the product. (Contributed by AV, 5-Apr-2026)

		Ref	Expression
	Assertion	nnmul2b	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to (A \in (2 ..^N) \leftrightarrow B \in (2 ..^N))$

Proof

Step	Hyp	Ref	Expression
1		nnmul2	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B \in (2 ..^N)$
2	1	a1d	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to (A \in ℕ \to B \in (2 ..^N))$
3	2	3exp	$⊢ A \in (2 ..^N) \to (B \in ℕ \to (A B = N \to (A \in ℕ \to B \in (2 ..^N))))$
4	3	com14	$⊢ A \in ℕ \to (B \in ℕ \to (A B = N \to (A \in (2 ..^N) \to B \in (2 ..^N))))$
5	4	3imp	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to (A \in (2 ..^N) \to B \in (2 ..^N))$
6		simpr	$⊢ ((A \in ℕ \land B \in ℕ \land A B = N) \land B \in (2 ..^N)) \to B \in (2 ..^N)$
7		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A B = N) \land B \in (2 ..^N)) \to A \in ℕ$
8		nnmulcom	$⊢ (A \in ℕ \land B \in ℕ) \to A B = B A$
9	8	eqcomd	$⊢ (A \in ℕ \land B \in ℕ) \to B A = A B$
10	9	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to B A = A B$
11		simp3	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to A B = N$
12	10 11	eqtrd	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to B A = N$
13	12	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land A B = N) \land B \in (2 ..^N)) \to B A = N$
14		nnmul2	$⊢ (B \in (2 ..^N) \land A \in ℕ \land B A = N) \to A \in (2 ..^N)$
15	6 7 13 14	syl3anc	$⊢ ((A \in ℕ \land B \in ℕ \land A B = N) \land B \in (2 ..^N)) \to A \in (2 ..^N)$
16	15	ex	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to (B \in (2 ..^N) \to A \in (2 ..^N))$
17	5 16	impbid	$⊢ (A \in ℕ \land B \in ℕ \land A B = N) \to (A \in (2 ..^N) \leftrightarrow B \in (2 ..^N))$