Proof of Theorem xdivrec
Step | Hyp | Ref
| Expression |
1 | | simp2 1139 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ∈
ℝ) |
2 | 1 | rexrd 10883 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ∈
ℝ*) |
3 | | simp1 1138 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐴 ∈
ℝ*) |
4 | | 1xr 10892 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → 1
∈ ℝ*) |
6 | | simp3 1140 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ≠ 0) |
7 | 5, 1, 6 | xdivcld 30917 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → (1
/𝑒 𝐵)
∈ ℝ*) |
8 | 3, 7 | xmulcld 12892 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e (1
/𝑒 𝐵))
∈ ℝ*) |
9 | | xmulcom 12856 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ (𝐴
·e (1 /𝑒 𝐵)) ∈ ℝ*) → (𝐵 ·e (𝐴 ·e (1
/𝑒 𝐵)))
= ((𝐴 ·e
(1 /𝑒 𝐵)) ·e 𝐵)) |
10 | 2, 8, 9 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= ((𝐴 ·e
(1 /𝑒 𝐵)) ·e 𝐵)) |
11 | | xmulass 12877 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (1 /𝑒 𝐵) ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ((𝐴
·e (1 /𝑒 𝐵)) ·e 𝐵) = (𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵))) |
12 | 3, 7, 2, 11 | syl3anc 1373 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
((𝐴 ·e (1
/𝑒 𝐵))
·e 𝐵) =
(𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵))) |
13 | | xmulcom 12856 |
. . . . . . 7
⊢ (((1
/𝑒 𝐵)
∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((1
/𝑒 𝐵)
·e 𝐵) =
(𝐵 ·e (1
/𝑒 𝐵))) |
14 | 7, 2, 13 | syl2anc 587 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵)
·e 𝐵) =
(𝐵 ·e (1
/𝑒 𝐵))) |
15 | | eqid 2737 |
. . . . . . 7
⊢ (1
/𝑒 𝐵) =
(1 /𝑒 𝐵) |
16 | | xdivmul 30919 |
. . . . . . . 8
⊢ ((1
∈ ℝ* ∧ (1 /𝑒 𝐵) ∈ ℝ* ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → ((1
/𝑒 𝐵) =
(1 /𝑒 𝐵)
↔ (𝐵
·e (1 /𝑒 𝐵)) = 1)) |
17 | 5, 7, 1, 6, 16 | syl112anc 1376 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵) =
(1 /𝑒 𝐵)
↔ (𝐵
·e (1 /𝑒 𝐵)) = 1)) |
18 | 15, 17 | mpbii 236 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e (1
/𝑒 𝐵)) =
1) |
19 | 14, 18 | eqtrd 2777 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵)
·e 𝐵) =
1) |
20 | 19 | oveq2d 7229 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵)) =
(𝐴 ·e
1)) |
21 | 10, 12, 20 | 3eqtrd 2781 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= (𝐴 ·e
1)) |
22 | | xmulid1 12869 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 1) = 𝐴) |
23 | 3, 22 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e 1)
= 𝐴) |
24 | 21, 23 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= 𝐴) |
25 | | xdivmul 30919 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐴
·e (1 /𝑒 𝐵)) ∈ ℝ* ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → ((𝐴 /𝑒 𝐵) = (𝐴 ·e (1
/𝑒 𝐵))
↔ (𝐵
·e (𝐴
·e (1 /𝑒 𝐵))) = 𝐴)) |
26 | 3, 8, 1, 6, 25 | syl112anc 1376 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
((𝐴 /𝑒
𝐵) = (𝐴 ·e (1
/𝑒 𝐵))
↔ (𝐵
·e (𝐴
·e (1 /𝑒 𝐵))) = 𝐴)) |
27 | 24, 26 | mpbird 260 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 /𝑒
𝐵) = (𝐴 ·e (1
/𝑒 𝐵))) |