Metamath Proof Explorer

Theorem remul02

Description: Real number version of mul02 proven without ax-mulcom . (Contributed by SN, 23-Jan-2024)

Ref Expression
Assertion remul02 ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 sn-1ne2 ⊢ 1 ≠ 2
2 elre0re ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
3 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
4 2 3 remulcld ⊢ ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) ∈ ℝ )
5 ax-rrecex ⊢ ( ( ( 0 · 𝐴 ) ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 )
6 4 5 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 )
7 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 0 · 𝐴 ) · 𝑥 ) = 1 )
8 df-2 ⊢ 2 = ( 1 + 1 )
9 8 oveq1i ⊢ ( 2 · 0 ) = ( ( 1 + 1 ) · 0 )
10 re0m0e0 ⊢ ( 0 −ℝ 0 ) = 0
11 10 eqcomi ⊢ 0 = ( 0 −ℝ 0 )
12 11 oveq2i ⊢ ( ( 1 + 1 ) · 0 ) = ( ( 1 + 1 ) · ( 0 −ℝ 0 ) )
13 1re ⊢ 1 ∈ ℝ
14 13 13 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
15 sn-00idlem1 ⊢ ( ( 1 + 1 ) ∈ ℝ → ( ( 1 + 1 ) · ( 0 −ℝ 0 ) ) = ( ( 1 + 1 ) −ℝ ( 1 + 1 ) ) )
16 14 15 ax-mp ⊢ ( ( 1 + 1 ) · ( 0 −ℝ 0 ) ) = ( ( 1 + 1 ) −ℝ ( 1 + 1 ) )
17 repnpcan ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 + 1 ) −ℝ ( 1 + 1 ) ) = ( 1 −ℝ 1 ) )
18 13 13 13 17 mp3an ⊢ ( ( 1 + 1 ) −ℝ ( 1 + 1 ) ) = ( 1 −ℝ 1 )
19 re1m1e0m0 ⊢ ( 1 −ℝ 1 ) = ( 0 −ℝ 0 )
20 18 19 10 3eqtri ⊢ ( ( 1 + 1 ) −ℝ ( 1 + 1 ) ) = 0
21 12 16 20 3eqtri ⊢ ( ( 1 + 1 ) · 0 ) = 0
22 9 21 eqtr2i ⊢ 0 = ( 2 · 0 )
23 22 oveq1i ⊢ ( 0 · 𝐴 ) = ( ( 2 · 0 ) · 𝐴 )
24 23 oveq1i ⊢ ( ( 0 · 𝐴 ) · 𝑥 ) = ( ( ( 2 · 0 ) · 𝐴 ) · 𝑥 )
25 24 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 0 · 𝐴 ) · 𝑥 ) = ( ( ( 2 · 0 ) · 𝐴 ) · 𝑥 ) )
26 2cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 2 ∈ ℂ )
27 0cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 0 ∈ ℂ )
28 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
30 26 27 29 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 2 · 0 ) · 𝐴 ) = ( 2 · ( 0 · 𝐴 ) ) )
31 30 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( ( 2 · 0 ) · 𝐴 ) · 𝑥 ) = ( ( 2 · ( 0 · 𝐴 ) ) · 𝑥 ) )
32 4 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( 0 · 𝐴 ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( 0 · 𝐴 ) ∈ ℂ )
34 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
35 34 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
36 26 33 35 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 2 · ( 0 · 𝐴 ) ) · 𝑥 ) = ( 2 · ( ( 0 · 𝐴 ) · 𝑥 ) ) )
37 25 31 36 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 0 · 𝐴 ) · 𝑥 ) = ( 2 · ( ( 0 · 𝐴 ) · 𝑥 ) ) )
38 7 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( 2 · ( ( 0 · 𝐴 ) · 𝑥 ) ) = ( 2 · 1 ) )
39 2re ⊢ 2 ∈ ℝ
40 ax-1rid ⊢ ( 2 ∈ ℝ → ( 2 · 1 ) = 2 )
41 39 40 mp1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( 2 · 1 ) = 2 )
42 37 38 41 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → ( ( 0 · 𝐴 ) · 𝑥 ) = 2 )
43 7 42 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑥 ) = 1 ) ) → 1 = 2 )
44 6 43 rexlimddv ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → 1 = 2 )
45 44 ex ⊢ ( 𝐴 ∈ ℝ → ( ( 0 · 𝐴 ) ≠ 0 → 1 = 2 ) )
46 45 necon1d ⊢ ( 𝐴 ∈ ℝ → ( 1 ≠ 2 → ( 0 · 𝐴 ) = 0 ) )
47 1 46 mpi ⊢ ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )