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	syl5eq	⊢ ( 𝐴 ∈ 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	syl6bi	⊢ ( 𝐴 ∈ 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	syl5eq	⊢ ( 𝐴 ∈ 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 𝐴 ) )