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 )