Step | Hyp | Ref
| Expression |
1 | | elq 12740 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โ
๐ด = (๐ฅ / ๐ฆ)) |
2 | | elq 12740 |
. 2
โข (๐ต โ โ โ
โ๐ง โ โค
โ๐ค โ โ
๐ต = (๐ง / ๐ค)) |
3 | | nnz 12392 |
. . . . . . . . . . . 12
โข (๐ค โ โ โ ๐ค โ
โค) |
4 | | zmulcl 12419 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โค โง ๐ค โ โค) โ (๐ฅ ยท ๐ค) โ โค) |
5 | 3, 4 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ค โ โ) โ (๐ฅ ยท ๐ค) โ โค) |
6 | 5 | ad2ant2rl 747 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ (๐ฅ ยท ๐ค) โ โค) |
7 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ค โ โ) โ ๐ง โ
โค) |
8 | | nnz 12392 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ ๐ฆ โ
โค) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ ๐ฆ โ
โค) |
10 | | zmulcl 12419 |
. . . . . . . . . . 11
โข ((๐ง โ โค โง ๐ฆ โ โค) โ (๐ง ยท ๐ฆ) โ โค) |
11 | 7, 9, 10 | syl2anr 598 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ (๐ง ยท ๐ฆ) โ โค) |
12 | 6, 11 | zaddcld 12480 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ ((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) โ โค) |
13 | 12 | adantr 482 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ ((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) โ โค) |
14 | | nnmulcl 12047 |
. . . . . . . . . 10
โข ((๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ ยท ๐ค) โ โ) |
15 | 14 | ad2ant2l 744 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ (๐ฆ ยท ๐ค) โ โ) |
16 | 15 | adantr 482 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ (๐ฆ ยท ๐ค) โ โ) |
17 | | oveq12 7316 |
. . . . . . . . 9
โข ((๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค)) โ (๐ด + ๐ต) = ((๐ฅ / ๐ฆ) + (๐ง / ๐ค))) |
18 | | zcn 12374 |
. . . . . . . . . . . 12
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
19 | | zcn 12374 |
. . . . . . . . . . . 12
โข (๐ง โ โค โ ๐ง โ
โ) |
20 | 18, 19 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ง โ โค) โ (๐ฅ โ โ โง ๐ง โ
โ)) |
21 | | nncn 12031 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
22 | | nnne0 12057 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ ๐ฆ โ 0) |
23 | 21, 22 | jca 513 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ โ (๐ฆ โ โ โง ๐ฆ โ 0)) |
24 | | nncn 12031 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ ๐ค โ
โ) |
25 | | nnne0 12057 |
. . . . . . . . . . . . 13
โข (๐ค โ โ โ ๐ค โ 0) |
26 | 24, 25 | jca 513 |
. . . . . . . . . . . 12
โข (๐ค โ โ โ (๐ค โ โ โง ๐ค โ 0)) |
27 | 23, 26 | anim12i 614 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ โง ๐ค โ โ) โ ((๐ฆ โ โ โง ๐ฆ โ 0) โง (๐ค โ โ โง ๐ค โ 0))) |
28 | | divadddiv 11740 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ง โ โ) โง ((๐ฆ โ โ โง ๐ฆ โ 0) โง (๐ค โ โ โง ๐ค โ 0))) โ ((๐ฅ / ๐ฆ) + (๐ง / ๐ค)) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) |
29 | 20, 27, 28 | syl2an 597 |
. . . . . . . . . 10
โข (((๐ฅ โ โค โง ๐ง โ โค) โง (๐ฆ โ โ โง ๐ค โ โ)) โ ((๐ฅ / ๐ฆ) + (๐ง / ๐ค)) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) |
30 | 29 | an4s 658 |
. . . . . . . . 9
โข (((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โ ((๐ฅ / ๐ฆ) + (๐ง / ๐ค)) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) |
31 | 17, 30 | sylan9eqr 2798 |
. . . . . . . 8
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด + ๐ต) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) |
32 | | rspceov 7354 |
. . . . . . . . 9
โข ((((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) โ โค โง (๐ฆ ยท ๐ค) โ โ โง (๐ด + ๐ต) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) โ โ๐ข โ โค โ๐ฃ โ โ (๐ด + ๐ต) = (๐ข / ๐ฃ)) |
33 | | elq 12740 |
. . . . . . . . 9
โข ((๐ด + ๐ต) โ โ โ โ๐ข โ โค โ๐ฃ โ โ (๐ด + ๐ต) = (๐ข / ๐ฃ)) |
34 | 32, 33 | sylibr 233 |
. . . . . . . 8
โข ((((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) โ โค โง (๐ฆ ยท ๐ค) โ โ โง (๐ด + ๐ต) = (((๐ฅ ยท ๐ค) + (๐ง ยท ๐ฆ)) / (๐ฆ ยท ๐ค))) โ (๐ด + ๐ต) โ โ) |
35 | 13, 16, 31, 34 | syl3anc 1371 |
. . . . . . 7
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง (๐ง โ โค โง ๐ค โ โ)) โง (๐ด = (๐ฅ / ๐ฆ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด + ๐ต) โ โ) |
36 | 35 | an4s 658 |
. . . . . 6
โข ((((๐ฅ โ โค โง ๐ฆ โ โ) โง ๐ด = (๐ฅ / ๐ฆ)) โง ((๐ง โ โค โง ๐ค โ โ) โง ๐ต = (๐ง / ๐ค))) โ (๐ด + ๐ต) โ โ) |
37 | 36 | exp43 438 |
. . . . 5
โข ((๐ฅ โ โค โง ๐ฆ โ โ) โ (๐ด = (๐ฅ / ๐ฆ) โ ((๐ง โ โค โง ๐ค โ โ) โ (๐ต = (๐ง / ๐ค) โ (๐ด + ๐ต) โ โ)))) |
38 | 37 | rexlimivv 3193 |
. . . 4
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โ ((๐ง โ โค โง ๐ค โ โ) โ (๐ต = (๐ง / ๐ค) โ (๐ด + ๐ต) โ โ))) |
39 | 38 | rexlimdvv 3201 |
. . 3
โข
(โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โ (โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค) โ (๐ด + ๐ต) โ โ)) |
40 | 39 | imp 408 |
. 2
โข
((โ๐ฅ โ
โค โ๐ฆ โ
โ ๐ด = (๐ฅ / ๐ฆ) โง โ๐ง โ โค โ๐ค โ โ ๐ต = (๐ง / ๐ค)) โ (๐ด + ๐ต) โ โ) |
41 | 1, 2, 40 | syl2anb 599 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |