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	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		elreal2	⊢ ( 𝐴 ∈ ℝ ↔ ( ( 1^st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ ) )
2	1	simplbi	⊢ ( 𝐴 ∈ ℝ → ( 1^st ‘ 𝐴 ) ∈ R )
3		m1r	⊢ -1_R ∈ R
4		mulclsr	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ R ∧ -1_R ∈ R ) → ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ∈ R )
5	2 3 4	sylancl	⊢ ( 𝐴 ∈ ℝ → ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ∈ R )
6		opelreal	⊢ ( ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ∈ ℝ ↔ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ∈ R )
7	5 6	sylibr	⊢ ( 𝐴 ∈ ℝ → ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ∈ ℝ )
8	1	simprbi	⊢ ( 𝐴 ∈ ℝ → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ )
9	8	oveq1d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = ( ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) )
10		addresr	⊢ ( ( ( 1^st ‘ 𝐴 ) ∈ R ∧ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ∈ R ) → ( ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = ⟨ ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) , 0_R ⟩ )
11	2 5 10	syl2anc	⊢ ( 𝐴 ∈ ℝ → ( ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = ⟨ ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) , 0_R ⟩ )
12		pn0sr	⊢ ( ( 1^st ‘ 𝐴 ) ∈ R → ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) = 0_R )
13	12	opeq1d	⊢ ( ( 1^st ‘ 𝐴 ) ∈ R → ⟨ ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) , 0_R ⟩ = ⟨ 0_R , 0_R ⟩ )
14		df-0	⊢ 0 = ⟨ 0_R , 0_R ⟩
15	13 14	eqtr4di	⊢ ( ( 1^st ‘ 𝐴 ) ∈ R → ⟨ ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) , 0_R ⟩ = 0 )
16	2 15	syl	⊢ ( 𝐴 ∈ ℝ → ⟨ ( ( 1^st ‘ 𝐴 ) +_R ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) ) , 0_R ⟩ = 0 )
17	9 11 16	3eqtrd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = 0 )
18		oveq2	⊢ ( 𝑥 = ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ → ( 𝐴 + 𝑥 ) = ( 𝐴 + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) )
19	18	eqeq1d	⊢ ( 𝑥 = ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ → ( ( 𝐴 + 𝑥 ) = 0 ↔ ( 𝐴 + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = 0 ) )
20	19	rspcev	⊢ ( ( ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ∈ ℝ ∧ ( 𝐴 + ⟨ ( ( 1^st ‘ 𝐴 ) ·_R -1_R ) , 0_R ⟩ ) = 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )
21	7 17 20	syl2anc	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )

Metamath Proof Explorer

Theorem axrnegex

Proof