Step | Hyp | Ref
| Expression |
1 | | itscnhlc0yqe.q |
. . . . . . . . 9
โข ๐ = ((๐ดโ2) + (๐ตโ2)) |
2 | | itsclc0yqsol.d |
. . . . . . . . 9
โข ๐ท = (((๐
โ2) ยท ๐) โ (๐ถโ2)) |
3 | 1, 2 | itscnhlc0xyqsol 46941 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))) |
4 | 3 | 3exp 1120 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐
โ โ+ โง 0 โค
๐ท) โ ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))))) |
5 | 4 | 3exp 1120 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0) โ (๐ต โ โ โ (๐ถ โ โ โ ((๐
โ โ+
โง 0 โค ๐ท) โ
((๐ โ โ โง
๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))))))) |
6 | 5 | expcom 415 |
. . . . 5
โข (๐ด โ 0 โ (๐ด โ โ โ (๐ต โ โ โ (๐ถ โ โ โ ((๐
โ โ+
โง 0 โค ๐ท) โ
((๐ โ โ โง
๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))))))))) |
7 | 6 | 3impd 1349 |
. . . 4
โข (๐ด โ 0 โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐
โ โ+
โง 0 โค ๐ท) โ
((๐ โ โ โง
๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))))))) |
8 | | nne 2944 |
. . . . 5
โข (ยฌ
๐ด โ 0 โ ๐ด = 0) |
9 | 1, 2 | itschlc0xyqsol 46943 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด = 0 โง ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))) |
10 | 9 | 3exp 1120 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด = 0 โง ๐ต โ 0)) โ ((๐
โ โ+ โง 0 โค
๐ท) โ ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))))) |
11 | 10 | expcom 415 |
. . . . 5
โข ((๐ด = 0 โง ๐ต โ 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐
โ โ+ โง 0 โค
๐ท) โ ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))))))) |
12 | 8, 11 | sylanb 582 |
. . . 4
โข ((ยฌ
๐ด โ 0 โง ๐ต โ 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐
โ โ+
โง 0 โค ๐ท) โ
((๐ โ โ โง
๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))))))) |
13 | 7, 12 | jaoi3 1060 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐
โ โ+ โง 0 โค
๐ท) โ ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐)))))))) |
14 | 13 | impcom 409 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โ ((๐
โ โ+ โง 0 โค
๐ท) โ ((๐ โ โ โง ๐ โ โ) โ
((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))))) |
15 | 14 | 3imp 1112 |
1
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด โ 0 โจ ๐ต โ 0)) โง (๐
โ โ+ โง 0 โค
๐ท) โง (๐ โ โ โง ๐ โ โ)) โ ((((๐โ2) + (๐โ2)) = (๐
โ2) โง ((๐ด ยท ๐) + (๐ต ยท ๐)) = ๐ถ) โ ((๐ = (((๐ด ยท ๐ถ) + (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) โ (๐ด ยท (โโ๐ท))) / ๐)) โจ (๐ = (((๐ด ยท ๐ถ) โ (๐ต ยท (โโ๐ท))) / ๐) โง ๐ = (((๐ต ยท ๐ถ) + (๐ด ยท (โโ๐ท))) / ๐))))) |