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∈ℕ→∀x∈ℕAx∈ℕ→x=1∨x=A↔∀x∈ℕ1<x∧x≤A∧Ax∈ℕ→x=A

Proof

Step Hyp Ref Expression
1 bi2.04 ⊢x≠1→Ax∈ℕ→x=A↔Ax∈ℕ→x≠1→x=A
2 impexp ⊢x≠1∧Ax∈ℕ→x=A↔x≠1→Ax∈ℕ→x=A
3 neor ⊢x=1∨x=A↔x≠1→x=A
4 3 imbi2i ⊢Ax∈ℕ→x=1∨x=A↔Ax∈ℕ→x≠1→x=A
5 1 2 4 3bitr4ri ⊢Ax∈ℕ→x=1∨x=A↔x≠1∧Ax∈ℕ→x=A
6 nngt1ne1 ⊢x∈ℕ→1<x↔x≠1
7 6 adantl ⊢A∈ℕ∧x∈ℕ→1<x↔x≠1
8 7 anbi1d ⊢A∈ℕ∧x∈ℕ→1<x∧Ax∈ℕ↔x≠1∧Ax∈ℕ
9 nnz ⊢Ax∈ℕ→Ax∈ℤ
10 nnre ⊢x∈ℕ→x∈ℝ
11 gtndiv ⊢x∈ℝ∧A∈ℕ∧A<x→¬Ax∈ℤ
12 11 3expia ⊢x∈ℝ∧A∈ℕ→A<x→¬Ax∈ℤ
13 10 12 sylan ⊢x∈ℕ∧A∈ℕ→A<x→¬Ax∈ℤ
14 13 con2d ⊢x∈ℕ∧A∈ℕ→Ax∈ℤ→¬A<x
15 nnre ⊢A∈ℕ→A∈ℝ
16 lenlt ⊢x∈ℝ∧A∈ℝ→x≤A↔¬A<x
17 10 15 16 syl2an ⊢x∈ℕ∧A∈ℕ→x≤A↔¬A<x
18 14 17 sylibrd ⊢x∈ℕ∧A∈ℕ→Ax∈ℤ→x≤A
19 18 ancoms ⊢A∈ℕ∧x∈ℕ→Ax∈ℤ→x≤A
20 9 19 syl5 ⊢A∈ℕ∧x∈ℕ→Ax∈ℕ→x≤A
21 20 pm4.71rd ⊢A∈ℕ∧x∈ℕ→Ax∈ℕ↔x≤A∧Ax∈ℕ
22 21 anbi2d ⊢A∈ℕ∧x∈ℕ→1<x∧Ax∈ℕ↔1<x∧x≤A∧Ax∈ℕ
23 3anass ⊢1<x∧x≤A∧Ax∈ℕ↔1<x∧x≤A∧Ax∈ℕ
24 22 23 bitr4di ⊢A∈ℕ∧x∈ℕ→1<x∧Ax∈ℕ↔1<x∧x≤A∧Ax∈ℕ
25 8 24 bitr3d ⊢A∈ℕ∧x∈ℕ→x≠1∧Ax∈ℕ↔1<x∧x≤A∧Ax∈ℕ
26 25 imbi1d ⊢A∈ℕ∧x∈ℕ→x≠1∧Ax∈ℕ→x=A↔1<x∧x≤A∧Ax∈ℕ→x=A
27 5 26 bitrid ⊢A∈ℕ∧x∈ℕ→Ax∈ℕ→x=1∨x=A↔1<x∧x≤A∧Ax∈ℕ→x=A
28 27 ralbidva ⊢A∈ℕ→∀x∈ℕAx∈ℕ→x=1∨x=A↔∀x∈ℕ1<x∧x≤A∧Ax∈ℕ→x=A