This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ ∧ B ∈ ℕ ∧ A ⁢ B = N → A ∈ 2 ..^ N ↔ B ∈ 2 ..^ N

Proof

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