Metamath Proof Explorer

Theorem ncoprmlnprm

Description: If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020)

Ref Expression
Assertion ncoprmlnprm 
|- ( ( A e. NN /\ B e. NN /\ A < B ) -> ( 1 < ( A gcd B ) -> B e/ Prime ) )

Proof

Step Hyp Ref Expression
1 ncoprmgcdgt1b 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) <-> 1 < ( A gcd B ) ) )
2 1 bicomd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( 1 < ( A gcd B ) <-> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) ) )
3 2 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( 1 < ( A gcd B ) <-> E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) ) )
4 simp1 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> A e. NN )
5 eluzelz 
 |-  ( i e. ( ZZ>= ` 2 ) -> i e. ZZ )
6 4 5 anim12ci 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i e. ZZ /\ A e. NN ) )
7 dvdsle 
 |-  ( ( i e. ZZ /\ A e. NN ) -> ( i || A -> i <_ A ) )
8 6 7 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i || A -> i <_ A ) )
9 nnre 
 |-  ( A e. NN -> A e. RR )
10 nnre 
 |-  ( B e. NN -> B e. RR )
11 eluzelre 
 |-  ( i e. ( ZZ>= ` 2 ) -> i e. RR )
12 9 10 11 3anim123i 
 |-  ( ( A e. NN /\ B e. NN /\ i e. ( ZZ>= ` 2 ) ) -> ( A e. RR /\ B e. RR /\ i e. RR ) )
13 3anrot 
 |-  ( ( i e. RR /\ A e. RR /\ B e. RR ) <-> ( A e. RR /\ B e. RR /\ i e. RR ) )
14 12 13 sylibr 
 |-  ( ( A e. NN /\ B e. NN /\ i e. ( ZZ>= ` 2 ) ) -> ( i e. RR /\ A e. RR /\ B e. RR ) )
15 lelttr 
 |-  ( ( i e. RR /\ A e. RR /\ B e. RR ) -> ( ( i <_ A /\ A < B ) -> i < B ) )
16 14 15 syl 
 |-  ( ( A e. NN /\ B e. NN /\ i e. ( ZZ>= ` 2 ) ) -> ( ( i <_ A /\ A < B ) -> i < B ) )
17 16 expcomd 
 |-  ( ( A e. NN /\ B e. NN /\ i e. ( ZZ>= ` 2 ) ) -> ( A < B -> ( i <_ A -> i < B ) ) )
18 17 3exp 
 |-  ( A e. NN -> ( B e. NN -> ( i e. ( ZZ>= ` 2 ) -> ( A < B -> ( i <_ A -> i < B ) ) ) ) )
19 18 com34 
 |-  ( A e. NN -> ( B e. NN -> ( A < B -> ( i e. ( ZZ>= ` 2 ) -> ( i <_ A -> i < B ) ) ) ) )
20 19 3imp1 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i <_ A -> i < B ) )
21 20 imp 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ i <_ A ) -> i < B )
22 nnz 
 |-  ( B e. NN -> B e. ZZ )
23 22 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> B e. ZZ )
24 23 5 anim12ci 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i e. ZZ /\ B e. ZZ ) )
25 24 adantr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ i <_ A ) -> ( i e. ZZ /\ B e. ZZ ) )
26 zltlem1 
 |-  ( ( i e. ZZ /\ B e. ZZ ) -> ( i < B <-> i <_ ( B - 1 ) ) )
27 25 26 syl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ i <_ A ) -> ( i < B <-> i <_ ( B - 1 ) ) )
28 21 27 mpbid 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ i <_ A ) -> i <_ ( B - 1 ) )
29 28 ex 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i <_ A -> i <_ ( B - 1 ) ) )
30 8 29 syldc 
 |-  ( i || A -> ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> i <_ ( B - 1 ) ) )
31 30 adantr 
 |-  ( ( i || A /\ i || B ) -> ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> i <_ ( B - 1 ) ) )
32 31 impcom 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> i <_ ( B - 1 ) )
33 peano2zm 
 |-  ( B e. ZZ -> ( B - 1 ) e. ZZ )
34 22 33 syl 
 |-  ( B e. NN -> ( B - 1 ) e. ZZ )
35 34 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( B - 1 ) e. ZZ )
36 35 anim1ci 
 |-  ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) -> ( i e. ( ZZ>= ` 2 ) /\ ( B - 1 ) e. ZZ ) )
37 36 adantr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> ( i e. ( ZZ>= ` 2 ) /\ ( B - 1 ) e. ZZ ) )
38 elfz5 
 |-  ( ( i e. ( ZZ>= ` 2 ) /\ ( B - 1 ) e. ZZ ) -> ( i e. ( 2 ... ( B - 1 ) ) <-> i <_ ( B - 1 ) ) )
39 37 38 syl 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> ( i e. ( 2 ... ( B - 1 ) ) <-> i <_ ( B - 1 ) ) )
40 32 39 mpbird 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> i e. ( 2 ... ( B - 1 ) ) )
41 breq1 
 |-  ( j = i -> ( j || B <-> i || B ) )
42 41 adantl 
 |-  ( ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) /\ j = i ) -> ( j || B <-> i || B ) )
43 simprr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> i || B )
44 40 42 43 rspcedvd 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> E. j e. ( 2 ... ( B - 1 ) ) j || B )
45 rexnal 
 |-  ( E. j e. ( 2 ... ( B - 1 ) ) -. -. j || B <-> -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B )
46 notnotb 
 |-  ( j || B <-> -. -. j || B )
47 46 bicomi 
 |-  ( -. -. j || B <-> j || B )
48 47 rexbii 
 |-  ( E. j e. ( 2 ... ( B - 1 ) ) -. -. j || B <-> E. j e. ( 2 ... ( B - 1 ) ) j || B )
49 45 48 bitr3i 
 |-  ( -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B <-> E. j e. ( 2 ... ( B - 1 ) ) j || B )
50 44 49 sylibr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B )
51 50 olcd 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> ( -. B e. ( ZZ>= ` 2 ) \/ -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) )
52 df-nel 
 |-  ( B e/ Prime <-> -. B e. Prime )
53 ianor 
 |-  ( -. ( B e. ( ZZ>= ` 2 ) /\ A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) <-> ( -. B e. ( ZZ>= ` 2 ) \/ -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) )
54 isprm3 
 |-  ( B e. Prime <-> ( B e. ( ZZ>= ` 2 ) /\ A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) )
55 53 54 xchnxbir 
 |-  ( -. B e. Prime <-> ( -. B e. ( ZZ>= ` 2 ) \/ -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) )
56 52 55 bitri 
 |-  ( B e/ Prime <-> ( -. B e. ( ZZ>= ` 2 ) \/ -. A. j e. ( 2 ... ( B - 1 ) ) -. j || B ) )
57 51 56 sylibr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ A < B ) /\ i e. ( ZZ>= ` 2 ) ) /\ ( i || A /\ i || B ) ) -> B e/ Prime )
58 57 rexlimdva2 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( E. i e. ( ZZ>= ` 2 ) ( i || A /\ i || B ) -> B e/ Prime ) )
59 3 58 sylbid 
 |-  ( ( A e. NN /\ B e. NN /\ A < B ) -> ( 1 < ( A gcd B ) -> B e/ Prime ) )