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

Metamath Proof Explorer

Theorem sn-negex12

Description: A combination of cnegex and cnegex2 , this proof takes cnre A = r +i x. s and shows that i x. -u s + -u r is both a left and right inverse. (Contributed by SN, 5-May-2024) (Proof shortened by SN, 4-Jul-2025)

Ref Expression
Assertion sn-negex12 ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 cnre ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2 oveq2 ⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
3 2 eqeq1d ⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ↔ ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ) )
4 oveq1 ⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) )
5 4 eqeq1d ⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ↔ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
6 3 5 anbi12d ⊢ ( 𝑏 = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) → ( ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ∧ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) ↔ ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ∧ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) ) )
7 ax-icn ⊢ i ∈ ℂ
8 7 a1i ⊢ ( 𝑦 ∈ ℝ → i ∈ ℂ )
9 rernegcl ⊢ ( 𝑦 ∈ ℝ → ( 0 −ℝ 𝑦 ) ∈ ℝ )
10 9 recnd ⊢ ( 𝑦 ∈ ℝ → ( 0 −ℝ 𝑦 ) ∈ ℂ )
11 8 10 mulcld ⊢ ( 𝑦 ∈ ℝ → ( i · ( 0 −ℝ 𝑦 ) ) ∈ ℂ )
12 11 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · ( 0 −ℝ 𝑦 ) ) ∈ ℂ )
13 rernegcl ⊢ ( 𝑥 ∈ ℝ → ( 0 −ℝ 𝑥 ) ∈ ℝ )
14 13 recnd ⊢ ( 𝑥 ∈ ℝ → ( 0 −ℝ 𝑥 ) ∈ ℂ )
15 14 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 −ℝ 𝑥 ) ∈ ℂ )
16 12 15 addcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ∈ ℂ )
17 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
18 17 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℂ )
19 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
20 8 19 mulcld ⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∈ ℂ )
21 20 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) ∈ ℂ )
22 18 21 12 addassd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = ( 𝑥 + ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) ) )
23 8 19 10 adddid ⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 + ( 0 −ℝ 𝑦 ) ) ) = ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) )
24 renegid ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + ( 0 −ℝ 𝑦 ) ) = 0 )
25 24 oveq2d ⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 + ( 0 −ℝ 𝑦 ) ) ) = ( i · 0 ) )
26 sn-it0e0 ⊢ ( i · 0 ) = 0
27 25 26 eqtrdi ⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 + ( 0 −ℝ 𝑦 ) ) ) = 0 )
28 23 27 eqtr3d ⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 0 )
29 28 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 0 )
30 29 oveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( ( i · 𝑦 ) + ( i · ( 0 −ℝ 𝑦 ) ) ) ) = ( 𝑥 + 0 ) )
31 readdrid ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 0 ) = 𝑥 )
32 31 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + 0 ) = 𝑥 )
33 22 30 32 3eqtrd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) = 𝑥 )
34 33 oveq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) + ( 0 −ℝ 𝑥 ) ) = ( 𝑥 + ( 0 −ℝ 𝑥 ) ) )
35 18 21 addcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
36 35 12 15 addassd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( i · ( 0 −ℝ 𝑦 ) ) ) + ( 0 −ℝ 𝑥 ) ) = ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) )
37 renegid ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + ( 0 −ℝ 𝑥 ) ) = 0 )
38 37 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( 0 −ℝ 𝑥 ) ) = 0 )
39 34 36 38 3eqtr3d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 )
40 12 15 35 addassd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) ) )
41 renegid2 ⊢ ( 𝑥 ∈ ℝ → ( ( 0 −ℝ 𝑥 ) + 𝑥 ) = 0 )
42 41 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 0 −ℝ 𝑥 ) + 𝑥 ) = 0 )
43 42 oveq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) = ( 0 + ( i · 𝑦 ) ) )
44 15 18 21 addassd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 0 −ℝ 𝑥 ) + 𝑥 ) + ( i · 𝑦 ) ) = ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) )
45 sn-addlid ⊢ ( ( i · 𝑦 ) ∈ ℂ → ( 0 + ( i · 𝑦 ) ) = ( i · 𝑦 ) )
46 21 45 syl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 0 + ( i · 𝑦 ) ) = ( i · 𝑦 ) )
47 43 44 46 3eqtr3rd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) = ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) )
48 47 oveq2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( ( 0 −ℝ 𝑥 ) + ( 𝑥 + ( i · 𝑦 ) ) ) ) )
49 8 10 19 adddid ⊢ ( 𝑦 ∈ ℝ → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) )
50 renegid2 ⊢ ( 𝑦 ∈ ℝ → ( ( 0 −ℝ 𝑦 ) + 𝑦 ) = 0 )
51 50 oveq2d ⊢ ( 𝑦 ∈ ℝ → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = ( i · 0 ) )
52 51 26 eqtrdi ⊢ ( 𝑦 ∈ ℝ → ( i · ( ( 0 −ℝ 𝑦 ) + 𝑦 ) ) = 0 )
53 49 52 eqtr3d ⊢ ( 𝑦 ∈ ℝ → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) = 0 )
54 53 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( i · ( 0 −ℝ 𝑦 ) ) + ( i · 𝑦 ) ) = 0 )
55 40 48 54 3eqtr2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 )
56 39 55 jca ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( i · 𝑦 ) ) + ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) ) = 0 ∧ ( ( ( i · ( 0 −ℝ 𝑦 ) ) + ( 0 −ℝ 𝑥 ) ) + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
57 6 16 56 rspcedvdw ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ∃ 𝑏 ∈ ℂ ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ∧ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
58 57 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ∃ 𝑏 ∈ ℂ ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ∧ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
59 oveq1 ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 + 𝑏 ) = ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) )
60 59 eqeq1d ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐴 + 𝑏 ) = 0 ↔ ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ) )
61 oveq2 ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝑏 + 𝐴 ) = ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) )
62 61 eqeq1d ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝑏 + 𝐴 ) = 0 ↔ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) )
63 60 62 anbi12d ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ↔ ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ∧ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) ) )
64 63 rexbidv ⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ↔ ∃ 𝑏 ∈ ℂ ( ( ( 𝑥 + ( i · 𝑦 ) ) + 𝑏 ) = 0 ∧ ( 𝑏 + ( 𝑥 + ( i · 𝑦 ) ) ) = 0 ) ) )
65 58 64 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
66 65 rexlimdvva ⊢ ( 𝐴 ∈ ℂ → ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) ) )
67 1 66 mpd ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐴 + 𝑏 ) = 0 ∧ ( 𝑏 + 𝐴 ) = 0 ) )