Metamath Proof Explorer

Theorem nprmmul2

Description: Special factorization of a non-prime integer greater than 3. (Contributed by AV, 6-Apr-2026)

Ref Expression
Assertion nprmmul2 
|- ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )

Proof

Step Hyp Ref Expression
1 nprmmul1 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) ) )
2 breq1 
 |-  ( a = n -> ( a <_ b <-> n <_ b ) )
3 oveq1 
 |-  ( a = n -> ( a x. b ) = ( n x. b ) )
4 3 eqeq2d 
 |-  ( a = n -> ( N = ( a x. b ) <-> N = ( n x. b ) ) )
5 2 4 anbi12d 
 |-  ( a = n -> ( ( a <_ b /\ N = ( a x. b ) ) <-> ( n <_ b /\ N = ( n x. b ) ) ) )
6 breq2 
 |-  ( b = m -> ( n <_ b <-> n <_ m ) )
7 oveq2 
 |-  ( b = m -> ( n x. b ) = ( n x. m ) )
8 7 eqeq2d 
 |-  ( b = m -> ( N = ( n x. b ) <-> N = ( n x. m ) ) )
9 6 8 anbi12d 
 |-  ( b = m -> ( ( n <_ b /\ N = ( n x. b ) ) <-> ( n <_ m /\ N = ( n x. m ) ) ) )
10 simp1rr 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> n e. ( 2 ..^ N ) )
11 simp1rl 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> m e. ( 2 ..^ N ) )
12 simp2 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> n <_ m )
13 elfzo2nn 
 |-  ( m e. ( 2 ..^ N ) -> m e. NN )
14 elfzo2nn 
 |-  ( n e. ( 2 ..^ N ) -> n e. NN )
15 nnmulcom 
 |-  ( ( m e. NN /\ n e. NN ) -> ( m x. n ) = ( n x. m ) )
16 13 14 15 syl2an 
 |-  ( ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) -> ( m x. n ) = ( n x. m ) )
17 16 eqeq2d 
 |-  ( ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) -> ( N = ( m x. n ) <-> N = ( n x. m ) ) )
18 17 biimpd 
 |-  ( ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) -> ( N = ( m x. n ) -> N = ( n x. m ) ) )
19 18 adantl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( N = ( m x. n ) -> N = ( n x. m ) ) )
20 19 imp 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ N = ( m x. n ) ) -> N = ( n x. m ) )
21 20 3adant2 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> N = ( n x. m ) )
22 12 21 jca 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> ( n <_ m /\ N = ( n x. m ) ) )
23 5 9 10 11 22 2rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ n <_ m /\ N = ( m x. n ) ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) )
24 23 3exp 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( n <_ m -> ( N = ( m x. n ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) ) )
25 breq1 
 |-  ( a = m -> ( a <_ b <-> m <_ b ) )
26 oveq1 
 |-  ( a = m -> ( a x. b ) = ( m x. b ) )
27 26 eqeq2d 
 |-  ( a = m -> ( N = ( a x. b ) <-> N = ( m x. b ) ) )
28 25 27 anbi12d 
 |-  ( a = m -> ( ( a <_ b /\ N = ( a x. b ) ) <-> ( m <_ b /\ N = ( m x. b ) ) ) )
29 breq2 
 |-  ( b = n -> ( m <_ b <-> m <_ n ) )
30 oveq2 
 |-  ( b = n -> ( m x. b ) = ( m x. n ) )
31 30 eqeq2d 
 |-  ( b = n -> ( N = ( m x. b ) <-> N = ( m x. n ) ) )
32 29 31 anbi12d 
 |-  ( b = n -> ( ( m <_ b /\ N = ( m x. b ) ) <-> ( m <_ n /\ N = ( m x. n ) ) ) )
33 simp1rl 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ m <_ n /\ N = ( m x. n ) ) -> m e. ( 2 ..^ N ) )
34 simp1rr 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ m <_ n /\ N = ( m x. n ) ) -> n e. ( 2 ..^ N ) )
35 3simpc 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ m <_ n /\ N = ( m x. n ) ) -> ( m <_ n /\ N = ( m x. n ) ) )
36 28 32 33 34 35 2rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) /\ m <_ n /\ N = ( m x. n ) ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) )
37 36 3exp 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( m <_ n -> ( N = ( m x. n ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) ) )
38 elfzoelz 
 |-  ( m e. ( 2 ..^ N ) -> m e. ZZ )
39 38 zred 
 |-  ( m e. ( 2 ..^ N ) -> m e. RR )
40 elfzoelz 
 |-  ( n e. ( 2 ..^ N ) -> n e. ZZ )
41 40 zred 
 |-  ( n e. ( 2 ..^ N ) -> n e. RR )
42 39 41 anim12ci 
 |-  ( ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) -> ( n e. RR /\ m e. RR ) )
43 42 adantl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( n e. RR /\ m e. RR ) )
44 letric 
 |-  ( ( n e. RR /\ m e. RR ) -> ( n <_ m \/ m <_ n ) )
45 43 44 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( n <_ m \/ m <_ n ) )
46 24 37 45 mpjaod 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( m e. ( 2 ..^ N ) /\ n e. ( 2 ..^ N ) ) ) -> ( N = ( m x. n ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )
47 46 rexlimdvva 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) -> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )
48 oveq1 
 |-  ( m = a -> ( m x. n ) = ( a x. n ) )
49 48 eqeq2d 
 |-  ( m = a -> ( N = ( m x. n ) <-> N = ( a x. n ) ) )
50 oveq2 
 |-  ( n = b -> ( a x. n ) = ( a x. b ) )
51 50 eqeq2d 
 |-  ( n = b -> ( N = ( a x. n ) <-> N = ( a x. b ) ) )
52 simplrl 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ N = ( a x. b ) ) -> a e. ( 2 ..^ N ) )
53 simplrr 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ N = ( a x. b ) ) -> b e. ( 2 ..^ N ) )
54 simpr 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ N = ( a x. b ) ) -> N = ( a x. b ) )
55 49 51 52 53 54 2rspcedvdw 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) /\ N = ( a x. b ) ) -> E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) )
56 55 ex 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> ( N = ( a x. b ) -> E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) ) )
57 56 adantld 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ ( a e. ( 2 ..^ N ) /\ b e. ( 2 ..^ N ) ) ) -> ( ( a <_ b /\ N = ( a x. b ) ) -> E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) ) )
58 57 rexlimdvva 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) -> E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) ) )
59 47 58 impbid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( E. m e. ( 2 ..^ N ) E. n e. ( 2 ..^ N ) N = ( m x. n ) <-> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )
60 1 59 bitrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )