Metamath Proof Explorer

Theorem renegclALT

Description: Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl . (Contributed by NM, 15-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion renegclALT ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 negeq ⊢ ( 𝑥 = 𝐴 → - 𝑥 = - 𝐴 )
2 1 eleq1d ⊢ ( 𝑥 = 𝐴 → ( - 𝑥 ∈ ℝ ↔ - 𝐴 ∈ ℝ ) )
3 vex ⊢ 𝑥 ∈ V
4 c0ex ⊢ 0 ∈ V
5 3 4 ifex ⊢ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ V
6 csbnegg ⊢ ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ V → ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ - 𝑥 = - ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥 )
7 5 6 ax-mp ⊢ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ - 𝑥 = - ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥
8 csbvarg ⊢ ( 0 ∈ V → ⦋ 0 / 𝑥 ⦌ 𝑥 = 0 )
9 4 8 ax-mp ⊢ ⦋ 0 / 𝑥 ⦌ 𝑥 = 0
10 0re ⊢ 0 ∈ ℝ
11 9 10 eqeltri ⊢ ⦋ 0 / 𝑥 ⦌ 𝑥 ∈ ℝ
12 sbcel1g ⊢ ( 0 ∈ V → ( [ 0 / 𝑥 ] 𝑥 ∈ ℝ ↔ ⦋ 0 / 𝑥 ⦌ 𝑥 ∈ ℝ ) )
13 4 12 ax-mp ⊢ ( [ 0 / 𝑥 ] 𝑥 ∈ ℝ ↔ ⦋ 0 / 𝑥 ⦌ 𝑥 ∈ ℝ )
14 11 13 mpbir ⊢ [ 0 / 𝑥 ] 𝑥 ∈ ℝ
15 14 elimhyps ⊢ [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] 𝑥 ∈ ℝ
16 sbcel1g ⊢ ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ V → ( [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] 𝑥 ∈ ℝ ↔ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥 ∈ ℝ ) )
17 5 16 ax-mp ⊢ ( [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] 𝑥 ∈ ℝ ↔ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥 ∈ ℝ )
18 15 17 mpbi ⊢ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥 ∈ ℝ
19 18 renegcli ⊢ - ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ 𝑥 ∈ ℝ
20 7 19 eqeltri ⊢ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ - 𝑥 ∈ ℝ
21 sbcel1g ⊢ ( if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) ∈ V → ( [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] - 𝑥 ∈ ℝ ↔ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ - 𝑥 ∈ ℝ ) )
22 5 21 ax-mp ⊢ ( [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] - 𝑥 ∈ ℝ ↔ ⦋ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ⦌ - 𝑥 ∈ ℝ )
23 20 22 mpbir ⊢ [ if ( 𝑥 ∈ ℝ , 𝑥 , 0 ) / 𝑥 ] - 𝑥 ∈ ℝ
24 23 dedths ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
25 2 24 vtoclga ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )