Theorem axrnegex

Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex . (Contributed by NM, 15-May-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	axrnegex	$$⊢A\in ℝ\to \exists x\in ℝA+x=0$$

Proof

Step	Hyp	Ref	Expression
1		elreal2	$$⊢A\in ℝ\leftrightarrow \left(1^{st}\left(A\right)\in 𝑹\wedge A=⟨1^{st}\left(A\right),0_{𝑹}⟩\right)$$
2	1	simplbi	$$⊢A\in ℝ\to 1^{st}\left(A\right)\in 𝑹$$
3		m1r	$$⊢{-1}_{𝑹}\in 𝑹$$
4		mulclsr	$$⊢\left(1^{st}\left(A\right)\in 𝑹\wedge {-1}_{𝑹}\in 𝑹\right)\to 1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹$$
5	2 3 4	sylancl	$$⊢A\in ℝ\to 1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹$$
6		opelreal	$$⊢⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩\in ℝ\leftrightarrow 1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹$$
7	5 6	sylibr	$$⊢A\in ℝ\to ⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩\in ℝ$$
8	1	simprbi	$$⊢A\in ℝ\to A=⟨1^{st}\left(A\right),0_{𝑹}⟩$$
9	8	oveq1d	$$⊢A\in ℝ\to A+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=⟨1^{st}\left(A\right),0_{𝑹}⟩+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩$$
10		addresr	$$⊢\left(1^{st}\left(A\right)\in 𝑹\wedge 1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\in 𝑹\right)\to ⟨1^{st}\left(A\right),0_{𝑹}⟩+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=⟨1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right),0_{𝑹}⟩$$
11	2 5 10	syl2anc	$$⊢A\in ℝ\to ⟨1^{st}\left(A\right),0_{𝑹}⟩+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=⟨1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right),0_{𝑹}⟩$$
12		pn0sr	$$⊢1^{st}\left(A\right)\in 𝑹\to 1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right)=0_{𝑹}$$
13	12	opeq1d	$$⊢1^{st}\left(A\right)\in 𝑹\to ⟨1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right),0_{𝑹}⟩=⟨0_{𝑹},0_{𝑹}⟩$$
14		df-0	$$⊢0=⟨0_{𝑹},0_{𝑹}⟩$$
15	13 14	eqtr4di	$$⊢1^{st}\left(A\right)\in 𝑹\to ⟨1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right),0_{𝑹}⟩=0$$
16	2 15	syl	$$⊢A\in ℝ\to ⟨1^{st}\left(A\right){+}_{𝑹}\left(1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹}\right),0_{𝑹}⟩=0$$
17	9 11 16	3eqtrd	$$⊢A\in ℝ\to A+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=0$$
18		oveq2	$$⊢x=⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩\to A+x=A+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩$$
19	18	eqeq1d	$$⊢x=⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩\to \left(A+x=0\leftrightarrow A+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=0\right)$$
20	19	rspcev	$$⊢\left(⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩\in ℝ\wedge A+⟨1^{st}\left(A\right){\cdot }_{𝑹}{-1}_{𝑹},0_{𝑹}⟩=0\right)\to \exists x\in ℝA+x=0$$
21	7 17 20	syl2anc	$$⊢A\in ℝ\to \exists x\in ℝA+x=0$$