Description: Swap denominators in a division. (Contributed by NM, 15-Sep-1999)
Ref | Expression | ||
---|---|---|---|
Hypotheses | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
divclz.2 | ⊢ 𝐵 ∈ ℂ | ||
divmulz.3 | ⊢ 𝐶 ∈ ℂ | ||
Assertion | divdiv23zi | ⊢ ( ( 𝐵 ≠ 0 ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | divclz.1 | ⊢ 𝐴 ∈ ℂ | |
2 | divclz.2 | ⊢ 𝐵 ∈ ℂ | |
3 | divmulz.3 | ⊢ 𝐶 ∈ ℂ | |
4 | divdiv32 | ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) ) | |
5 | 1 4 | mp3an1 | ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) ) |
6 | 3 5 | mpanr1 | ⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) ) |
7 | 2 6 | mpanl1 | ⊢ ( ( 𝐵 ≠ 0 ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) / 𝐵 ) ) |