Proof of Theorem xdivrec
Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ∈
ℝ) |
2 | 1 | rexrd 9968 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ∈
ℝ*) |
3 | | simp1 1054 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐴 ∈
ℝ*) |
4 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
5 | 4 | rexri 9976 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → 1
∈ ℝ*) |
7 | | simp3 1056 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
𝐵 ≠ 0) |
8 | 6, 1, 7 | xdivcld 28962 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → (1
/𝑒 𝐵)
∈ ℝ*) |
9 | 3, 8 | xmulcld 12004 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e (1
/𝑒 𝐵))
∈ ℝ*) |
10 | | xmulcom 11968 |
. . . . 5
⊢ ((𝐵 ∈ ℝ*
∧ (𝐴
·e (1 /𝑒 𝐵)) ∈ ℝ*) → (𝐵 ·e (𝐴 ·e (1
/𝑒 𝐵)))
= ((𝐴 ·e
(1 /𝑒 𝐵)) ·e 𝐵)) |
11 | 2, 9, 10 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= ((𝐴 ·e
(1 /𝑒 𝐵)) ·e 𝐵)) |
12 | | xmulass 11989 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (1 /𝑒 𝐵) ∈ ℝ* ∧ 𝐵 ∈ ℝ*)
→ ((𝐴
·e (1 /𝑒 𝐵)) ·e 𝐵) = (𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵))) |
13 | 3, 8, 2, 12 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
((𝐴 ·e (1
/𝑒 𝐵))
·e 𝐵) =
(𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵))) |
14 | | xmulcom 11968 |
. . . . . . 7
⊢ (((1
/𝑒 𝐵)
∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((1
/𝑒 𝐵)
·e 𝐵) =
(𝐵 ·e (1
/𝑒 𝐵))) |
15 | 8, 2, 14 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵)
·e 𝐵) =
(𝐵 ·e (1
/𝑒 𝐵))) |
16 | | eqid 2610 |
. . . . . . 7
⊢ (1
/𝑒 𝐵) =
(1 /𝑒 𝐵) |
17 | | xdivmul 28964 |
. . . . . . . 8
⊢ ((1
∈ ℝ* ∧ (1 /𝑒 𝐵) ∈ ℝ* ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → ((1
/𝑒 𝐵) =
(1 /𝑒 𝐵)
↔ (𝐵
·e (1 /𝑒 𝐵)) = 1)) |
18 | 6, 8, 1, 7, 17 | syl112anc 1322 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵) =
(1 /𝑒 𝐵)
↔ (𝐵
·e (1 /𝑒 𝐵)) = 1)) |
19 | 16, 18 | mpbii 222 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e (1
/𝑒 𝐵)) =
1) |
20 | 15, 19 | eqtrd 2644 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) → ((1
/𝑒 𝐵)
·e 𝐵) =
1) |
21 | 20 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e ((1
/𝑒 𝐵)
·e 𝐵)) =
(𝐴 ·e
1)) |
22 | 11, 13, 21 | 3eqtrd 2648 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= (𝐴 ·e
1)) |
23 | | xmulid1 11981 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 1) = 𝐴) |
24 | 3, 23 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 ·e 1)
= 𝐴) |
25 | 22, 24 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐵 ·e
(𝐴 ·e (1
/𝑒 𝐵)))
= 𝐴) |
26 | | xdivmul 28964 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ (𝐴
·e (1 /𝑒 𝐵)) ∈ ℝ* ∧ (𝐵 ∈ ℝ ∧ 𝐵 ≠ 0)) → ((𝐴 /𝑒 𝐵) = (𝐴 ·e (1
/𝑒 𝐵))
↔ (𝐵
·e (𝐴
·e (1 /𝑒 𝐵))) = 𝐴)) |
27 | 3, 9, 1, 7, 26 | syl112anc 1322 |
. 2
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
((𝐴 /𝑒
𝐵) = (𝐴 ·e (1
/𝑒 𝐵))
↔ (𝐵
·e (𝐴
·e (1 /𝑒 𝐵))) = 𝐴)) |
28 | 25, 27 | mpbird 246 |
1
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 /𝑒
𝐵) = (𝐴 ·e (1
/𝑒 𝐵))) |