Theorem 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	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn1uz2	⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 = 1 ∨ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) )
2		oveq2	⊢ ( 𝐵 = 1 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 1 ) )
3	2	eqeq1d	⊢ ( 𝐵 = 1 → ( ( 𝐴 · 𝐵 ) = 𝑁 ↔ ( 𝐴 · 1 ) = 𝑁 ) )
4	3	adantr	⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 𝐵 ) = 𝑁 ↔ ( 𝐴 · 1 ) = 𝑁 ) )
5		elfzoelz	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℤ )
6	5	zred	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ℝ )
7		ax-1rid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
8	6 7	syl	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 · 1 ) = 𝐴 )
9	8	eqeq1d	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 1 ) = 𝑁 ↔ 𝐴 = 𝑁 ) )
10		elfzo2	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ↔ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) )
11		breq2	⊢ ( 𝑁 = 𝐴 → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
12	11	eqcoms	⊢ ( 𝐴 = 𝑁 → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
13	12	adantl	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝑁 ↔ 𝐴 < 𝐴 ) )
14		eluzelre	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℝ )
15	14	ltnrd	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ¬ 𝐴 < 𝐴 )
16	15	pm2.21d	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 < 𝐴 → 2 ≤ 𝐵 ) )
17	16	adantr	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝐴 → 2 ≤ 𝐵 ) )
18	13 17	sylbid	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 = 𝑁 ) → ( 𝐴 < 𝑁 → 2 ≤ 𝐵 ) )
19	18	impancom	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 < 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
20	19	3adant2	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
21	10 20	sylbi	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐴 = 𝑁 → 2 ≤ 𝐵 ) )
22	9 21	sylbid	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 1 ) = 𝑁 → 2 ≤ 𝐵 ) )
23	22	adantl	⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 1 ) = 𝑁 → 2 ≤ 𝐵 ) )
24	4 23	sylbid	⊢ ( ( 𝐵 = 1 ∧ 𝐴 ∈ ( 2 ..^ 𝑁 ) ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) )
25	24	ex	⊢ ( 𝐵 = 1 → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
26		eluzle	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝐵 )
27	26	2a1d	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
28	25 27	jaoi	⊢ ( ( 𝐵 = 1 ∨ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
29	1 28	sylbi	⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( ( 𝐴 · 𝐵 ) = 𝑁 → 2 ≤ 𝐵 ) ) )
30	29	3imp21	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 2 ≤ 𝐵 )
31		eluz2gt1	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐴 )
32	31	3ad2ant1	⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℤ ∧ 𝐴 < 𝑁 ) → 1 < 𝐴 )
33	10 32	sylbi	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 1 < 𝐴 )
34	33	3ad2ant1	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 1 < 𝐴 )
35	6	3ad2ant1	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐴 ∈ ℝ )
36		nnrp	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
37	36	3ad2ant2	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ℝ+ )
38	35 37	ltmulgt12d	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 1 < 𝐴 ↔ 𝐵 < ( 𝐴 · 𝐵 ) ) )
39	34 38	mpbid	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 < ( 𝐴 · 𝐵 ) )
40		breq2	⊢ ( ( 𝐴 · 𝐵 ) = 𝑁 → ( 𝐵 < ( 𝐴 · 𝐵 ) ↔ 𝐵 < 𝑁 ) )
41	40	3ad2ant3	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 < ( 𝐴 · 𝐵 ) ↔ 𝐵 < 𝑁 ) )
42	39 41	mpbid	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 < 𝑁 )
43		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
44	43	3ad2ant2	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ℤ )
45		2z	⊢ 2 ∈ ℤ
46	45	a1i	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 2 ∈ ℤ )
47		elfzoel2	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
48	47	3ad2ant1	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝑁 ∈ ℤ )
49		elfzo	⊢ ( ( 𝐵 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐵 ∈ ( 2 ..^ 𝑁 ) ↔ ( 2 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) ) )
50	44 46 48 49	syl3anc	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 ∈ ( 2 ..^ 𝑁 ) ↔ ( 2 ≤ 𝐵 ∧ 𝐵 < 𝑁 ) ) )
51	30 42 50	mpbir2and	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )