This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem receu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by NM, 29-Jan-1995) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion receu ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 recex ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℂ ( 𝐵 · 𝑦 ) = 1 )
2 1 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑦 ∈ ℂ ( 𝐵 · 𝑦 ) = 1 )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℂ )
4 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝐴 ∈ ℂ )
5 3 4 mulcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 𝑦 · 𝐴 ) ∈ ℂ )
6 oveq1 ⊢ ( ( 𝐵 · 𝑦 ) = 1 → ( ( 𝐵 · 𝑦 ) · 𝐴 ) = ( 1 · 𝐴 ) )
7 6 ad2antll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( ( 𝐵 · 𝑦 ) · 𝐴 ) = ( 1 · 𝐴 ) )
8 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → 𝐵 ∈ ℂ )
9 8 3 4 mulassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( ( 𝐵 · 𝑦 ) · 𝐴 ) = ( 𝐵 · ( 𝑦 · 𝐴 ) ) )
10 4 mullidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 1 · 𝐴 ) = 𝐴 )
11 7 9 10 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ( 𝐵 · ( 𝑦 · 𝐴 ) ) = 𝐴 )
12 oveq2 ⊢ ( 𝑥 = ( 𝑦 · 𝐴 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( 𝑦 · 𝐴 ) ) )
13 12 eqeq1d ⊢ ( 𝑥 = ( 𝑦 · 𝐴 ) → ( ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · ( 𝑦 · 𝐴 ) ) = 𝐴 ) )
14 13 rspcev ⊢ ( ( ( 𝑦 · 𝐴 ) ∈ ℂ ∧ ( 𝐵 · ( 𝑦 · 𝐴 ) ) = 𝐴 ) → ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
15 5 11 14 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝐵 · 𝑦 ) = 1 ) ) → ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
16 15 rexlimdvaa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑦 ∈ ℂ ( 𝐵 · 𝑦 ) = 1 → ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ∃ 𝑦 ∈ ℂ ( 𝐵 · 𝑦 ) = 1 → ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ) )
18 2 17 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )
19 eqtr3 ⊢ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) )
20 mulcan ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) ↔ 𝑥 = 𝑦 ) )
21 19 20 imbitrid ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
22 21 3expa ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
23 22 expcom ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
24 23 3adant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
25 24 ralrimivv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) )
26 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) )
27 26 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( 𝐵 · 𝑦 ) = 𝐴 ) )
28 27 reu4 ⊢ ( ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ↔ ( ∃ 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( 𝐵 · 𝑥 ) = 𝐴 ∧ ( 𝐵 · 𝑦 ) = 𝐴 ) → 𝑥 = 𝑦 ) ) )
29 18 25 28 sylanbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ∃! 𝑥 ∈ ℂ ( 𝐵 · 𝑥 ) = 𝐴 )