Metamath Proof Explorer


Theorem zmulcomlem

Description: Lemma for zmulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion zmulcomlem ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
2 renegneg ( 𝐴 ∈ ℝ → ( 0 − ( 0 − 𝐴 ) ) = 𝐴 )
3 2 oveq1d ( 𝐴 ∈ ℝ → ( ( 0 − ( 0 − 𝐴 ) ) · 𝐵 ) = ( 𝐴 · 𝐵 ) )
4 3 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( ( 0 − ( 0 − 𝐴 ) ) · 𝐵 ) = ( 𝐴 · 𝐵 ) )
5 rernegcl ( 𝐴 ∈ ℝ → ( 0 − 𝐴 ) ∈ ℝ )
6 5 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 0 − 𝐴 ) ∈ ℝ )
7 simpr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℕ )
8 6 7 renegmulnnass ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( ( 0 − ( 0 − 𝐴 ) ) · 𝐵 ) = ( 0 − ( ( 0 − 𝐴 ) · 𝐵 ) ) )
9 nnmulcom ( ( ( 0 − 𝐴 ) ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 0 − 𝐴 ) · 𝐵 ) = ( 𝐵 · ( 0 − 𝐴 ) ) )
10 9 adantll ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( ( 0 − 𝐴 ) · 𝐵 ) = ( 𝐵 · ( 0 − 𝐴 ) ) )
11 10 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 0 − ( ( 0 − 𝐴 ) · 𝐵 ) ) = ( 0 − ( 𝐵 · ( 0 − 𝐴 ) ) ) )
12 nnre ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
13 12 adantl ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → 𝐵 ∈ ℝ )
14 0red ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → 0 ∈ ℝ )
15 resubdi ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( 0 − ( 0 − 𝐴 ) ) ) = ( ( 𝐵 · 0 ) − ( 𝐵 · ( 0 − 𝐴 ) ) ) )
16 13 14 6 15 syl3anc ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · ( 0 − ( 0 − 𝐴 ) ) ) = ( ( 𝐵 · 0 ) − ( 𝐵 · ( 0 − 𝐴 ) ) ) )
17 remul01 ( 𝐵 ∈ ℝ → ( 𝐵 · 0 ) = 0 )
18 12 17 syl ( 𝐵 ∈ ℕ → ( 𝐵 · 0 ) = 0 )
19 18 adantl ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · 0 ) = 0 )
20 19 oveq1d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( ( 𝐵 · 0 ) − ( 𝐵 · ( 0 − 𝐴 ) ) ) = ( 0 − ( 𝐵 · ( 0 − 𝐴 ) ) ) )
21 16 20 eqtrd ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · ( 0 − ( 0 − 𝐴 ) ) ) = ( 0 − ( 𝐵 · ( 0 − 𝐴 ) ) ) )
22 2 ad2antrr ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 0 − ( 0 − 𝐴 ) ) = 𝐴 )
23 22 oveq2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐵 · ( 0 − ( 0 − 𝐴 ) ) ) = ( 𝐵 · 𝐴 ) )
24 11 21 23 3eqtr2d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 0 − ( ( 0 − 𝐴 ) · 𝐵 ) ) = ( 𝐵 · 𝐴 ) )
25 8 4 24 3eqtr3d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
26 4 4 25 3eqtr3d ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
27 remul01 ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
28 remul02 ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )
29 27 28 eqtr4d ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) )
30 29 adantr ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) → ( 𝐴 · 0 ) = ( 0 · 𝐴 ) )
31 oveq2 ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
32 oveq1 ( 𝐵 = 0 → ( 𝐵 · 𝐴 ) = ( 0 · 𝐴 ) )
33 31 32 eqeq12d ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ↔ ( 𝐴 · 0 ) = ( 0 · 𝐴 ) ) )
34 30 33 syl5ibrcom ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) → ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) )
35 34 imp ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 = 0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
36 26 35 jaodan ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
37 1 36 sylan2b ( ( ( 𝐴 ∈ ℝ ∧ ( 0 − 𝐴 ) ∈ ℕ ) ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )