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

 Description: Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.)
Assertion
Ref Expression
sadass ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶)))

Proof of Theorem sadass
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 sadcl 15590 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
2 sadcl 15590 . . . . 5 (((𝐴 sadd 𝐵) ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
31, 2stoic3 1820 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
43sseld 3820 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) → 𝑘 ∈ ℕ0))
5 simp1 1127 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → 𝐴 ⊆ ℕ0)
6 sadcl 15590 . . . . . 6 ((𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
763adant1 1121 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
8 sadcl 15590 . . . . 5 ((𝐴 ⊆ ℕ0 ∧ (𝐵 sadd 𝐶) ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
95, 7, 8syl2anc 579 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
109sseld 3820 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) → 𝑘 ∈ ℕ0))
11 simpl1 1199 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆ ℕ0)
12 simpl2 1201 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℕ0)
13 simpl3 1203 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐶 ⊆ ℕ0)
14 simpr 479 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
15 1nn0 11660 . . . . . . . . . 10 1 ∈ ℕ0
1615a1i 11 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
1714, 16nn0addcld 11706 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
1811, 12, 13, 17sadasslem 15598 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))))
1918eleq2d 2845 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ 𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1)))))
20 elin 4019 . . . . . 6 (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
21 elin 4019 . . . . . 6 (𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
2219, 20, 213bitr3g 305 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
23 nn0uz 12028 . . . . . . . . 9 0 = (ℤ‘0)
2414, 23syl6eleq 2869 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (ℤ‘0))
25 eluzfz2 12666 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ (0...𝑘))
2624, 25syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0...𝑘))
2714nn0zd 11832 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
28 fzval3 12856 . . . . . . . 8 (𝑘 ∈ ℤ → (0...𝑘) = (0..^(𝑘 + 1)))
2927, 28syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (0...𝑘) = (0..^(𝑘 + 1)))
3026, 29eleqtrd 2861 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0..^(𝑘 + 1)))
3130biantrud 527 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3230biantrud 527 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3322, 31, 323bitr4d 303 . . . 4 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))
3433ex 403 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ℕ0 → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)))))
354, 10, 34pm5.21ndd 371 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))
3635eqrdv 2776 1 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶)))