Theorem sqnprm

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

	Ref	Expression
Assertion	sqnprm	⊢ ( 𝐴 ∈ ℤ → ¬ ( 𝐴 ↑ 2 ) ∈ ℙ )

Proof

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