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∈𝑹∧A≠0𝑹→0𝑹<𝑹A⋅𝑹A

Proof

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