Metamath Proof Explorer

Theorem zmulcomlem

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

Ref Expression
Assertion zmulcomlem ⊢ A ∈ ℝ ∧ 0 - ℝ A ∈ ℕ ∧ B ∈ ℕ 0 → A ⁢ B = B ⁢ A

Proof

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