Metamath Proof Explorer

Theorem remul01

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

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

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( ( 𝐴 · 0 ) = 1 → ( 2 · ( 𝐴 · 0 ) ) = ( 2 · 1 ) )
2 1 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · ( 𝐴 · 0 ) ) = ( 2 · 1 ) )
3 2re ⊢ 2 ∈ ℝ
4 ax-1rid ⊢ ( 2 ∈ ℝ → ( 2 · 1 ) = 2 )
5 3 4 mp1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · 1 ) = 2 )
6 2 5 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · ( 𝐴 · 0 ) ) = 2 )
7 3 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → 2 ∈ ℝ )
8 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → 𝐴 ∈ ℝ )
9 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → 0 ∈ ℝ )
10 8 9 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 𝐴 · 0 ) ∈ ℝ )
11 7 10 remulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · ( 𝐴 · 0 ) ) ∈ ℝ )
12 sn-0ne2 ⊢ 0 ≠ 2
13 12 necomi ⊢ 2 ≠ 0
14 13 a1i ⊢ ( ( 2 · ( 𝐴 · 0 ) ) = 2 → 2 ≠ 0 )
15 eqtr2 ⊢ ( ( ( 2 · ( 𝐴 · 0 ) ) = 2 ∧ ( 2 · ( 𝐴 · 0 ) ) = 0 ) → 2 = 0 )
16 14 15 mteqand ⊢ ( ( 2 · ( 𝐴 · 0 ) ) = 2 → ( 2 · ( 𝐴 · 0 ) ) ≠ 0 )
17 ax-rrecex ⊢ ( ( ( 2 · ( 𝐴 · 0 ) ) ∈ ℝ ∧ ( 2 · ( 𝐴 · 0 ) ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 )
18 11 16 17 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) → ∃ 𝑥 ∈ ℝ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 )
19 2cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 2 ∈ ℂ )
20 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
21 0red ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 0 ∈ ℝ )
22 20 21 remulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 𝐴 · 0 ) ∈ ℝ )
23 22 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 𝐴 · 0 ) ∈ ℂ )
24 simprl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
25 24 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
26 19 23 25 mulassd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = ( 2 · ( ( 𝐴 · 0 ) · 𝑥 ) ) )
27 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 )
28 20 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
29 0cnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → 0 ∈ ℂ )
30 28 29 25 mulassd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 0 ) · 𝑥 ) = ( 𝐴 · ( 0 · 𝑥 ) ) )
31 remul02 ⊢ ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
32 31 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 0 · 𝑥 ) = 0 )
33 32 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 0 · 𝑥 ) ) = ( 𝐴 · 0 ) )
34 30 33 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 0 ) · 𝑥 ) = ( 𝐴 · 0 ) )
35 34 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 2 · ( ( 𝐴 · 0 ) · 𝑥 ) ) = ( 2 · ( 𝐴 · 0 ) ) )
36 26 27 35 3eqtr3rd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 2 · ( 𝐴 · 0 ) ) · 𝑥 ) = 1 ) ) → ( 2 · ( 𝐴 · 0 ) ) = 1 )
37 18 36 rexlimddv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) ∧ ( 2 · ( 𝐴 · 0 ) ) = 2 ) → ( 2 · ( 𝐴 · 0 ) ) = 1 )
38 6 37 mpdan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · ( 𝐴 · 0 ) ) = 1 )
39 sn-1ne2 ⊢ 1 ≠ 2
40 39 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → 1 ≠ 2 )
41 38 40 eqnetrd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ( 2 · ( 𝐴 · 0 ) ) ≠ 2 )
42 6 41 pm2.21ddne ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) = 1 ) → ¬ ( 𝐴 · 0 ) = 1 )
43 42 ex ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 · 0 ) = 1 → ¬ ( 𝐴 · 0 ) = 1 ) )
44 pm2.01 ⊢ ( ( ( 𝐴 · 0 ) = 1 → ¬ ( 𝐴 · 0 ) = 1 ) → ¬ ( 𝐴 · 0 ) = 1 )
45 44 neqned ⊢ ( ( ( 𝐴 · 0 ) = 1 → ¬ ( 𝐴 · 0 ) = 1 ) → ( 𝐴 · 0 ) ≠ 1 )
46 43 45 syl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) ≠ 1 )
47 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
48 elre0re ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
49 47 48 remulcld ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) ∈ ℝ )
50 ax-rrecex ⊢ ( ( ( 𝐴 · 0 ) ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 )
51 49 50 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 )
52 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
53 52 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
54 0cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → 0 ∈ ℂ )
55 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
56 55 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
57 53 54 56 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 0 ) · 𝑥 ) = ( 𝐴 · ( 0 · 𝑥 ) ) )
58 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 0 ) · 𝑥 ) = 1 )
59 31 oveq2d ⊢ ( 𝑥 ∈ ℝ → ( 𝐴 · ( 0 · 𝑥 ) ) = ( 𝐴 · 0 ) )
60 59 ad2antrl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 0 · 𝑥 ) ) = ( 𝐴 · 0 ) )
61 57 58 60 3eqtr3rd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( ( 𝐴 · 0 ) · 𝑥 ) = 1 ) ) → ( 𝐴 · 0 ) = 1 )
62 51 61 rexlimddv ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 · 0 ) ≠ 0 ) → ( 𝐴 · 0 ) = 1 )
63 62 ex ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 · 0 ) ≠ 0 → ( 𝐴 · 0 ) = 1 ) )
64 63 necon1d ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 · 0 ) ≠ 1 → ( 𝐴 · 0 ) = 0 ) )
65 46 64 mpd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )