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 ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )