Step |
Hyp |
Ref |
Expression |
1 |
|
mulcl |
|- ( ( A e. CC /\ D e. CC ) -> ( A x. D ) e. CC ) |
2 |
1
|
ad2ant2r |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( A x. D ) e. CC ) |
3 |
2
|
adantrl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) e. CC ) |
4 |
|
mulcl |
|- ( ( B e. CC /\ C e. CC ) -> ( B x. C ) e. CC ) |
5 |
4
|
adantrr |
|- ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B x. C ) e. CC ) |
6 |
5
|
ad2ant2lr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) e. CC ) |
7 |
|
mulcl |
|- ( ( C e. CC /\ D e. CC ) -> ( C x. D ) e. CC ) |
8 |
7
|
ad2ant2r |
|- ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) e. CC ) |
9 |
|
mulne0 |
|- ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( C x. D ) =/= 0 ) |
10 |
8 9
|
jca |
|- ( ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) ) |
11 |
10
|
adantl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) ) |
12 |
|
divdir |
|- ( ( ( A x. D ) e. CC /\ ( B x. C ) e. CC /\ ( ( C x. D ) e. CC /\ ( C x. D ) =/= 0 ) ) -> ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) = ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) ) |
13 |
3 6 11 12
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) = ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) ) |
14 |
|
simpll |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> A e. CC ) |
15 |
|
simprr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( D e. CC /\ D =/= 0 ) ) |
16 |
15
|
simpld |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> D e. CC ) |
17 |
14 16
|
mulcomd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( A x. D ) = ( D x. A ) ) |
18 |
|
simprll |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> C e. CC ) |
19 |
18 16
|
mulcomd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C x. D ) = ( D x. C ) ) |
20 |
17 19
|
oveq12d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) / ( C x. D ) ) = ( ( D x. A ) / ( D x. C ) ) ) |
21 |
|
simprl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( C e. CC /\ C =/= 0 ) ) |
22 |
|
divcan5 |
|- ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) -> ( ( D x. A ) / ( D x. C ) ) = ( A / C ) ) |
23 |
14 21 15 22
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( D x. A ) / ( D x. C ) ) = ( A / C ) ) |
24 |
20 23
|
eqtrd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A x. D ) / ( C x. D ) ) = ( A / C ) ) |
25 |
|
simplr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> B e. CC ) |
26 |
25 18
|
mulcomd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( B x. C ) = ( C x. B ) ) |
27 |
26
|
oveq1d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B x. C ) / ( C x. D ) ) = ( ( C x. B ) / ( C x. D ) ) ) |
28 |
|
divcan5 |
|- ( ( B e. CC /\ ( D e. CC /\ D =/= 0 ) /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) / ( C x. D ) ) = ( B / D ) ) |
29 |
25 15 21 28
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( C x. B ) / ( C x. D ) ) = ( B / D ) ) |
30 |
27 29
|
eqtrd |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( B x. C ) / ( C x. D ) ) = ( B / D ) ) |
31 |
24 30
|
oveq12d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( ( A x. D ) / ( C x. D ) ) + ( ( B x. C ) / ( C x. D ) ) ) = ( ( A / C ) + ( B / D ) ) ) |
32 |
13 31
|
eqtr2d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / C ) + ( B / D ) ) = ( ( ( A x. D ) + ( B x. C ) ) / ( C x. D ) ) ) |