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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 elnn1uz2 
 |-  ( B e. NN <-> ( B = 1 \/ B e. ( ZZ>= ` 2 ) ) )
2 oveq2 
 |-  ( B = 1 -> ( A x. B ) = ( A x. 1 ) )
3 2 eqeq1d 
 |-  ( B = 1 -> ( ( A x. B ) = N <-> ( A x. 1 ) = N ) )
4 3 adantr 
 |-  ( ( B = 1 /\ A e. ( 2 ..^ N ) ) -> ( ( A x. B ) = N <-> ( A x. 1 ) = N ) )
5 elfzoelz 
 |-  ( A e. ( 2 ..^ N ) -> A e. ZZ )
6 5 zred 
 |-  ( A e. ( 2 ..^ N ) -> A e. RR )
7 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
8 6 7 syl 
 |-  ( A e. ( 2 ..^ N ) -> ( A x. 1 ) = A )
9 8 eqeq1d 
 |-  ( A e. ( 2 ..^ N ) -> ( ( A x. 1 ) = N <-> A = N ) )
10 elfzo2 
 |-  ( A e. ( 2 ..^ N ) <-> ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ A < N ) )
11 breq2 
 |-  ( N = A -> ( A < N <-> A < A ) )
12 11 eqcoms 
 |-  ( A = N -> ( A < N <-> A < A ) )
13 12 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ A = N ) -> ( A < N <-> A < A ) )
14 eluzelre 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. RR )
15 14 ltnrd 
 |-  ( A e. ( ZZ>= ` 2 ) -> -. A < A )
16 15 pm2.21d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A < A -> 2 <_ B ) )
17 16 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ A = N ) -> ( A < A -> 2 <_ B ) )
18 13 17 sylbid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ A = N ) -> ( A < N -> 2 <_ B ) )
19 18 impancom 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ A < N ) -> ( A = N -> 2 <_ B ) )
20 19 3adant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ A < N ) -> ( A = N -> 2 <_ B ) )
21 10 20 sylbi 
 |-  ( A e. ( 2 ..^ N ) -> ( A = N -> 2 <_ B ) )
22 9 21 sylbid 
 |-  ( A e. ( 2 ..^ N ) -> ( ( A x. 1 ) = N -> 2 <_ B ) )
23 22 adantl 
 |-  ( ( B = 1 /\ A e. ( 2 ..^ N ) ) -> ( ( A x. 1 ) = N -> 2 <_ B ) )
24 4 23 sylbid 
 |-  ( ( B = 1 /\ A e. ( 2 ..^ N ) ) -> ( ( A x. B ) = N -> 2 <_ B ) )
25 24 ex 
 |-  ( B = 1 -> ( A e. ( 2 ..^ N ) -> ( ( A x. B ) = N -> 2 <_ B ) ) )
26 eluzle 
 |-  ( B e. ( ZZ>= ` 2 ) -> 2 <_ B )
27 26 2a1d 
 |-  ( B e. ( ZZ>= ` 2 ) -> ( A e. ( 2 ..^ N ) -> ( ( A x. B ) = N -> 2 <_ B ) ) )
28 25 27 jaoi 
 |-  ( ( B = 1 \/ B e. ( ZZ>= ` 2 ) ) -> ( A e. ( 2 ..^ N ) -> ( ( A x. B ) = N -> 2 <_ B ) ) )
29 1 28 sylbi 
 |-  ( B e. NN -> ( A e. ( 2 ..^ N ) -> ( ( A x. B ) = N -> 2 <_ B ) ) )
30 29 3imp21 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> 2 <_ B )
31 eluz2gt1 
 |-  ( A e. ( ZZ>= ` 2 ) -> 1 < A )
32 31 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ A < N ) -> 1 < A )
33 10 32 sylbi 
 |-  ( A e. ( 2 ..^ N ) -> 1 < A )
34 33 3ad2ant1 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> 1 < A )
35 6 3ad2ant1 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> A e. RR )
36 nnrp 
 |-  ( B e. NN -> B e. RR+ )
37 36 3ad2ant2 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B e. RR+ )
38 35 37 ltmulgt12d 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> ( 1 < A <-> B < ( A x. B ) ) )
39 34 38 mpbid 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B < ( A x. B ) )
40 breq2 
 |-  ( ( A x. B ) = N -> ( B < ( A x. B ) <-> B < N ) )
41 40 3ad2ant3 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> ( B < ( A x. B ) <-> B < N ) )
42 39 41 mpbid 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B < N )
43 nnz 
 |-  ( B e. NN -> B e. ZZ )
44 43 3ad2ant2 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B e. ZZ )
45 2z 
 |-  2 e. ZZ
46 45 a1i 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> 2 e. ZZ )
47 elfzoel2 
 |-  ( A e. ( 2 ..^ N ) -> N e. ZZ )
48 47 3ad2ant1 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> N e. ZZ )
49 elfzo 
 |-  ( ( B e. ZZ /\ 2 e. ZZ /\ N e. ZZ ) -> ( B e. ( 2 ..^ N ) <-> ( 2 <_ B /\ B < N ) ) )
50 44 46 48 49 syl3anc 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> ( B e. ( 2 ..^ N ) <-> ( 2 <_ B /\ B < N ) ) )
51 30 42 50 mpbir2and 
 |-  ( ( A e. ( 2 ..^ N ) /\ B e. NN /\ ( A x. B ) = N ) -> B e. ( 2 ..^ N ) )