Proof of Theorem xmulasslem
Step | Hyp | Ref
| Expression |
1 | | xmulasslem.d |
. . 3
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
2 | | 0xr 9965 |
. . 3
⊢ 0 ∈
ℝ* |
3 | | xrltso 11850 |
. . . 4
⊢ < Or
ℝ* |
4 | | solin 4982 |
. . . 4
⊢ (( <
Or ℝ* ∧ (𝐷 ∈ ℝ* ∧ 0 ∈
ℝ*)) → (𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷)) |
5 | 3, 4 | mpan 702 |
. . 3
⊢ ((𝐷 ∈ ℝ*
∧ 0 ∈ ℝ*) → (𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷)) |
6 | 1, 2, 5 | sylancl 693 |
. 2
⊢ (𝜑 → (𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷)) |
7 | | xlt0neg1 11924 |
. . . . . 6
⊢ (𝐷 ∈ ℝ*
→ (𝐷 < 0 ↔ 0
< -𝑒𝐷)) |
8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐷 < 0 ↔ 0 <
-𝑒𝐷)) |
9 | | xnegcl 11918 |
. . . . . . 7
⊢ (𝐷 ∈ ℝ*
→ -𝑒𝐷 ∈
ℝ*) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → -𝑒𝐷 ∈
ℝ*) |
11 | | breq2 4587 |
. . . . . . . . 9
⊢ (𝑥 = -𝑒𝐷 → (0 < 𝑥 ↔ 0 <
-𝑒𝐷)) |
12 | | xmulasslem.2 |
. . . . . . . . 9
⊢ (𝑥 = -𝑒𝐷 → (𝜓 ↔ 𝐸 = 𝐹)) |
13 | 11, 12 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑥 = -𝑒𝐷 → ((0 < 𝑥 → 𝜓) ↔ (0 < -𝑒𝐷 → 𝐸 = 𝐹))) |
14 | 13 | imbi2d 329 |
. . . . . . 7
⊢ (𝑥 = -𝑒𝐷 → ((𝜑 → (0 < 𝑥 → 𝜓)) ↔ (𝜑 → (0 < -𝑒𝐷 → 𝐸 = 𝐹)))) |
15 | | xmulasslem.ps |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ* ∧ 0 <
𝑥)) → 𝜓) |
16 | 15 | exp32 629 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ* → (0 <
𝑥 → 𝜓))) |
17 | 16 | com12 32 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ*
→ (𝜑 → (0 <
𝑥 → 𝜓))) |
18 | 14, 17 | vtoclga 3245 |
. . . . . 6
⊢
(-𝑒𝐷 ∈ ℝ* → (𝜑 → (0 <
-𝑒𝐷
→ 𝐸 = 𝐹))) |
19 | 10, 18 | mpcom 37 |
. . . . 5
⊢ (𝜑 → (0 <
-𝑒𝐷
→ 𝐸 = 𝐹)) |
20 | 8, 19 | sylbid 229 |
. . . 4
⊢ (𝜑 → (𝐷 < 0 → 𝐸 = 𝐹)) |
21 | | xmulasslem.e |
. . . . . 6
⊢ (𝜑 → 𝐸 = -𝑒𝑋) |
22 | | xmulasslem.f |
. . . . . 6
⊢ (𝜑 → 𝐹 = -𝑒𝑌) |
23 | 21, 22 | eqeq12d 2625 |
. . . . 5
⊢ (𝜑 → (𝐸 = 𝐹 ↔ -𝑒𝑋 = -𝑒𝑌)) |
24 | | xmulasslem.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
25 | | xmulasslem.y |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
26 | | xneg11 11920 |
. . . . . 6
⊢ ((𝑋 ∈ ℝ*
∧ 𝑌 ∈
ℝ*) → (-𝑒𝑋 = -𝑒𝑌 ↔ 𝑋 = 𝑌)) |
27 | 24, 25, 26 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
(-𝑒𝑋 =
-𝑒𝑌
↔ 𝑋 = 𝑌)) |
28 | 23, 27 | bitrd 267 |
. . . 4
⊢ (𝜑 → (𝐸 = 𝐹 ↔ 𝑋 = 𝑌)) |
29 | 20, 28 | sylibd 228 |
. . 3
⊢ (𝜑 → (𝐷 < 0 → 𝑋 = 𝑌)) |
30 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → (𝑥 = 0 ↔ 𝐷 = 0)) |
31 | | xmulasslem.1 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → (𝜓 ↔ 𝑋 = 𝑌)) |
32 | 30, 31 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝐷 → ((𝑥 = 0 → 𝜓) ↔ (𝐷 = 0 → 𝑋 = 𝑌))) |
33 | 32 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝐷 → ((𝜑 → (𝑥 = 0 → 𝜓)) ↔ (𝜑 → (𝐷 = 0 → 𝑋 = 𝑌)))) |
34 | | xmulasslem.0 |
. . . . 5
⊢ (𝜑 → (𝑥 = 0 → 𝜓)) |
35 | 33, 34 | vtoclg 3239 |
. . . 4
⊢ (𝐷 ∈ ℝ*
→ (𝜑 → (𝐷 = 0 → 𝑋 = 𝑌))) |
36 | 1, 35 | mpcom 37 |
. . 3
⊢ (𝜑 → (𝐷 = 0 → 𝑋 = 𝑌)) |
37 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = 𝐷 → (0 < 𝑥 ↔ 0 < 𝐷)) |
38 | 37, 31 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝐷 → ((0 < 𝑥 → 𝜓) ↔ (0 < 𝐷 → 𝑋 = 𝑌))) |
39 | 38 | imbi2d 329 |
. . . . 5
⊢ (𝑥 = 𝐷 → ((𝜑 → (0 < 𝑥 → 𝜓)) ↔ (𝜑 → (0 < 𝐷 → 𝑋 = 𝑌)))) |
40 | 39, 17 | vtoclga 3245 |
. . . 4
⊢ (𝐷 ∈ ℝ*
→ (𝜑 → (0 <
𝐷 → 𝑋 = 𝑌))) |
41 | 1, 40 | mpcom 37 |
. . 3
⊢ (𝜑 → (0 < 𝐷 → 𝑋 = 𝑌)) |
42 | 29, 36, 41 | 3jaod 1384 |
. 2
⊢ (𝜑 → ((𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷) → 𝑋 = 𝑌)) |
43 | 6, 42 | mpd 15 |
1
⊢ (𝜑 → 𝑋 = 𝑌) |