Metamath Proof Explorer

Theorem divrec

Description: Relationship between division and reciprocal. Theorem I.9 of Apostol p. 18. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divrec ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B

Proof

Step Hyp Ref Expression
1 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
2 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
3 reccl ⊢ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 1 B ∈ ℂ
5 1 2 4 mul12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A ⁢ 1 B = A ⁢ B ⁢ 1 B
6 recid ⊢ B ∈ ℂ ∧ B ≠ 0 → B ⁢ 1 B = 1
7 6 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ 1 B = 1
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B ⁢ 1 B = A ⋅ 1
9 2 mulridd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⋅ 1 = A
10 5 8 9 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A ⁢ 1 B = A
11 2 4 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ 1 B ∈ ℂ
12 3simpc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ ∧ B ≠ 0
13 divmul ⊢ A ∈ ℂ ∧ A ⁢ 1 B ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B ↔ B ⁢ A ⁢ 1 B = A
14 2 11 12 13 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B ↔ B ⁢ A ⁢ 1 B = A
15 10 14 mpbird ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A ⁢ 1 B