Proof of Theorem sqgt0sr
| Step | Hyp | Ref
| Expression |
| 1 | | 0r 11120 |
. . . . 5
⊢
0R ∈ R |
| 2 | | ltsosr 11134 |
. . . . . 6
⊢
<R Or R |
| 3 | | sotrieq 5623 |
. . . . . 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 11122 |
. . . . . . . . 9
⊢
-1R ∈ R |
| 8 | | mulclsr 11124 |
. . . . . . . . 9
⊢ ((𝐴 ∈ R ∧
-1R ∈ R) → (𝐴 ·R
-1R) ∈ R) |
| 9 | 7, 8 | mpan2 691 |
. . . . . . . 8
⊢ (𝐴 ∈ R →
(𝐴
·R -1R) ∈
R) |
| 10 | | ltasr 11140 |
. . . . . . . 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 11127 |
. . . . . . . . 9
⊢ ((𝐴
·R -1R)
+R 𝐴) = (𝐴 +R (𝐴
·R
-1R)) |
| 13 | | pn0sr 11141 |
. . . . . . . . 9
⊢ (𝐴 ∈ R →
(𝐴
+R (𝐴 ·R
-1R)) = 0R) |
| 14 | 12, 13 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝐴 ∈ R →
((𝐴
·R -1R)
+R 𝐴) =
0R) |
| 15 | | 0idsr 11137 |
. . . . . . . . 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 5156 |
. . . . . . 7
⊢ (𝐴 ∈ R →
(((𝐴
·R -1R)
+R 𝐴) <R ((𝐴
·R -1R)
+R 0R) ↔
0R <R (𝐴 ·R
-1R))) |
| 18 | 11, 17 | bitrd 279 |
. . . . . 6
⊢ (𝐴 ∈ R →
(𝐴
<R 0R ↔
0R <R (𝐴 ·R
-1R))) |
| 19 | | mulgt0sr 11145 |
. . . . . . 7
⊢
((0R <R (𝐴
·R -1R) ∧
0R <R (𝐴 ·R
-1R)) → 0R
<R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R))) |
| 20 | 19 | anidms 566 |
. . . . . 6
⊢
(0R <R (𝐴
·R -1R) →
0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R))) |
| 21 | 18, 20 | biimtrdi 253 |
. . . . 5
⊢ (𝐴 ∈ R →
(𝐴
<R 0R →
0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R
-1R)))) |
| 22 | | mulcomsr 11129 |
. . . . . . . . . . . 12
⊢
(-1R ·R 𝐴) = (𝐴 ·R
-1R) |
| 23 | 22 | oveq1i 7441 |
. . . . . . . . . . 11
⊢
((-1R ·R 𝐴)
·R -1R) = ((𝐴
·R -1R)
·R
-1R) |
| 24 | | mulasssr 11130 |
. . . . . . . . . . 11
⊢
((-1R ·R 𝐴)
·R -1R) =
(-1R ·R (𝐴
·R
-1R)) |
| 25 | | mulasssr 11130 |
. . . . . . . . . . 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 11133 |
. . . . . . . . . . 11
⊢
(-1R ·R
-1R) = 1R |
| 28 | 27 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝐴
·R (-1R
·R -1R)) = (𝐴
·R
1R) |
| 29 | 26, 28 | eqtri 2765 |
. . . . . . . . 9
⊢
(-1R ·R (𝐴
·R -1R)) = (𝐴
·R
1R) |
| 30 | 29 | oveq2i 7442 |
. . . . . . . 8
⊢ (𝐴
·R (-1R
·R (𝐴 ·R
-1R))) = (𝐴 ·R (𝐴
·R
1R)) |
| 31 | | mulasssr 11130 |
. . . . . . . 8
⊢ ((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = (𝐴 ·R
(-1R ·R (𝐴
·R
-1R))) |
| 32 | | mulasssr 11130 |
. . . . . . . 8
⊢ ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R (𝐴
·R
1R)) |
| 33 | 30, 31, 32 | 3eqtr4i 2775 |
. . . . . . 7
⊢ ((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = ((𝐴 ·R 𝐴)
·R
1R) |
| 34 | | mulclsr 11124 |
. . . . . . . . 9
⊢ ((𝐴 ∈ R ∧
𝐴 ∈ R)
→ (𝐴
·R 𝐴) ∈ R) |
| 35 | | 1idsr 11138 |
. . . . . . . . 9
⊢ ((𝐴
·R 𝐴) ∈ R → ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ R ∧
𝐴 ∈ R)
→ ((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
| 37 | 36 | anidms 566 |
. . . . . . 7
⊢ (𝐴 ∈ R →
((𝐴
·R 𝐴) ·R
1R) = (𝐴 ·R 𝐴)) |
| 38 | 33, 37 | eqtrid 2789 |
. . . . . 6
⊢ (𝐴 ∈ R →
((𝐴
·R -1R)
·R (𝐴 ·R
-1R)) = (𝐴 ·R 𝐴)) |
| 39 | 38 | breq2d 5155 |
. . . . 5
⊢ (𝐴 ∈ R →
(0R <R ((𝐴 ·R
-1R) ·R (𝐴
·R -1R)) ↔
0R <R (𝐴 ·R 𝐴))) |
| 40 | 21, 39 | sylibd 239 |
. . . 4
⊢ (𝐴 ∈ R →
(𝐴
<R 0R →
0R <R (𝐴 ·R 𝐴))) |
| 41 | | mulgt0sr 11145 |
. . . . . 6
⊢
((0R <R 𝐴 ∧
0R <R 𝐴) → 0R
<R (𝐴 ·R 𝐴)) |
| 42 | 41 | anidms 566 |
. . . . 5
⊢
(0R <R 𝐴 →
0R <R (𝐴 ·R 𝐴)) |
| 43 | 42 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ R →
(0R <R 𝐴 → 0R
<R (𝐴 ·R 𝐴))) |
| 44 | 40, 43 | jaod 860 |
. . 3
⊢ (𝐴 ∈ R →
((𝐴
<R 0R ∨
0R <R 𝐴) → 0R
<R (𝐴 ·R 𝐴))) |
| 45 | 6, 44 | sylbird 260 |
. 2
⊢ (𝐴 ∈ R →
(𝐴 ≠
0R → 0R
<R (𝐴 ·R 𝐴))) |
| 46 | 45 | imp 406 |
1
⊢ ((𝐴 ∈ R ∧
𝐴 ≠
0R) → 0R
<R (𝐴 ·R 𝐴)) |