Metamath Proof Explorer

Theorem sqnprm

Description: A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Assertion sqnprm ⊢ A ∈ ℤ → ¬ A 2 ∈ ℙ

Proof

Step Hyp Ref Expression
1 zre ⊢ A ∈ ℤ → A ∈ ℝ
2 1 adantr ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℝ
3 absresq ⊢ A ∈ ℝ → A 2 = A 2
4 2 3 syl ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A 2 = A 2
5 2 recnd ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℂ
6 5 abscld ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℝ
7 6 recnd ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℂ
8 7 sqvald ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A 2 = A ⁢ A
9 4 8 eqtr3d ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A 2 = A ⁢ A
10 simpr ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A 2 ∈ ℙ
11 9 10 eqeltrrd ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ⁢ A ∈ ℙ
12 nn0abscl ⊢ A ∈ ℤ → A ∈ ℕ 0
13 12 adantr ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℕ 0
14 13 nn0zd ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℤ
15 sq1 ⊢ 1 2 = 1
16 prmuz2 ⊢ A 2 ∈ ℙ → A 2 ∈ ℤ ≥ 2
17 16 adantl ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A 2 ∈ ℤ ≥ 2
18 eluz2gt1 ⊢ A 2 ∈ ℤ ≥ 2 → 1 < A 2
19 17 18 syl ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 1 < A 2
20 19 4 breqtrrd ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 1 < A 2
21 15 20 eqbrtrid ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 1 2 < A 2
22 5 absge0d ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 0 ≤ A
23 1re ⊢ 1 ∈ ℝ
24 0le1 ⊢ 0 ≤ 1
25 lt2sq ⊢ 1 ∈ ℝ ∧ 0 ≤ 1 ∧ A ∈ ℝ ∧ 0 ≤ A → 1 < A ↔ 1 2 < A 2
26 23 24 25 mpanl12 ⊢ A ∈ ℝ ∧ 0 ≤ A → 1 < A ↔ 1 2 < A 2
27 6 22 26 syl2anc ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 1 < A ↔ 1 2 < A 2
28 21 27 mpbird ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → 1 < A
29 eluz2b1 ⊢ A ∈ ℤ ≥ 2 ↔ A ∈ ℤ ∧ 1 < A
30 14 28 29 sylanbrc ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → A ∈ ℤ ≥ 2
31 nprm ⊢ A ∈ ℤ ≥ 2 ∧ A ∈ ℤ ≥ 2 → ¬ A ⁢ A ∈ ℙ
32 30 30 31 syl2anc ⊢ A ∈ ℤ ∧ A 2 ∈ ℙ → ¬ A ⁢ A ∈ ℙ
33 11 32 pm2.65da ⊢ A ∈ ℤ → ¬ A 2 ∈ ℙ