Proof of Theorem zaddcom
| Step | Hyp | Ref
| Expression |
| 1 | | reelznn0nn 42479 |
. 2
⊢ (𝐴 ∈ ℤ ↔ (𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ))) |
| 2 | | reelznn0nn 42479 |
. 2
⊢ (𝐵 ∈ ℤ ↔ (𝐵 ∈ ℕ0 ∨
(𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ))) |
| 3 | | nn0addcom 42480 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 4 | | zaddcomlem 42481 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ 𝐵 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 5 | | zaddcomlem 42481 |
. . . . 5
⊢ (((𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ) ∧ 𝐴 ∈ ℕ0) → (𝐵 + 𝐴) = (𝐴 + 𝐵)) |
| 6 | 5 | eqcomd 2743 |
. . . 4
⊢ (((𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ) ∧ 𝐴 ∈ ℕ0) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 7 | 6 | ancoms 458 |
. . 3
⊢ ((𝐴 ∈ ℕ0
∧ (𝐵 ∈ ℝ
∧ (0 −ℝ 𝐵) ∈ ℕ)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 8 | | renegid2 42443 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → ((0
−ℝ 𝐵) + 𝐵) = 0) |
| 9 | 8 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐵) + 𝐵) = 0) |
| 10 | | renegid2 42443 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → ((0
−ℝ 𝐴) + 𝐴) = 0) |
| 11 | 10 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + 𝐴) = 0) |
| 12 | 11 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = (0 + 𝐵)) |
| 13 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0
−ℝ 𝐴) ∈ ℕ) |
| 14 | 13 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0
−ℝ 𝐴) ∈ ℂ) |
| 15 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → 𝐴 ∈ ℝ) |
| 16 | 15 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → 𝐴 ∈ ℂ) |
| 17 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → 𝐵 ∈ ℝ) |
| 18 | 17 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → 𝐵 ∈ ℂ) |
| 19 | 14, 16, 18 | addassd 11283 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐴) + 𝐴) + 𝐵) = ((0 −ℝ 𝐴) + (𝐴 + 𝐵))) |
| 20 | | readdlid 42433 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (0 +
𝐵) = 𝐵) |
| 21 | 20 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0 + 𝐵) = 𝐵) |
| 22 | 12, 19, 21 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + (𝐴 + 𝐵)) = 𝐵) |
| 23 | 22 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐵) + ((0 −ℝ 𝐴) + (𝐴 + 𝐵))) = ((0 −ℝ 𝐵) + 𝐵)) |
| 24 | 9, 23, 11 | 3eqtr4d 2787 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐵) + ((0 −ℝ 𝐴) + (𝐴 + 𝐵))) = ((0 −ℝ 𝐴) + 𝐴)) |
| 25 | | simprr 773 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0
−ℝ 𝐵) ∈ ℕ) |
| 26 | 25 | nncnd 12282 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0
−ℝ 𝐵) ∈ ℂ) |
| 27 | 16, 18 | addcld 11280 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (𝐴 + 𝐵) ∈ ℂ) |
| 28 | 26, 14, 27 | addassd 11283 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐵) + (0 −ℝ 𝐴)) + (𝐴 + 𝐵)) = ((0 −ℝ 𝐵) + ((0
−ℝ 𝐴) + (𝐴 + 𝐵)))) |
| 29 | 9 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐵) + 𝐵) + 𝐴) = (0 + 𝐴)) |
| 30 | 26, 18, 16 | addassd 11283 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐵) + 𝐵) + 𝐴) = ((0 −ℝ 𝐵) + (𝐵 + 𝐴))) |
| 31 | | readdlid 42433 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 +
𝐴) = 𝐴) |
| 32 | 31 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (0 + 𝐴) = 𝐴) |
| 33 | 29, 30, 32 | 3eqtr3d 2785 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐵) + (𝐵 + 𝐴)) = 𝐴) |
| 34 | 33 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + ((0 −ℝ 𝐵) + (𝐵 + 𝐴))) = ((0 −ℝ 𝐴) + 𝐴)) |
| 35 | 24, 28, 34 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐵) + (0 −ℝ 𝐴)) + (𝐴 + 𝐵)) = ((0 −ℝ 𝐴) + ((0
−ℝ 𝐵) + (𝐵 + 𝐴)))) |
| 36 | | nnaddcom 42303 |
. . . . . . 7
⊢ (((0
−ℝ 𝐴) ∈ ℕ ∧ (0
−ℝ 𝐵) ∈ ℕ) → ((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) = ((0
−ℝ 𝐵) + (0 −ℝ 𝐴))) |
| 37 | 36 | ad2ant2l 746 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) = ((0
−ℝ 𝐵) + (0 −ℝ 𝐴))) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) + (𝐴 + 𝐵)) = (((0 −ℝ 𝐵) + (0 −ℝ
𝐴)) + (𝐴 + 𝐵))) |
| 39 | 18, 16 | addcld 11280 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (𝐵 + 𝐴) ∈ ℂ) |
| 40 | 14, 26, 39 | addassd 11283 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) + (𝐵 + 𝐴)) = ((0 −ℝ 𝐴) + ((0
−ℝ 𝐵) + (𝐵 + 𝐴)))) |
| 41 | 35, 38, 40 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) + (𝐴 + 𝐵)) = (((0 −ℝ 𝐴) + (0 −ℝ
𝐵)) + (𝐵 + 𝐴))) |
| 42 | 13, 25 | nnaddcld 12318 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) ∈
ℕ) |
| 43 | 42 | nncnd 12282 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) ∈
ℂ) |
| 44 | 43, 27, 39 | sn-addcand 42449 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → ((((0
−ℝ 𝐴) + (0 −ℝ 𝐵)) + (𝐴 + 𝐵)) = (((0 −ℝ 𝐴) + (0 −ℝ
𝐵)) + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
| 45 | 41, 44 | mpbid 232 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ) ∧ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 46 | 3, 4, 7, 45 | ccase 1038 |
. 2
⊢ (((𝐴 ∈ ℕ0 ∨
(𝐴 ∈ ℝ ∧ (0
−ℝ 𝐴) ∈ ℕ)) ∧ (𝐵 ∈ ℕ0 ∨ (𝐵 ∈ ℝ ∧ (0
−ℝ 𝐵) ∈ ℕ))) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
| 47 | 1, 2, 46 | syl2anb 598 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |