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 e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( A e. ( 2 ..^ N ) <-> B e. ( 2 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 nnmul2 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B e. ( 2 ..^ N ) )
2 1 a1d 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> ( A e. NN -> B e. ( 2 ..^ N ) ) )
3 2 3exp 
 |-  ( A e. ( 2 ..^ N ) -> ( B e. NN -> ( ( A x. B ) = N -> ( A e. NN -> B e. ( 2 ..^ N ) ) ) ) )
4 3 com14 
 |-  ( A e. NN -> ( B e. NN -> ( ( A x. B ) = N -> ( A e. ( 2 ..^ N ) -> B e. ( 2 ..^ N ) ) ) ) )
5 4 3imp 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( A e. ( 2 ..^ N ) -> B e. ( 2 ..^ N ) ) )
6 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) /\ B e. ( 2 ..^ N ) ) -> B e. ( 2 ..^ N ) )
7 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) /\ B e. ( 2 ..^ N ) ) -> A e. NN )
8 nnmulcom 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) = ( B x. A ) )
9 8 eqcomd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( B x. A ) = ( A x. B ) )
10 9 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( B x. A ) = ( A x. B ) )
11 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( A x. B ) = N )
12 10 11 eqtrd 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( B x. A ) = N )
13 12 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) /\ B e. ( 2 ..^ N ) ) -> ( B x. A ) = N )
14 nnmul2 
 |-  ( ( B e. ( 2 ..^ N ) /\ A e. NN /\ ( B x. A ) = N ) -> A e. ( 2 ..^ N ) )
15 6 7 13 14 syl3anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) /\ B e. ( 2 ..^ N ) ) -> A e. ( 2 ..^ N ) )
16 15 ex 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( B e. ( 2 ..^ N ) -> A e. ( 2 ..^ N ) ) )
17 5 16 impbid 
 |-  ( ( A e. NN /\ B e. NN /\ ( A x. B ) = N ) -> ( A e. ( 2 ..^ N ) <-> B e. ( 2 ..^ N ) ) )