Metamath Proof Explorer

Theorem dvdsnprmd

Description: If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021)

Ref Expression
Hypotheses dvdsnprmd.g 
|- ( ph -> 1 < A )
dvdsnprmd.l 
|- ( ph -> A < N )
dvdsnprmd.d 
|- ( ph -> A || N )
Assertion dvdsnprmd 
|- ( ph -> -. N e. Prime )

Proof

Step Hyp Ref Expression
1 dvdsnprmd.g 
 |-  ( ph -> 1 < A )
2 dvdsnprmd.l 
 |-  ( ph -> A < N )
3 dvdsnprmd.d 
 |-  ( ph -> A || N )
4 dvdszrcl 
 |-  ( A || N -> ( A e. ZZ /\ N e. ZZ ) )
5 divides 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A || N <-> E. k e. ZZ ( k x. A ) = N ) )
6 3 4 5 3syl 
 |-  ( ph -> ( A || N <-> E. k e. ZZ ( k x. A ) = N ) )
7 2z 
 |-  2 e. ZZ
8 7 a1i 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> 2 e. ZZ )
9 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> k e. ZZ )
10 2 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> A < N )
11 10 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> A < N )
12 breq2 
 |-  ( ( k x. A ) = N -> ( A < ( k x. A ) <-> A < N ) )
13 12 adantl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( A < ( k x. A ) <-> A < N ) )
14 11 13 mpbird 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> A < ( k x. A ) )
15 zre 
 |-  ( A e. ZZ -> A e. RR )
16 15 3ad2ant1 
 |-  ( ( A e. ZZ /\ 1 < A /\ k e. ZZ ) -> A e. RR )
17 zre 
 |-  ( k e. ZZ -> k e. RR )
18 17 3ad2ant3 
 |-  ( ( A e. ZZ /\ 1 < A /\ k e. ZZ ) -> k e. RR )
19 0lt1 
 |-  0 < 1
20 0red 
 |-  ( A e. ZZ -> 0 e. RR )
21 1red 
 |-  ( A e. ZZ -> 1 e. RR )
22 lttr 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
23 20 21 15 22 syl3anc 
 |-  ( A e. ZZ -> ( ( 0 < 1 /\ 1 < A ) -> 0 < A ) )
24 19 23 mpani 
 |-  ( A e. ZZ -> ( 1 < A -> 0 < A ) )
25 24 imp 
 |-  ( ( A e. ZZ /\ 1 < A ) -> 0 < A )
26 25 3adant3 
 |-  ( ( A e. ZZ /\ 1 < A /\ k e. ZZ ) -> 0 < A )
27 16 18 26 3jca 
 |-  ( ( A e. ZZ /\ 1 < A /\ k e. ZZ ) -> ( A e. RR /\ k e. RR /\ 0 < A ) )
28 27 3exp 
 |-  ( A e. ZZ -> ( 1 < A -> ( k e. ZZ -> ( A e. RR /\ k e. RR /\ 0 < A ) ) ) )
29 28 adantr 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( 1 < A -> ( k e. ZZ -> ( A e. RR /\ k e. RR /\ 0 < A ) ) ) )
30 3 4 29 3syl 
 |-  ( ph -> ( 1 < A -> ( k e. ZZ -> ( A e. RR /\ k e. RR /\ 0 < A ) ) ) )
31 1 30 mpd 
 |-  ( ph -> ( k e. ZZ -> ( A e. RR /\ k e. RR /\ 0 < A ) ) )
32 31 imp 
 |-  ( ( ph /\ k e. ZZ ) -> ( A e. RR /\ k e. RR /\ 0 < A ) )
33 32 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( A e. RR /\ k e. RR /\ 0 < A ) )
34 ltmulgt12 
 |-  ( ( A e. RR /\ k e. RR /\ 0 < A ) -> ( 1 < k <-> A < ( k x. A ) ) )
35 33 34 syl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( 1 < k <-> A < ( k x. A ) ) )
36 14 35 mpbird 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> 1 < k )
37 df-2 
 |-  2 = ( 1 + 1 )
38 37 breq1i 
 |-  ( 2 <_ k <-> ( 1 + 1 ) <_ k )
39 1zzd 
 |-  ( k e. ZZ -> 1 e. ZZ )
40 zltp1le 
 |-  ( ( 1 e. ZZ /\ k e. ZZ ) -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
41 39 40 mpancom 
 |-  ( k e. ZZ -> ( 1 < k <-> ( 1 + 1 ) <_ k ) )
42 41 bicomd 
 |-  ( k e. ZZ -> ( ( 1 + 1 ) <_ k <-> 1 < k ) )
43 42 adantl 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( 1 + 1 ) <_ k <-> 1 < k ) )
44 43 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( ( 1 + 1 ) <_ k <-> 1 < k ) )
45 38 44 syl5bb 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( 2 <_ k <-> 1 < k ) )
46 36 45 mpbird 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> 2 <_ k )
47 eluz2 
 |-  ( k e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ k e. ZZ /\ 2 <_ k ) )
48 8 9 46 47 syl3anbrc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> k e. ( ZZ>= ` 2 ) )
49 7 a1i 
 |-  ( ( A e. ZZ /\ 1 < A ) -> 2 e. ZZ )
50 simpl 
 |-  ( ( A e. ZZ /\ 1 < A ) -> A e. ZZ )
51 1zzd 
 |-  ( A e. ZZ -> 1 e. ZZ )
52 zltp1le 
 |-  ( ( 1 e. ZZ /\ A e. ZZ ) -> ( 1 < A <-> ( 1 + 1 ) <_ A ) )
53 51 52 mpancom 
 |-  ( A e. ZZ -> ( 1 < A <-> ( 1 + 1 ) <_ A ) )
54 53 biimpa 
 |-  ( ( A e. ZZ /\ 1 < A ) -> ( 1 + 1 ) <_ A )
55 37 breq1i 
 |-  ( 2 <_ A <-> ( 1 + 1 ) <_ A )
56 54 55 sylibr 
 |-  ( ( A e. ZZ /\ 1 < A ) -> 2 <_ A )
57 49 50 56 3jca 
 |-  ( ( A e. ZZ /\ 1 < A ) -> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) )
58 57 ex 
 |-  ( A e. ZZ -> ( 1 < A -> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) ) )
59 58 adantr 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( 1 < A -> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) ) )
60 3 4 59 3syl 
 |-  ( ph -> ( 1 < A -> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) ) )
61 1 60 mpd 
 |-  ( ph -> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) )
62 eluz2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) )
63 61 62 sylibr 
 |-  ( ph -> A e. ( ZZ>= ` 2 ) )
64 63 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> A e. ( ZZ>= ` 2 ) )
65 64 adantr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> A e. ( ZZ>= ` 2 ) )
66 nprm 
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ A e. ( ZZ>= ` 2 ) ) -> -. ( k x. A ) e. Prime )
67 48 65 66 syl2anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> -. ( k x. A ) e. Prime )
68 eleq1 
 |-  ( ( k x. A ) = N -> ( ( k x. A ) e. Prime <-> N e. Prime ) )
69 68 notbid 
 |-  ( ( k x. A ) = N -> ( -. ( k x. A ) e. Prime <-> -. N e. Prime ) )
70 69 adantl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> ( -. ( k x. A ) e. Prime <-> -. N e. Prime ) )
71 67 70 mpbid 
 |-  ( ( ( ph /\ k e. ZZ ) /\ ( k x. A ) = N ) -> -. N e. Prime )
72 71 rexlimdva2 
 |-  ( ph -> ( E. k e. ZZ ( k x. A ) = N -> -. N e. Prime ) )
73 6 72 sylbid 
 |-  ( ph -> ( A || N -> -. N e. Prime ) )
74 3 73 mpd 
 |-  ( ph -> -. N e. Prime )