Metamath Proof Explorer

Theorem nndivides2

Description: Definition of the divides relation for divisors greater than 1. (Contributed by AV, 5-Apr-2026)

Ref Expression
Assertion nndivides2 
|- ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( M || N <-> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )

Proof

Step Hyp Ref Expression
1 elfzo2nn 
 |-  ( M e. ( 2 ..^ N ) -> M e. NN )
2 nndivides 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )
3 1 2 sylan 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )
4 oveq1 
 |-  ( n = m -> ( n x. M ) = ( m x. M ) )
5 4 eqeq1d 
 |-  ( n = m -> ( ( n x. M ) = N <-> ( m x. M ) = N ) )
6 5 cbvrexvw 
 |-  ( E. n e. NN ( n x. M ) = N <-> E. m e. NN ( m x. M ) = N )
7 simplll 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> M e. ( 2 ..^ N ) )
8 simpr 
 |-  ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) -> m e. NN )
9 8 adantr 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> m e. NN )
10 1 adantr 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> M e. NN )
11 10 anim1i 
 |-  ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) -> ( M e. NN /\ m e. NN ) )
12 11 adantr 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> ( M e. NN /\ m e. NN ) )
13 nnmulcom 
 |-  ( ( M e. NN /\ m e. NN ) -> ( M x. m ) = ( m x. M ) )
14 12 13 syl 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> ( M x. m ) = ( m x. M ) )
15 simpr 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> ( m x. M ) = N )
16 14 15 eqtrd 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> ( M x. m ) = N )
17 nnmul2 
 |-  ( ( M e. ( 2 ..^ N ) /\ m e. NN /\ ( M x. m ) = N ) -> m e. ( 2 ..^ N ) )
18 7 9 16 17 syl3anc 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> m e. ( 2 ..^ N ) )
19 simpr 
 |-  ( ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) /\ m e. ( 2 ..^ N ) ) -> m e. ( 2 ..^ N ) )
20 5 adantl 
 |-  ( ( ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) /\ m e. ( 2 ..^ N ) ) /\ n = m ) -> ( ( n x. M ) = N <-> ( m x. M ) = N ) )
21 15 adantr 
 |-  ( ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) /\ m e. ( 2 ..^ N ) ) -> ( m x. M ) = N )
22 19 20 21 rspcedvd 
 |-  ( ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) /\ m e. ( 2 ..^ N ) ) -> E. n e. ( 2 ..^ N ) ( n x. M ) = N )
23 18 22 mpdan 
 |-  ( ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) /\ ( m x. M ) = N ) -> E. n e. ( 2 ..^ N ) ( n x. M ) = N )
24 23 ex 
 |-  ( ( ( M e. ( 2 ..^ N ) /\ N e. NN ) /\ m e. NN ) -> ( ( m x. M ) = N -> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )
25 24 rexlimdva 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( E. m e. NN ( m x. M ) = N -> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )
26 6 25 biimtrid 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( E. n e. NN ( n x. M ) = N -> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )
27 fzossnn 
 |-  ( 1 ..^ N ) C_ NN
28 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
29 fzoss1 
 |-  ( 2 e. ( ZZ>= ` 1 ) -> ( 2 ..^ N ) C_ ( 1 ..^ N ) )
30 28 29 mp1i 
 |-  ( ( 1 ..^ N ) C_ NN -> ( 2 ..^ N ) C_ ( 1 ..^ N ) )
31 id 
 |-  ( ( 1 ..^ N ) C_ NN -> ( 1 ..^ N ) C_ NN )
32 30 31 sstrd 
 |-  ( ( 1 ..^ N ) C_ NN -> ( 2 ..^ N ) C_ NN )
33 27 32 ax-mp 
 |-  ( 2 ..^ N ) C_ NN
34 ssrexv 
 |-  ( ( 2 ..^ N ) C_ NN -> ( E. n e. ( 2 ..^ N ) ( n x. M ) = N -> E. n e. NN ( n x. M ) = N ) )
35 33 34 mp1i 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( E. n e. ( 2 ..^ N ) ( n x. M ) = N -> E. n e. NN ( n x. M ) = N ) )
36 26 35 impbid 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( E. n e. NN ( n x. M ) = N <-> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )
37 3 36 bitrd 
 |-  ( ( M e. ( 2 ..^ N ) /\ N e. NN ) -> ( M || N <-> E. n e. ( 2 ..^ N ) ( n x. M ) = N ) )