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 ) ) )