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