Theorem nprmmul3

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

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

Proof

Step	Hyp	Ref	Expression
1		nprmmul2	|- ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) ) )
2		elfzoelz	|- ( a e. ( 2 ..^ N ) -> a e. ZZ )
3	2	zred	|- ( a e. ( 2 ..^ N ) -> a e. RR )
4	3	adantl	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> a e. RR )
5		elfzoelz	|- ( b e. ( 2 ..^ N ) -> b e. ZZ )
6	5	zred	|- ( b e. ( 2 ..^ N ) -> b e. RR )
7		leloe	|- ( ( a e. RR /\ b e. RR ) -> ( a <_ b <-> ( a < b \/ a = b ) ) )
8	4 6 7	syl2an	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( a <_ b <-> ( a < b \/ a = b ) ) )
9	8	anbi1d	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( ( a <_ b /\ N = ( a x. b ) ) <-> ( ( a < b \/ a = b ) /\ N = ( a x. b ) ) ) )
10		andir	|- ( ( ( a < b \/ a = b ) /\ N = ( a x. b ) ) <-> ( ( a < b /\ N = ( a x. b ) ) \/ ( a = b /\ N = ( a x. b ) ) ) )
11	9 10	bitrdi	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ b e. ( 2 ..^ N ) ) -> ( ( a <_ b /\ N = ( a x. b ) ) <-> ( ( a < b /\ N = ( a x. b ) ) \/ ( a = b /\ N = ( a x. b ) ) ) ) )
12	11	rexbidva	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) <-> E. b e. ( 2 ..^ N ) ( ( a < b /\ N = ( a x. b ) ) \/ ( a = b /\ N = ( a x. b ) ) ) ) )
13		r19.43	|- ( E. b e. ( 2 ..^ N ) ( ( a < b /\ N = ( a x. b ) ) \/ ( a = b /\ N = ( a x. b ) ) ) <-> ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) ) )
14		oveq2	|- ( b = a -> ( a x. b ) = ( a x. a ) )
15	14	equcoms	|- ( a = b -> ( a x. b ) = ( a x. a ) )
16	15	adantl	|- ( ( a e. ( 2 ..^ N ) /\ a = b ) -> ( a x. b ) = ( a x. a ) )
17	2	zcnd	|- ( a e. ( 2 ..^ N ) -> a e. CC )
18	17	sqvald	|- ( a e. ( 2 ..^ N ) -> ( a ^ 2 ) = ( a x. a ) )
19	18	adantr	|- ( ( a e. ( 2 ..^ N ) /\ a = b ) -> ( a ^ 2 ) = ( a x. a ) )
20	16 19	eqtr4d	|- ( ( a e. ( 2 ..^ N ) /\ a = b ) -> ( a x. b ) = ( a ^ 2 ) )
21	20	eqeq2d	|- ( ( a e. ( 2 ..^ N ) /\ a = b ) -> ( N = ( a x. b ) <-> N = ( a ^ 2 ) ) )
22	21	biimpd	|- ( ( a e. ( 2 ..^ N ) /\ a = b ) -> ( N = ( a x. b ) -> N = ( a ^ 2 ) ) )
23	22	ex	|- ( a e. ( 2 ..^ N ) -> ( a = b -> ( N = ( a x. b ) -> N = ( a ^ 2 ) ) ) )
24	23	adantl	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( a = b -> ( N = ( a x. b ) -> N = ( a ^ 2 ) ) ) )
25	24	impd	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( ( a = b /\ N = ( a x. b ) ) -> N = ( a ^ 2 ) ) )
26	25	a1d	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( b e. ( 2 ..^ N ) -> ( ( a = b /\ N = ( a x. b ) ) -> N = ( a ^ 2 ) ) ) )
27	26	rexlimdv	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) -> N = ( a ^ 2 ) ) )
28		simplr	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ N = ( a ^ 2 ) ) -> a e. ( 2 ..^ N ) )
29		equequ2	|- ( b = a -> ( a = b <-> a = a ) )
30	14	eqeq2d	|- ( b = a -> ( N = ( a x. b ) <-> N = ( a x. a ) ) )
31	29 30	anbi12d	|- ( b = a -> ( ( a = b /\ N = ( a x. b ) ) <-> ( a = a /\ N = ( a x. a ) ) ) )
32	31	adantl	|- ( ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ N = ( a ^ 2 ) ) /\ b = a ) -> ( ( a = b /\ N = ( a x. b ) ) <-> ( a = a /\ N = ( a x. a ) ) ) )
33	18	eqeq2d	|- ( a e. ( 2 ..^ N ) -> ( N = ( a ^ 2 ) <-> N = ( a x. a ) ) )
34	33	biimpd	|- ( a e. ( 2 ..^ N ) -> ( N = ( a ^ 2 ) -> N = ( a x. a ) ) )
35	34	adantl	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( N = ( a ^ 2 ) -> N = ( a x. a ) ) )
36	35	imp	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ N = ( a ^ 2 ) ) -> N = ( a x. a ) )
37		equid	|- a = a
38	36 37	jctil	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ N = ( a ^ 2 ) ) -> ( a = a /\ N = ( a x. a ) ) )
39	28 32 38	rspcedvd	|- ( ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) /\ N = ( a ^ 2 ) ) -> E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) )
40	39	ex	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( N = ( a ^ 2 ) -> E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) ) )
41	27 40	impbid	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) <-> N = ( a ^ 2 ) ) )
42	41	orbi2d	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. b e. ( 2 ..^ N ) ( a = b /\ N = ( a x. b ) ) ) <-> ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ N = ( a ^ 2 ) ) ) )
43	13 42	bitrid	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( ( a < b /\ N = ( a x. b ) ) \/ ( a = b /\ N = ( a x. b ) ) ) <-> ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ N = ( a ^ 2 ) ) ) )
44	12 43	bitrd	|- ( ( N e. ( ZZ>= ` 4 ) /\ a e. ( 2 ..^ N ) ) -> ( E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) <-> ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ N = ( a ^ 2 ) ) ) )
45	44	rexbidva	|- ( N e. ( ZZ>= ` 4 ) -> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) <-> E. a e. ( 2 ..^ N ) ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ N = ( a ^ 2 ) ) ) )
46		r19.43	|- ( E. a e. ( 2 ..^ N ) ( E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ N = ( a ^ 2 ) ) <-> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) )
47	45 46	bitrdi	|- ( N e. ( ZZ>= ` 4 ) -> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a <_ b /\ N = ( a x. b ) ) <-> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) ) )
48	1 47	bitrd	|- ( N e. ( ZZ>= ` 4 ) -> ( N e/ Prime <-> ( E. a e. ( 2 ..^ N ) E. b e. ( 2 ..^ N ) ( a < b /\ N = ( a x. b ) ) \/ E. a e. ( 2 ..^ N ) N = ( a ^ 2 ) ) ) )