Proof of Theorem zaddcomlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → 𝐵 ∈
ℕ0) | 
| 2 | 1 | nn0cnd 12589 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 3 |  | rernegcl 42401 | . . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0
−ℝ 𝐴) ∈ ℝ) | 
| 4 | 3 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (0
−ℝ 𝐴) ∈ ℝ) | 
| 5 | 4 | recnd 11289 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (0
−ℝ 𝐴) ∈ ℂ) | 
| 6 |  | simpll 767 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → 𝐴 ∈
ℝ) | 
| 7 | 6 | recnd 11289 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 8 | 2, 5, 7 | addassd 11283 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → ((𝐵 + (0 −ℝ
𝐴)) + 𝐴) = (𝐵 + ((0 −ℝ 𝐴) + 𝐴))) | 
| 9 |  | renegid2 42443 | . . . . . . 7
⊢ (𝐴 ∈ ℝ → ((0
−ℝ 𝐴) + 𝐴) = 0) | 
| 10 | 9 | ad2antrr 726 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → ((0
−ℝ 𝐴) + 𝐴) = 0) | 
| 11 | 10 | oveq2d 7447 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐵 + ((0 −ℝ
𝐴) + 𝐴)) = (𝐵 + 0)) | 
| 12 |  | nn0re 12535 | . . . . . . 7
⊢ (𝐵 ∈ ℕ0
→ 𝐵 ∈
ℝ) | 
| 13 |  | readdrid 42439 | . . . . . . 7
⊢ (𝐵 ∈ ℝ → (𝐵 + 0) = 𝐵) | 
| 14 | 12, 13 | syl 17 | . . . . . 6
⊢ (𝐵 ∈ ℕ0
→ (𝐵 + 0) = 𝐵) | 
| 15 | 14 | adantl 481 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐵 + 0) = 𝐵) | 
| 16 | 8, 11, 15 | 3eqtrrd 2782 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → 𝐵 = ((𝐵 + (0 −ℝ 𝐴)) + 𝐴)) | 
| 17 | 9 | oveq1d 7446 | . . . . . 6
⊢ (𝐴 ∈ ℝ → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = (0 + 𝐵)) | 
| 18 | 17 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = (0 + 𝐵)) | 
| 19 |  | readdlid 42433 | . . . . . 6
⊢ (𝐵 ∈ ℝ → (0 +
𝐵) = 𝐵) | 
| 20 | 12, 19 | syl 17 | . . . . 5
⊢ (𝐵 ∈ ℕ0
→ (0 + 𝐵) = 𝐵) | 
| 21 | 18, 20 | sylan9eq 2797 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = 𝐵) | 
| 22 |  | nnnn0 12533 | . . . . . . 7
⊢ ((0
−ℝ 𝐴) ∈ ℕ → (0
−ℝ 𝐴) ∈
ℕ0) | 
| 23 |  | nn0addcom 42480 | . . . . . . 7
⊢ (((0
−ℝ 𝐴) ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)
→ ((0 −ℝ 𝐴) + 𝐵) = (𝐵 + (0 −ℝ 𝐴))) | 
| 24 | 22, 23 | sylan 580 | . . . . . 6
⊢ (((0
−ℝ 𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ0) → ((0
−ℝ 𝐴) + 𝐵) = (𝐵 + (0 −ℝ 𝐴))) | 
| 25 | 24 | adantll 714 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → ((0
−ℝ 𝐴) + 𝐵) = (𝐵 + (0 −ℝ 𝐴))) | 
| 26 | 25 | oveq1d 7446 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + 𝐵) + 𝐴) = ((𝐵 + (0 −ℝ 𝐴)) + 𝐴)) | 
| 27 | 16, 21, 26 | 3eqtr4d 2787 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = (((0 −ℝ 𝐴) + 𝐵) + 𝐴)) | 
| 28 | 5, 7, 2 | addassd 11283 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = ((0 −ℝ 𝐴) + (𝐴 + 𝐵))) | 
| 29 | 5, 2, 7 | addassd 11283 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + 𝐵) + 𝐴) = ((0 −ℝ 𝐴) + (𝐵 + 𝐴))) | 
| 30 | 27, 28, 29 | 3eqtr3d 2785 | . 2
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → ((0
−ℝ 𝐴) + (𝐴 + 𝐵)) = ((0 −ℝ 𝐴) + (𝐵 + 𝐴))) | 
| 31 | 7, 2 | addcld 11280 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℂ) | 
| 32 | 2, 7 | addcld 11280 | . . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐵 + 𝐴) ∈ ℂ) | 
| 33 | 5, 31, 32 | sn-addcand 42449 | . 2
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (((0
−ℝ 𝐴) + (𝐴 + 𝐵)) = ((0 −ℝ 𝐴) + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) | 
| 34 | 30, 33 | mpbid 232 | 1
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |