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