Metamath Proof Explorer

Theorem nprmmul1

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

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

Proof

Step Hyp Ref Expression
1 isprm3 
 |-  ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. a e. ( 2 ... ( N - 1 ) ) -. a || N ) )
2 1 a1i 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e. Prime <-> ( N e. ( ZZ>= ` 2 ) /\ A. a e. ( 2 ... ( N - 1 ) ) -. a || N ) ) )
3 uzuzle24 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ( ZZ>= ` 2 ) )
4 3 biantrurd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( A. a e. ( 2 ... ( N - 1 ) ) -. a || N <-> ( N e. ( ZZ>= ` 2 ) /\ A. a e. ( 2 ... ( N - 1 ) ) -. a || N ) ) )
5 eluzelz 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. ZZ )
6 fzoval 
 |-  ( N e. ZZ -> ( 2 ..^ N ) = ( 2 ... ( N - 1 ) ) )
7 5 6 syl 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 ..^ N ) = ( 2 ... ( N - 1 ) ) )
8 7 eqcomd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 ... ( N - 1 ) ) = ( 2 ..^ N ) )
9 8 raleqdv 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( A. a e. ( 2 ... ( N - 1 ) ) -. a || N <-> A. a e. ( 2 ..^ N ) -. a || N ) )
10 eluz4nn 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. NN )
11 10 anim1ci 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( a e. ( 2 ..^ N ) /\ N e. NN ) )
12 nndivides2 
 |-  ( ( a e. ( 2 ..^ N ) /\ N e. NN ) -> ( a || N <-> E. b e. ( 2 ..^ N ) ( b x. a ) = N ) )
13 11 12 syl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( a || N <-> E. b e. ( 2 ..^ N ) ( b x. a ) = N ) )
14 eqcom 
 |-  ( ( b x. a ) = N <-> N = ( b x. a ) )
15 elfzo2nn 
 |-  ( b e. ( 2 ..^ N ) -> b e. NN )
16 elfzo2nn 
 |-  ( a e. ( 2 ..^ N ) -> a e. NN )
17 16 adantl 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> a e. NN )
18 nnmulcom 
 |-  ( ( b e. NN /\ a e. NN ) -> ( b x. a ) = ( a x. b ) )
19 15 17 18 syl2anr 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( b x. a ) = ( a x. b ) )
20 19 eqeq2d 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( N = ( b x. a ) <-> N = ( a x. b ) ) )
21 14 20 bitrid 
 |-  ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( ( b x. a ) = N <-> N = ( a x. b ) ) )
22 21 rexbidva 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( b x. a ) = N <-> E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
23 13 22 bitrd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( a || N <-> E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
24 23 notbid 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( -. a || N <-> -. E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
25 24 ralbidva 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( A. a e. ( 2 ..^ N ) -. a || N <-> A. a e. ( 2 ..^ N ) -. E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
26 9 25 bitrd 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( A. a e. ( 2 ... ( N - 1 ) ) -. a || N <-> A. a e. ( 2 ..^ N ) -. E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
27 2 4 26 3bitr2d 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e. Prime <-> A. a e. ( 2 ..^ N ) -. E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
28 nnel 
 |-  ( -. N e/ Prime <-> N e. Prime )
29 ralnex 
 |-  ( A. a e. ( 2 ..^ N ) -. E. b e. ( 2 ..^ N ) N = ( a x. b ) <-> -. E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) N = ( a x. b ) )
30 29 bicomi 
 |-  ( -. E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) N = ( a x. b ) <-> A. a e. ( 2 ..^ N ) -. E. b e. ( 2 ..^ N ) N = ( a x. b ) )
31 27 28 30 3bitr4g 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( -. N e/ Prime <-> -. E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )
32 31 con4bid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) N = ( a x. b ) ) )