Step |
Hyp |
Ref |
Expression |
1 |
|
remulcl |
โข ( ( ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) โ โ ) |
2 |
1
|
3adant2 |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ ) โ โ ) |
3 |
2
|
adantr |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ( ๐ ยท ๐ ) โ โ ) |
4 |
|
simpl2 |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ๐ โ โ ) |
5 |
|
resqrtcl |
โข ( ( ๐ โ โ โง 0 โค ๐ ) โ ( โ โ ๐ ) โ โ ) |
6 |
5
|
adantl |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ( โ โ ๐ ) โ โ ) |
7 |
4 6
|
remulcld |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ( ๐ ยท ( โ โ ๐ ) ) โ โ ) |
8 |
3 7
|
readdcld |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ( ( ๐ ยท ๐ ) + ( ๐ ยท ( โ โ ๐ ) ) ) โ โ ) |
9 |
8
|
3adant3 |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ๐ ยท ๐ ) + ( ๐ ยท ( โ โ ๐ ) ) ) โ โ ) |
10 |
|
simp3l |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ๐ โ โ ) |
11 |
|
simp3r |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ๐ โ 0 ) |
12 |
9 10 11
|
redivcld |
โข ( ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ โ ) โง ( ๐ โ โ โง 0 โค ๐ ) โง ( ๐ โ โ โง ๐ โ 0 ) ) โ ( ( ( ๐ ยท ๐ ) + ( ๐ ยท ( โ โ ๐ ) ) ) / ๐ ) โ โ ) |