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

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 ( ( 𝐴 ∈ R ∧ 𝐴 ≠ 0R ) → 0R <R ( 𝐴 ·R 𝐴 ) )

Proof

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