Step | Hyp | Ref
| Expression |
1 | | elq 9621 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ)) |
2 | | elq 9621 |
. 2
โข (๐ต โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ต = (๐ง / ๐ค)) |
3 | | zmulcl 9305 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ง โ โค) โ (๐ฅ ยท ๐ง) โ โค) |
4 | | nnmulcl 8939 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ ยท ๐ค) โ โ) |
5 | 3, 4 | anim12i 338 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ง โ โค) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ)) |
6 | 5 | an4s 588 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ ((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ)) |
7 | 6 | adantr 276 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ ((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ)) |
8 | | oveq12 5883 |
. . . . . . . . 9
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ด ยท ๐ต) = ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค))) |
9 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
10 | | zcn 9257 |
. . . . . . . . . . . 12
โข (๐ง โ โค โ ๐ง โ
โ) |
11 | 9, 10 | anim12i 338 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ง โ โค) โ (๐ฅ โ โ โง ๐ง โ
โ)) |
12 | 11 | ad2ant2r 509 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ (๐ฅ โ โ โง ๐ง โ
โ)) |
13 | | nncn 8926 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
14 | | nnap0 8947 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ # 0) |
15 | 13, 14 | jca 306 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (๐ฆ โ โ โง ๐ฆ # 0)) |
16 | | nncn 8926 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ ๐ค โ
โ) |
17 | | nnap0 8947 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ ๐ค # 0) |
18 | 16, 17 | jca 306 |
. . . . . . . . . . . 12
โข (๐ค โ โ โ (๐ค โ โ โง ๐ค # 0)) |
19 | 15, 18 | anim12i 338 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ค โ โ) โ ((๐ฆ โ โ โง ๐ฆ # 0) โง (๐ค โ โ โง ๐ค # 0))) |
20 | 19 | ad2ant2l 508 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ ((๐ฆ โ โ โง ๐ฆ # 0) โง (๐ค โ โ โง ๐ค # 0))) |
21 | | divmuldivap 8668 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ง โ โ) โง ((๐ฆ โ โ โง ๐ฆ # 0) โง (๐ค โ โ โง ๐ค # 0))) โ ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค)) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) |
22 | 12, 20, 21 | syl2anc 411 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ ((๐ฅ / ๐ฆ) ยท (๐ง / ๐ค)) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) |
23 | 8, 22 | sylan9eqr 2232 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด ยท ๐ต) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) |
24 | | rspceov 5916 |
. . . . . . . . . 10
โข (((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ โง (๐ด ยท ๐ต) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) โ โ๐ฃ โ โค โ๐ข โ โ (๐ด ยท ๐ต) = (๐ฃ / ๐ข)) |
25 | 24 | 3expa 1203 |
. . . . . . . . 9
โข ((((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ) โง (๐ด ยท ๐ต) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) โ โ๐ฃ โ โค โ๐ข โ โ (๐ด ยท ๐ต) = (๐ฃ / ๐ข)) |
26 | | elq 9621 |
. . . . . . . . 9
โข ((๐ด ยท ๐ต) โ โ โ โ๐ฃ โ โค โ๐ข โ โ (๐ด ยท ๐ต) = (๐ฃ / ๐ข)) |
27 | 25, 26 | sylibr 134 |
. . . . . . . 8
โข ((((๐ฅ ยท ๐ง) โ โค โง (๐ฆ ยท ๐ค) โ โ) โง (๐ด ยท ๐ต) = ((๐ฅ ยท ๐ง) / (๐ฆ ยท ๐ค))) โ (๐ด ยท ๐ต) โ โ) |
28 | 7, 23, 27 | syl2anc 411 |
. . . . . . 7
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด ยท ๐ต) โ โ) |
29 | 28 | an4s 588 |
. . . . . 6
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ด = (๐ฅ / ๐ฆ)) โง ((๐ง โ โค โง ๐ค โ โ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด ยท ๐ต) โ โ) |
30 | 29 | exp43 372 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ด = (๐ฅ / ๐ฆ) โ ((๐ง โ โค โง ๐ค โ โ) โ (๐ต = (๐ง / ๐ค) โ (๐ด ยท ๐ต) โ โ)))) |
31 | 30 | rexlimivv 2600 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โ ((๐ง โ โค โง ๐ค โ โ) โ (๐ต = (๐ง / ๐ค) โ (๐ด ยท ๐ต) โ โ))) |
32 | 31 | rexlimdvv 2601 |
. . 3
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โ (โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค) โ (๐ด ยท ๐ต) โ โ)) |
33 | 32 | imp 124 |
. 2
โข
((โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ด ยท ๐ต) โ โ) |
34 | 1, 2, 33 | syl2anb 291 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |