Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โ ๐ด โ
โ) |
2 | 1 | anim1i 616 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โง ๐ด = 0) โ (๐ด โ โ โง ๐ด = 0)) |
3 | 2 | ancoms 460 |
. . . 4
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ (๐ด โ โ โง ๐ด = 0)) |
4 | | simpr12 1259 |
. . . 4
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ ๐ต โ
โ) |
5 | | simpr13 1260 |
. . . 4
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ ๐ถ โ
โ) |
6 | | simpr2 1196 |
. . . 4
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ ๐
โ
โ+) |
7 | | simpr3 1197 |
. . . 4
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ (๐ โ โ โง ๐ โ
โ)) |
8 | | itscnhlc0yqe.q |
. . . . 5
โข ๐ = ((๐ดโ2) + (๐ตโ2)) |
9 | | itscnhlc0yqe.t |
. . . . 5
โข ๐ = -(2 ยท (๐ต ยท ๐ถ)) |
10 | | itscnhlc0yqe.u |
. . . . 5
โข ๐ = ((๐ถโ2) โ ((๐ดโ2) ยท (๐
โ2))) |
11 | 8, 9, 10 | itschlc0yqe 46936 |
. . . 4
โข ((((๐ด โ โ โง ๐ด = 0) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ)) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0)) |
12 | 3, 4, 5, 6, 7, 11 | syl311anc 1385 |
. . 3
โข ((๐ด = 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ))) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0)) |
13 | 12 | ex 414 |
. 2
โข (๐ด = 0 โ (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ)) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0))) |
14 | 1 | anim1i 616 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โง ๐ด โ 0) โ
(๐ด โ โ โง
๐ด โ 0)) |
15 | 14 | ancoms 460 |
. . . 4
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ (๐ด โ โ
โง ๐ด โ
0)) |
16 | | simpr12 1259 |
. . . 4
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ ๐ต โ
โ) |
17 | | simpr13 1260 |
. . . 4
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ ๐ถ โ
โ) |
18 | | simpr2 1196 |
. . . 4
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ ๐
โ
โ+) |
19 | | simpr3 1197 |
. . . 4
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ (๐ โ โ
โง ๐ โ
โ)) |
20 | 8, 9, 10 | itscnhlc0yqe 46935 |
. . . 4
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+ โง (๐ โ โ โง ๐ โ โ)) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0)) |
21 | 15, 16, 17, 18, 19, 20 | syl311anc 1385 |
. . 3
โข ((๐ด โ 0 โง ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ)))
โ ((((๐โ2) +
(๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0)) |
22 | 21 | ex 414 |
. 2
โข (๐ด โ 0 โ (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โ ((((๐โ2) +
(๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0))) |
23 | 13, 22 | pm2.61ine 3025 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง ๐
โ โ+
โง (๐ โ โ
โง ๐ โ โ))
โ ((((๐โ2) +
(๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ ยท (๐โ2)) + ((๐ ยท ๐) + ๐)) = 0)) |