Metamath Proof Explorer

Theorem sqgt0sr

Description: The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

Ref Expression
Assertion sqgt0sr 
|- ( ( A e. R. /\ A =/= 0R ) -> 0R

Proof

Step Hyp Ref Expression
1 0r 
 |-  0R e. R.
2 ltsosr 
 |-
3 sotrieq 
 |-  ( (  ( A = 0R <-> -. ( A
4 2 3 mpan 
 |-  ( ( A e. R. /\ 0R e. R. ) -> ( A = 0R <-> -. ( A
5 1 4 mpan2 
 |-  ( A e. R. -> ( A = 0R <-> -. ( A
6 5 necon2abid 
 |-  ( A e. R. -> ( ( A  A =/= 0R ) )
7 m1r 
 |-  -1R e. R.
8 mulclsr 
 |-  ( ( A e. R. /\ -1R e. R. ) -> ( A .R -1R ) e. R. )
9 7 8 mpan2 
 |-  ( A e. R. -> ( A .R -1R ) e. R. )
10 ltasr 
 |-  ( ( A .R -1R ) e. R. -> ( A  ( ( A .R -1R ) +R A )
11 9 10 syl 
 |-  ( A e. R. -> ( A  ( ( A .R -1R ) +R A )
12 addcomsr 
 |-  ( ( A .R -1R ) +R A ) = ( A +R ( A .R -1R ) )
13 pn0sr 
 |-  ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )
14 12 13 syl5eq 
 |-  ( A e. R. -> ( ( A .R -1R ) +R A ) = 0R )
15 0idsr 
 |-  ( ( A .R -1R ) e. R. -> ( ( A .R -1R ) +R 0R ) = ( A .R -1R ) )
16 9 15 syl 
 |-  ( A e. R. -> ( ( A .R -1R ) +R 0R ) = ( A .R -1R ) )
17 14 16 breq12d 
 |-  ( A e. R. -> ( ( ( A .R -1R ) +R A )  0R
18 11 17 bitrd 
 |-  ( A e. R. -> ( A  0R
19 mulgt0sr 
 |-  ( ( 0R  0R
20 19 anidms 
 |-  ( 0R  0R
21 18 20 syl6bi 
 |-  ( A e. R. -> ( A  0R
22 mulcomsr 
 |-  ( -1R .R A ) = ( A .R -1R )
23 22 oveq1i 
 |-  ( ( -1R .R A ) .R -1R ) = ( ( A .R -1R ) .R -1R )
24 mulasssr 
 |-  ( ( -1R .R A ) .R -1R ) = ( -1R .R ( A .R -1R ) )
25 mulasssr 
 |-  ( ( A .R -1R ) .R -1R ) = ( A .R ( -1R .R -1R ) )
26 23 24 25 3eqtr3i 
 |-  ( -1R .R ( A .R -1R ) ) = ( A .R ( -1R .R -1R ) )
27 m1m1sr 
 |-  ( -1R .R -1R ) = 1R
28 27 oveq2i 
 |-  ( A .R ( -1R .R -1R ) ) = ( A .R 1R )
29 26 28 eqtri 
 |-  ( -1R .R ( A .R -1R ) ) = ( A .R 1R )
30 29 oveq2i 
 |-  ( A .R ( -1R .R ( A .R -1R ) ) ) = ( A .R ( A .R 1R ) )
31 mulasssr 
 |-  ( ( A .R -1R ) .R ( A .R -1R ) ) = ( A .R ( -1R .R ( A .R -1R ) ) )
32 mulasssr 
 |-  ( ( A .R A ) .R 1R ) = ( A .R ( A .R 1R ) )
33 30 31 32 3eqtr4i 
 |-  ( ( A .R -1R ) .R ( A .R -1R ) ) = ( ( A .R A ) .R 1R )
34 mulclsr 
 |-  ( ( A e. R. /\ A e. R. ) -> ( A .R A ) e. R. )
35 1idsr 
 |-  ( ( A .R A ) e. R. -> ( ( A .R A ) .R 1R ) = ( A .R A ) )
36 34 35 syl 
 |-  ( ( A e. R. /\ A e. R. ) -> ( ( A .R A ) .R 1R ) = ( A .R A ) )
37 36 anidms 
 |-  ( A e. R. -> ( ( A .R A ) .R 1R ) = ( A .R A ) )
38 33 37 syl5eq 
 |-  ( A e. R. -> ( ( A .R -1R ) .R ( A .R -1R ) ) = ( A .R A ) )
39 38 breq2d 
 |-  ( A e. R. -> ( 0R  0R
40 21 39 sylibd 
 |-  ( A e. R. -> ( A  0R
41 mulgt0sr 
 |-  ( ( 0R  0R
42 41 anidms 
 |-  ( 0R  0R
43 42 a1i 
 |-  ( A e. R. -> ( 0R  0R
44 40 43 jaod 
 |-  ( A e. R. -> ( ( A  0R
45 6 44 sylbird 
 |-  ( A e. R. -> ( A =/= 0R -> 0R
46 45 imp 
 |-  ( ( A e. R. /\ A =/= 0R ) -> 0R