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 ) ) ) |