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

Proof

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