Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Structured version   Visualization version   GIF version

 Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
addcomd (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))

StepHypRef Expression
1 1cnd 10094 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
21, 1addcld 10097 . . . . . . 7 (𝜑 → (1 + 1) ∈ ℂ)
3 muld.1 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
4 addcomd.2 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
52, 3, 4adddid 10102 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)))
63, 4addcld 10097 . . . . . . 7 (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
7 1p1times 10245 . . . . . . 7 ((𝐴 + 𝐵) ∈ ℂ → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
86, 7syl 17 . . . . . 6 (𝜑 → ((1 + 1) · (𝐴 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
9 1p1times 10245 . . . . . . . 8 (𝐴 ∈ ℂ → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
103, 9syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐴) = (𝐴 + 𝐴))
11 1p1times 10245 . . . . . . . 8 (𝐵 ∈ ℂ → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
124, 11syl 17 . . . . . . 7 (𝜑 → ((1 + 1) · 𝐵) = (𝐵 + 𝐵))
1310, 12oveq12d 6708 . . . . . 6 (𝜑 → (((1 + 1) · 𝐴) + ((1 + 1) · 𝐵)) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
145, 8, 133eqtr3rd 2694 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + (𝐵 + 𝐵)) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
153, 3addcld 10097 . . . . . 6 (𝜑 → (𝐴 + 𝐴) ∈ ℂ)
1615, 4, 4addassd 10100 . . . . 5 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = ((𝐴 + 𝐴) + (𝐵 + 𝐵)))
176, 3, 4addassd 10100 . . . . 5 (𝜑 → (((𝐴 + 𝐵) + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + (𝐴 + 𝐵)))
1814, 16, 173eqtr4d 2695 . . . 4 (𝜑 → (((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵))
1915, 4addcld 10097 . . . . 5 (𝜑 → ((𝐴 + 𝐴) + 𝐵) ∈ ℂ)
206, 3addcld 10097 . . . . 5 (𝜑 → ((𝐴 + 𝐵) + 𝐴) ∈ ℂ)
21 addcan2 10259 . . . . 5 ((((𝐴 + 𝐴) + 𝐵) ∈ ℂ ∧ ((𝐴 + 𝐵) + 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2219, 20, 4, 21syl3anc 1366 . . . 4 (𝜑 → ((((𝐴 + 𝐴) + 𝐵) + 𝐵) = (((𝐴 + 𝐵) + 𝐴) + 𝐵) ↔ ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴)))
2318, 22mpbid 222 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = ((𝐴 + 𝐵) + 𝐴))
243, 3, 4addassd 10100 . . 3 (𝜑 → ((𝐴 + 𝐴) + 𝐵) = (𝐴 + (𝐴 + 𝐵)))
253, 4, 3addassd 10100 . . 3 (𝜑 → ((𝐴 + 𝐵) + 𝐴) = (𝐴 + (𝐵 + 𝐴)))
2623, 24, 253eqtr3d 2693 . 2 (𝜑 → (𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)))
274, 3addcld 10097 . . 3 (𝜑 → (𝐵 + 𝐴) ∈ ℂ)
28 addcan 10258 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 + 𝐵) ∈ ℂ ∧ (𝐵 + 𝐴) ∈ ℂ) → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
293, 6, 27, 28syl3anc 1366 . 2 (𝜑 → ((𝐴 + (𝐴 + 𝐵)) = (𝐴 + (𝐵 + 𝐴)) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴)))
3026, 29mpbid 222 1 (𝜑 → (𝐴 + 𝐵) = (𝐵 + 𝐴))