Proof of Theorem sqgt0sr
Step | Hyp | Ref
| Expression |
1 | | 0r 10694 |
. . . . 5
⊢
0R ∈ R |
2 | | ltsosr 10708 |
. . . . . 6
⊢
<R Or R |
3 | | sotrieq 5497 |
. . . . . 6
⊢ ((
<R Or R ∧ (𝐴 ∈ R ∧
0R ∈ R)) → (𝐴 = 0R ↔ ¬
(𝐴
<R 0R ∨
0R <R 𝐴))) |
4 | 2, 3 | mpan 690 |
. . . . 5
⊢ ((𝐴 ∈ R ∧
0R ∈ R) → (𝐴 = 0R ↔ ¬
(𝐴
<R 0R ∨
0R <R 𝐴))) |
5 | 1, 4 | mpan2 691 |
. . . 4
⊢ (𝐴 ∈ R →
(𝐴 =
0R ↔ ¬ (𝐴 <R
0R ∨ 0R
<R 𝐴))) |
6 | 5 | necon2abid 2983 |
. . 3
⊢ (𝐴 ∈ R →
((𝐴
<R 0R ∨
0R <R 𝐴) ↔ 𝐴 ≠
0R)) |
7 | | m1r 10696 |
. . . . . . . . 9
⊢
-1R ∈ R |
8 | | mulclsr 10698 |
. . . . . . . . 9
⊢ ((𝐴 ∈ R ∧
-1R ∈ R) → (𝐴 ·R
-1R) ∈ R) |
9 | 7, 8 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ R →
(𝐴
·R -1R) ∈
R) |
10 | | ltasr 10714 |
. . . . . . . 8
⊢ ((𝐴
·R -1R) ∈
R → (𝐴
<R 0R ↔ ((𝐴
·R -1R)
+R 𝐴) <R ((𝐴
·R -1R)
+R 0R))) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ R →
(𝐴
<R 0R ↔ ((𝐴
·R -1R)
+R 𝐴) <R ((𝐴
·R -1R)
+R 0R))) |
12 | | addcomsr 10701 |
. . . . . . . . 9
⊢ ((𝐴
·R -1R)
+R 𝐴) = (𝐴 +R (𝐴
·R
-1R)) |
13 | | pn0sr 10715 |
. . . . . . . . 9
⊢ (𝐴 ∈ R →
(𝐴
+R (𝐴 ·R
-1R)) = 0R) |
14 | 12, 13 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐴 ∈ R →
((𝐴
·R -1R)
+R 𝐴) =
0R) |
15 | | 0idsr 10711 |
. . . . . . . . 9
⊢ ((𝐴
·R -1R) ∈
R → ((𝐴
·R -1R)
+R 0R) = (𝐴 ·R
-1R)) |
16 | 9, 15 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ R →
((𝐴
·R -1R)
+R 0R) = (𝐴 ·R
-1R)) |
17 | 14, 16 | breq12d 5066 |
. . . . . . 7
⊢ (𝐴 ∈ R →
(((𝐴
·R -1R)
+R 𝐴) <R ((𝐴
·R -1R)
+R 0R) ↔
0R <R (𝐴 ·R
-1R))) |
18 | 11, 17 | bitrd 282 |
. . . . . 6
⊢ (𝐴 ∈ R →
(𝐴
<R 0R ↔
0R <R (𝐴 ·R
-1R))) |
19 | | mulgt0sr 10719 |
. . . . . . 7
⊢
((0R <R (𝐴
·R -1R) ∧
0R <R (𝐴 ·R
-1R)) → 0R
<R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R))) |
20 | 19 | anidms 570 |
. . . . . 6
⊢
(0R <R (𝐴
·R -1R) →
0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R))) |
21 | 18, 20 | syl6bi 256 |
. . . . 5
⊢ (𝐴 ∈ R →
(𝐴
<R 0R →
0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R)))) |
22 | | mulcomsr 10703 |
. . . . . . . . . . . 12
⊢
(-1R ·R 𝐴) = (𝐴 ·R
-1R) |
23 | 22 | oveq1i 7223 |
. . . . . . . . . . 11
⊢
((-1R ·R 𝐴)
·R -1R) = ((𝐴
·R -1R)
·R
-1R) |
24 | | mulasssr 10704 |
. . . . . . . . . . 11
⊢
((-1R ·R 𝐴)
·R -1R) =
(-1R ·R (𝐴
·R
-1R)) |
25 | | mulasssr 10704 |
. . . . . . . . . . 11
⊢ ((𝐴
·R -1R)
·R -1R) = (𝐴
·R (-1R
·R
-1R)) |
26 | 23, 24, 25 | 3eqtr3i 2773 |
. . . . . . . . . 10
⊢
(-1R ·R (𝐴
·R -1R)) = (𝐴
·R (-1R
·R
-1R)) |
27 | | m1m1sr 10707 |
. . . . . . . . . . 11
⊢
(-1R ·R
-1R) = 1R |
28 | 27 | oveq2i 7224 |
. . . . . . . . . 10
⊢ (𝐴
·R (-1R
·R -1R)) = (𝐴
·R
1R) |
29 | 26, 28 | eqtri 2765 |
. . . . . . . . 9
⊢
(-1R ·R (𝐴
·R -1R)) = (𝐴
·R
1R) |
30 | 29 | oveq2i 7224 |
. . . . . . . 8
⊢ (𝐴
·R (-1R
·R (𝐴 ·R
-1R))) = (𝐴 ·R (𝐴
·R
1R)) |
31 | | mulasssr 10704 |
. . . . . . . 8
⊢ ((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = (𝐴 ·R
(-1R ·R (𝐴
·R
-1R))) |
32 | | mulasssr 10704 |
. . . . . . . 8
⊢ ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R (𝐴
·R
1R)) |
33 | 30, 31, 32 | 3eqtr4i 2775 |
. . . . . . 7
⊢ ((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = ((𝐴 ·R 𝐴)
·R
1R) |
34 | | mulclsr 10698 |
. . . . . . . . 9
⊢ ((𝐴 ∈ R ∧
𝐴 ∈ R)
→ (𝐴
·R 𝐴) ∈ R) |
35 | | 1idsr 10712 |
. . . . . . . . 9
⊢ ((𝐴
·R 𝐴) ∈ R → ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ R ∧
𝐴 ∈ R)
→ ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
37 | 36 | anidms 570 |
. . . . . . 7
⊢ (𝐴 ∈ R →
((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
38 | 33, 37 | eqtrid 2789 |
. . . . . 6
⊢ (𝐴 ∈ R →
((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = (𝐴 ·R 𝐴)) |
39 | 38 | breq2d 5065 |
. . . . 5
⊢ (𝐴 ∈ R →
(0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R -1R)) ↔
0R <R (𝐴 ·R 𝐴))) |
40 | 21, 39 | sylibd 242 |
. . . 4
⊢ (𝐴 ∈ R →
(𝐴
<R 0R →
0R <R (𝐴 ·R 𝐴))) |
41 | | mulgt0sr 10719 |
. . . . . 6
⊢
((0R <R 𝐴 ∧
0R <R 𝐴) → 0R
<R (𝐴 ·R 𝐴)) |
42 | 41 | anidms 570 |
. . . . 5
⊢
(0R <R 𝐴 →
0R <R (𝐴 ·R 𝐴)) |
43 | 42 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ R →
(0R <R 𝐴 → 0R
<R (𝐴 ·R 𝐴))) |
44 | 40, 43 | jaod 859 |
. . 3
⊢ (𝐴 ∈ R →
((𝐴
<R 0R ∨
0R <R 𝐴) → 0R
<R (𝐴 ·R 𝐴))) |
45 | 6, 44 | sylbird 263 |
. 2
⊢ (𝐴 ∈ R →
(𝐴 ≠
0R → 0R
<R (𝐴 ·R 𝐴))) |
46 | 45 | imp 410 |
1
⊢ ((𝐴 ∈ R ∧
𝐴 ≠
0R) → 0R
<R (𝐴 ·R 𝐴)) |