Metamath Proof Explorer

Theorem sqnprm

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

Ref Expression
Assertion sqnprm 
|- ( A e. ZZ -> -. ( A ^ 2 ) e. Prime )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 1 adantr 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> A e. RR )
3 absresq 
 |-  ( A e. RR -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
4 2 3 syl 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( ( abs ` A ) ^ 2 ) = ( A ^ 2 ) )
5 2 recnd 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> A e. CC )
6 5 abscld 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( abs ` A ) e. RR )
7 6 recnd 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( abs ` A ) e. CC )
8 7 sqvald 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( ( abs ` A ) ^ 2 ) = ( ( abs ` A ) x. ( abs ` A ) ) )
9 4 8 eqtr3d 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( A ^ 2 ) = ( ( abs ` A ) x. ( abs ` A ) ) )
10 simpr 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( A ^ 2 ) e. Prime )
11 9 10 eqeltrrd 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( ( abs ` A ) x. ( abs ` A ) ) e. Prime )
12 nn0abscl 
 |-  ( A e. ZZ -> ( abs ` A ) e. NN0 )
13 12 adantr 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( abs ` A ) e. NN0 )
14 13 nn0zd 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( abs ` A ) e. ZZ )
15 sq1 
 |-  ( 1 ^ 2 ) = 1
16 prmuz2 
 |-  ( ( A ^ 2 ) e. Prime -> ( A ^ 2 ) e. ( ZZ>= ` 2 ) )
17 16 adantl 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( A ^ 2 ) e. ( ZZ>= ` 2 ) )
18 eluz2gt1 
 |-  ( ( A ^ 2 ) e. ( ZZ>= ` 2 ) -> 1 < ( A ^ 2 ) )
19 17 18 syl 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> 1 < ( A ^ 2 ) )
20 19 4 breqtrrd 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> 1 < ( ( abs ` A ) ^ 2 ) )
21 15 20 eqbrtrid 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( 1 ^ 2 ) < ( ( abs ` A ) ^ 2 ) )
22 5 absge0d 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> 0 <_ ( abs ` A ) )
23 1re 
 |-  1 e. RR
24 0le1 
 |-  0 <_ 1
25 lt2sq 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) ) -> ( 1 < ( abs ` A ) <-> ( 1 ^ 2 ) < ( ( abs ` A ) ^ 2 ) ) )
26 23 24 25 mpanl12 
 |-  ( ( ( abs ` A ) e. RR /\ 0 <_ ( abs ` A ) ) -> ( 1 < ( abs ` A ) <-> ( 1 ^ 2 ) < ( ( abs ` A ) ^ 2 ) ) )
27 6 22 26 syl2anc 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( 1 < ( abs ` A ) <-> ( 1 ^ 2 ) < ( ( abs ` A ) ^ 2 ) ) )
28 21 27 mpbird 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> 1 < ( abs ` A ) )
29 eluz2b1 
 |-  ( ( abs ` A ) e. ( ZZ>= ` 2 ) <-> ( ( abs ` A ) e. ZZ /\ 1 < ( abs ` A ) ) )
30 14 28 29 sylanbrc 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> ( abs ` A ) e. ( ZZ>= ` 2 ) )
31 nprm 
 |-  ( ( ( abs ` A ) e. ( ZZ>= ` 2 ) /\ ( abs ` A ) e. ( ZZ>= ` 2 ) ) -> -. ( ( abs ` A ) x. ( abs ` A ) ) e. Prime )
32 30 30 31 syl2anc 
 |-  ( ( A e. ZZ /\ ( A ^ 2 ) e. Prime ) -> -. ( ( abs ` A ) x. ( abs ` A ) ) e. Prime )
33 11 32 pm2.65da 
 |-  ( A e. ZZ -> -. ( A ^ 2 ) e. Prime )