Metamath Proof Explorer

Theorem prime

Description: Two ways to express " A is a prime number (or 1)." See also isprm . (Contributed by NM, 4-May-2005)

Ref Expression
Assertion prime 
|- ( A e. NN -> ( A. x e. NN ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> A. x e. NN ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) )

Proof

Step Hyp Ref Expression
1 bi2.04 
 |-  ( ( x =/= 1 -> ( ( A / x ) e. NN -> x = A ) ) <-> ( ( A / x ) e. NN -> ( x =/= 1 -> x = A ) ) )
2 impexp 
 |-  ( ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) <-> ( x =/= 1 -> ( ( A / x ) e. NN -> x = A ) ) )
3 neor 
 |-  ( ( x = 1 \/ x = A ) <-> ( x =/= 1 -> x = A ) )
4 3 imbi2i 
 |-  ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( A / x ) e. NN -> ( x =/= 1 -> x = A ) ) )
5 1 2 4 3bitr4ri 
 |-  ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) )
6 nngt1ne1 
 |-  ( x e. NN -> ( 1 < x <-> x =/= 1 ) )
7 6 adantl 
 |-  ( ( A e. NN /\ x e. NN ) -> ( 1 < x <-> x =/= 1 ) )
8 7 anbi1d 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( x =/= 1 /\ ( A / x ) e. NN ) ) )
9 nnz 
 |-  ( ( A / x ) e. NN -> ( A / x ) e. ZZ )
10 nnre 
 |-  ( x e. NN -> x e. RR )
11 gtndiv 
 |-  ( ( x e. RR /\ A e. NN /\ A < x ) -> -. ( A / x ) e. ZZ )
12 11 3expia 
 |-  ( ( x e. RR /\ A e. NN ) -> ( A < x -> -. ( A / x ) e. ZZ ) )
13 10 12 sylan 
 |-  ( ( x e. NN /\ A e. NN ) -> ( A < x -> -. ( A / x ) e. ZZ ) )
14 13 con2d 
 |-  ( ( x e. NN /\ A e. NN ) -> ( ( A / x ) e. ZZ -> -. A < x ) )
15 nnre 
 |-  ( A e. NN -> A e. RR )
16 lenlt 
 |-  ( ( x e. RR /\ A e. RR ) -> ( x <_ A <-> -. A < x ) )
17 10 15 16 syl2an 
 |-  ( ( x e. NN /\ A e. NN ) -> ( x <_ A <-> -. A < x ) )
18 14 17 sylibrd 
 |-  ( ( x e. NN /\ A e. NN ) -> ( ( A / x ) e. ZZ -> x <_ A ) )
19 18 ancoms 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. ZZ -> x <_ A ) )
20 9 19 syl5 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. NN -> x <_ A ) )
21 20 pm4.71rd 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( A / x ) e. NN <-> ( x <_ A /\ ( A / x ) e. NN ) ) )
22 21 anbi2d 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( 1 < x /\ ( x <_ A /\ ( A / x ) e. NN ) ) ) )
23 3anass 
 |-  ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) <-> ( 1 < x /\ ( x <_ A /\ ( A / x ) e. NN ) ) )
24 22 23 bitr4di 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( 1 < x /\ ( A / x ) e. NN ) <-> ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) ) )
25 8 24 bitr3d 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( x =/= 1 /\ ( A / x ) e. NN ) <-> ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) ) )
26 25 imbi1d 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( ( x =/= 1 /\ ( A / x ) e. NN ) -> x = A ) <-> ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) )
27 5 26 syl5bb 
 |-  ( ( A e. NN /\ x e. NN ) -> ( ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) )
28 27 ralbidva 
 |-  ( A e. NN -> ( A. x e. NN ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> A. x e. NN ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) )