Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | div1d.1 | |- ( ph -> A e. CC ) |
|
divcld.2 | |- ( ph -> B e. CC ) |
||
divmuld.3 | |- ( ph -> C e. CC ) |
||
divmuldivd.4 | |- ( ph -> D e. CC ) |
||
divmuldivd.5 | |- ( ph -> B =/= 0 ) |
||
divmuldivd.6 | |- ( ph -> D =/= 0 ) |
||
divdivdivd.7 | |- ( ph -> C =/= 0 ) |
||
Assertion | divdivdivd | |- ( ph -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | div1d.1 | |- ( ph -> A e. CC ) |
|
2 | divcld.2 | |- ( ph -> B e. CC ) |
|
3 | divmuld.3 | |- ( ph -> C e. CC ) |
|
4 | divmuldivd.4 | |- ( ph -> D e. CC ) |
|
5 | divmuldivd.5 | |- ( ph -> B =/= 0 ) |
|
6 | divmuldivd.6 | |- ( ph -> D =/= 0 ) |
|
7 | divdivdivd.7 | |- ( ph -> C =/= 0 ) |
|
8 | 2 5 | jca | |- ( ph -> ( B e. CC /\ B =/= 0 ) ) |
9 | 3 7 | jca | |- ( ph -> ( C e. CC /\ C =/= 0 ) ) |
10 | 4 6 | jca | |- ( ph -> ( D e. CC /\ D =/= 0 ) ) |
11 | divdivdiv | |- ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) ) |
|
12 | 1 8 9 10 11 | syl22anc | |- ( ph -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) ) |