This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∈ ℙ )