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

Proof

Step	Hyp	Ref	Expression
1		nnmul2	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )
2	1	a1d	⊢ ( ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐴 ∈ ℕ → 𝐵 ∈ ( 2 ..^ 𝑁 ) ) )
3	2	3exp	⊢ ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → ( 𝐵 ∈ ℕ → ( ( 𝐴 · 𝐵 ) = 𝑁 → ( 𝐴 ∈ ℕ → 𝐵 ∈ ( 2 ..^ 𝑁 ) ) ) ) )
4	3	com14	⊢ ( 𝐴 ∈ ℕ → ( 𝐵 ∈ ℕ → ( ( 𝐴 · 𝐵 ) = 𝑁 → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) ) ) ) )
5	4	3imp	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) ) )
6		simpr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) ∧ 𝐵 ∈ ( 2 ..^ 𝑁 ) ) → 𝐵 ∈ ( 2 ..^ 𝑁 ) )
7		simpl1	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) ∧ 𝐵 ∈ ( 2 ..^ 𝑁 ) ) → 𝐴 ∈ ℕ )
8		nnmulcom	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
9	8	eqcomd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
10	9	3adant3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) )
11		simp3	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐴 · 𝐵 ) = 𝑁 )
12	10 11	eqtrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 · 𝐴 ) = 𝑁 )
13	12	adantr	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) ∧ 𝐵 ∈ ( 2 ..^ 𝑁 ) ) → ( 𝐵 · 𝐴 ) = 𝑁 )
14		nnmul2	⊢ ( ( 𝐵 ∈ ( 2 ..^ 𝑁 ) ∧ 𝐴 ∈ ℕ ∧ ( 𝐵 · 𝐴 ) = 𝑁 ) → 𝐴 ∈ ( 2 ..^ 𝑁 ) )
15	6 7 13 14	syl3anc	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) ∧ 𝐵 ∈ ( 2 ..^ 𝑁 ) ) → 𝐴 ∈ ( 2 ..^ 𝑁 ) )
16	15	ex	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐵 ∈ ( 2 ..^ 𝑁 ) → 𝐴 ∈ ( 2 ..^ 𝑁 ) ) )
17	5 16	impbid	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = 𝑁 ) → ( 𝐴 ∈ ( 2 ..^ 𝑁 ) ↔ 𝐵 ∈ ( 2 ..^ 𝑁 ) ) )