nnmul2

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

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

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	$⊢ B \in ℕ \leftrightarrow (B = 1 \lor B \in ℤ_{\geq 2})$
2		oveq2	$⊢ B = 1 \to A B = A \cdot 1$
3	2	eqeq1d	$⊢ B = 1 \to (A B = N \leftrightarrow A \cdot 1 = N)$
4	3	adantr	$⊢ (B = 1 \land A \in (2 ..^N)) \to (A B = N \leftrightarrow A \cdot 1 = N)$
5		elfzoelz	$⊢ A \in (2 ..^N) \to A \in ℤ$
6	5	zred	$⊢ A \in (2 ..^N) \to A \in ℝ$
7		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
8	6 7	syl	$⊢ A \in (2 ..^N) \to A \cdot 1 = A$
9	8	eqeq1d	$⊢ A \in (2 ..^N) \to (A \cdot 1 = N \leftrightarrow A = N)$
10		elfzo2	$⊢ A \in (2 ..^N) \leftrightarrow (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N)$
11		breq2	$⊢ N = A \to (A < N \leftrightarrow A < A)$
12	11	eqcoms	$⊢ A = N \to (A < N \leftrightarrow A < A)$
13	12	adantl	$⊢ (A \in ℤ_{\geq 2} \land A = N) \to (A < N \leftrightarrow A < A)$
14		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
15	14	ltnrd	$⊢ A \in ℤ_{\geq 2} \to \neg A < A$
16	15	pm2.21d	$⊢ A \in ℤ_{\geq 2} \to (A < A \to 2 \leq B)$
17	16	adantr	$⊢ (A \in ℤ_{\geq 2} \land A = N) \to (A < A \to 2 \leq B)$
18	13 17	sylbid	$⊢ (A \in ℤ_{\geq 2} \land A = N) \to (A < N \to 2 \leq B)$
19	18	impancom	$⊢ (A \in ℤ_{\geq 2} \land A < N) \to (A = N \to 2 \leq B)$
20	19	3adant2	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to (A = N \to 2 \leq B)$
21	10 20	sylbi	$⊢ A \in (2 ..^N) \to (A = N \to 2 \leq B)$
22	9 21	sylbid	$⊢ A \in (2 ..^N) \to (A \cdot 1 = N \to 2 \leq B)$
23	22	adantl	$⊢ (B = 1 \land A \in (2 ..^N)) \to (A \cdot 1 = N \to 2 \leq B)$
24	4 23	sylbid	$⊢ (B = 1 \land A \in (2 ..^N)) \to (A B = N \to 2 \leq B)$
25	24	ex	$⊢ B = 1 \to (A \in (2 ..^N) \to (A B = N \to 2 \leq B))$
26		eluzle	$⊢ B \in ℤ_{\geq 2} \to 2 \leq B$
27	26	2a1d	$⊢ B \in ℤ_{\geq 2} \to (A \in (2 ..^N) \to (A B = N \to 2 \leq B))$
28	25 27	jaoi	$⊢ (B = 1 \lor B \in ℤ_{\geq 2}) \to (A \in (2 ..^N) \to (A B = N \to 2 \leq B))$
29	1 28	sylbi	$⊢ B \in ℕ \to (A \in (2 ..^N) \to (A B = N \to 2 \leq B))$
30	29	3imp21	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to 2 \leq B$
31		eluz2gt1	$⊢ A \in ℤ_{\geq 2} \to 1 < A$
32	31	3ad2ant1	$⊢ (A \in ℤ_{\geq 2} \land N \in ℤ \land A < N) \to 1 < A$
33	10 32	sylbi	$⊢ A \in (2 ..^N) \to 1 < A$
34	33	3ad2ant1	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to 1 < A$
35	6	3ad2ant1	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to A \in ℝ$
36		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
37	36	3ad2ant2	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B \in ℝ^{+}$
38	35 37	ltmulgt12d	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to (1 < A \leftrightarrow B < A B)$
39	34 38	mpbid	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B < A B$
40		breq2	$⊢ A B = N \to (B < A B \leftrightarrow B < N)$
41	40	3ad2ant3	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to (B < A B \leftrightarrow B < N)$
42	39 41	mpbid	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B < N$
43		nnz	$⊢ B \in ℕ \to B \in ℤ$
44	43	3ad2ant2	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B \in ℤ$
45		2z	$⊢ 2 \in ℤ$
46	45	a1i	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to 2 \in ℤ$
47		elfzoel2	$⊢ A \in (2 ..^N) \to N \in ℤ$
48	47	3ad2ant1	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to N \in ℤ$
49		elfzo	$⊢ (B \in ℤ \land 2 \in ℤ \land N \in ℤ) \to (B \in (2 ..^N) \leftrightarrow (2 \leq B \land B < N))$
50	44 46 48 49	syl3anc	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to (B \in (2 ..^N) \leftrightarrow (2 \leq B \land B < N))$
51	30 42 50	mpbir2and	$⊢ (A \in (2 ..^N) \land B \in ℕ \land A B = N) \to B \in (2 ..^N)$

Metamath Proof Explorer

Theorem nnmul2

Proof