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 ( 𝐴 ∈ ℕ → ( ∀ 𝑥 ∈ ℕ ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( 𝑥 = 1 ∨ 𝑥 = 𝐴 ) ) ↔ ∀ 𝑥 ∈ ℕ ( ( 1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ ( 𝐴 / 𝑥 ) ∈ ℕ ) → 𝑥 = 𝐴 ) ) )

Proof

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