Metamath Proof Explorer

Theorem sqnprm

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

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

Proof

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