Metamath Proof Explorer


Theorem xmulasslem

Description: Lemma for xmulass . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xmulasslem.1 ( 𝑥 = 𝐷 → ( 𝜓𝑋 = 𝑌 ) )
xmulasslem.2 ( 𝑥 = -𝑒 𝐷 → ( 𝜓𝐸 = 𝐹 ) )
xmulasslem.x ( 𝜑𝑋 ∈ ℝ* )
xmulasslem.y ( 𝜑𝑌 ∈ ℝ* )
xmulasslem.d ( 𝜑𝐷 ∈ ℝ* )
xmulasslem.ps ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ) ) → 𝜓 )
xmulasslem.0 ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) )
xmulasslem.e ( 𝜑𝐸 = -𝑒 𝑋 )
xmulasslem.f ( 𝜑𝐹 = -𝑒 𝑌 )
Assertion xmulasslem ( 𝜑𝑋 = 𝑌 )

Proof

Step Hyp Ref Expression
1 xmulasslem.1 ( 𝑥 = 𝐷 → ( 𝜓𝑋 = 𝑌 ) )
2 xmulasslem.2 ( 𝑥 = -𝑒 𝐷 → ( 𝜓𝐸 = 𝐹 ) )
3 xmulasslem.x ( 𝜑𝑋 ∈ ℝ* )
4 xmulasslem.y ( 𝜑𝑌 ∈ ℝ* )
5 xmulasslem.d ( 𝜑𝐷 ∈ ℝ* )
6 xmulasslem.ps ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ* ∧ 0 < 𝑥 ) ) → 𝜓 )
7 xmulasslem.0 ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) )
8 xmulasslem.e ( 𝜑𝐸 = -𝑒 𝑋 )
9 xmulasslem.f ( 𝜑𝐹 = -𝑒 𝑌 )
10 0xr 0 ∈ ℝ*
11 xrltso < Or ℝ*
12 solin ( ( < Or ℝ* ∧ ( 𝐷 ∈ ℝ* ∧ 0 ∈ ℝ* ) ) → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
13 11 12 mpan ( ( 𝐷 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
14 5 10 13 sylancl ( 𝜑 → ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) )
15 xlt0neg1 ( 𝐷 ∈ ℝ* → ( 𝐷 < 0 ↔ 0 < -𝑒 𝐷 ) )
16 5 15 syl ( 𝜑 → ( 𝐷 < 0 ↔ 0 < -𝑒 𝐷 ) )
17 xnegcl ( 𝐷 ∈ ℝ* → -𝑒 𝐷 ∈ ℝ* )
18 5 17 syl ( 𝜑 → -𝑒 𝐷 ∈ ℝ* )
19 breq2 ( 𝑥 = -𝑒 𝐷 → ( 0 < 𝑥 ↔ 0 < -𝑒 𝐷 ) )
20 19 2 imbi12d ( 𝑥 = -𝑒 𝐷 → ( ( 0 < 𝑥𝜓 ) ↔ ( 0 < -𝑒 𝐷𝐸 = 𝐹 ) ) )
21 20 imbi2d ( 𝑥 = -𝑒 𝐷 → ( ( 𝜑 → ( 0 < 𝑥𝜓 ) ) ↔ ( 𝜑 → ( 0 < -𝑒 𝐷𝐸 = 𝐹 ) ) ) )
22 6 exp32 ( 𝜑 → ( 𝑥 ∈ ℝ* → ( 0 < 𝑥𝜓 ) ) )
23 22 com12 ( 𝑥 ∈ ℝ* → ( 𝜑 → ( 0 < 𝑥𝜓 ) ) )
24 21 23 vtoclga ( -𝑒 𝐷 ∈ ℝ* → ( 𝜑 → ( 0 < -𝑒 𝐷𝐸 = 𝐹 ) ) )
25 18 24 mpcom ( 𝜑 → ( 0 < -𝑒 𝐷𝐸 = 𝐹 ) )
26 16 25 sylbid ( 𝜑 → ( 𝐷 < 0 → 𝐸 = 𝐹 ) )
27 8 9 eqeq12d ( 𝜑 → ( 𝐸 = 𝐹 ↔ -𝑒 𝑋 = -𝑒 𝑌 ) )
28 xneg11 ( ( 𝑋 ∈ ℝ*𝑌 ∈ ℝ* ) → ( -𝑒 𝑋 = -𝑒 𝑌𝑋 = 𝑌 ) )
29 3 4 28 syl2anc ( 𝜑 → ( -𝑒 𝑋 = -𝑒 𝑌𝑋 = 𝑌 ) )
30 27 29 bitrd ( 𝜑 → ( 𝐸 = 𝐹𝑋 = 𝑌 ) )
31 26 30 sylibd ( 𝜑 → ( 𝐷 < 0 → 𝑋 = 𝑌 ) )
32 eqeq1 ( 𝑥 = 𝐷 → ( 𝑥 = 0 ↔ 𝐷 = 0 ) )
33 32 1 imbi12d ( 𝑥 = 𝐷 → ( ( 𝑥 = 0 → 𝜓 ) ↔ ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) )
34 33 imbi2d ( 𝑥 = 𝐷 → ( ( 𝜑 → ( 𝑥 = 0 → 𝜓 ) ) ↔ ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) ) )
35 34 7 vtoclg ( 𝐷 ∈ ℝ* → ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) ) )
36 5 35 mpcom ( 𝜑 → ( 𝐷 = 0 → 𝑋 = 𝑌 ) )
37 breq2 ( 𝑥 = 𝐷 → ( 0 < 𝑥 ↔ 0 < 𝐷 ) )
38 37 1 imbi12d ( 𝑥 = 𝐷 → ( ( 0 < 𝑥𝜓 ) ↔ ( 0 < 𝐷𝑋 = 𝑌 ) ) )
39 38 imbi2d ( 𝑥 = 𝐷 → ( ( 𝜑 → ( 0 < 𝑥𝜓 ) ) ↔ ( 𝜑 → ( 0 < 𝐷𝑋 = 𝑌 ) ) ) )
40 39 23 vtoclga ( 𝐷 ∈ ℝ* → ( 𝜑 → ( 0 < 𝐷𝑋 = 𝑌 ) ) )
41 5 40 mpcom ( 𝜑 → ( 0 < 𝐷𝑋 = 𝑌 ) )
42 31 36 41 3jaod ( 𝜑 → ( ( 𝐷 < 0 ∨ 𝐷 = 0 ∨ 0 < 𝐷 ) → 𝑋 = 𝑌 ) )
43 14 42 mpd ( 𝜑𝑋 = 𝑌 )