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

Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 sadcl 15392 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
2 sadcl 15392 . . . . 5 (((𝐴 sadd 𝐵) ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
31, 2stoic3 1849 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
43sseld 3751 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) → 𝑘 ∈ ℕ0))
5 simp1 1130 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → 𝐴 ⊆ ℕ0)
6 sadcl 15392 . . . . . 6 ((𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
763adant1 1124 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
8 sadcl 15392 . . . . 5 ((𝐴 ⊆ ℕ0 ∧ (𝐵 sadd 𝐶) ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
95, 7, 8syl2anc 573 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
109sseld 3751 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) → 𝑘 ∈ ℕ0))
11 simpl1 1227 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆ ℕ0)
12 simpl2 1229 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℕ0)
13 simpl3 1231 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐶 ⊆ ℕ0)
14 simpr 471 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
15 1nn0 11515 . . . . . . . . . 10 1 ∈ ℕ0
1615a1i 11 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
1714, 16nn0addcld 11562 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
1811, 12, 13, 17sadasslem 15400 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))))
1918eleq2d 2836 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ 𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1)))))
20 elin 3947 . . . . . 6 (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
21 elin 3947 . . . . . 6 (𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
2219, 20, 213bitr3g 302 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
23 nn0uz 11929 . . . . . . . . 9 0 = (ℤ‘0)
2414, 23syl6eleq 2860 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (ℤ‘0))
25 eluzfz2 12556 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ (0...𝑘))
2624, 25syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0...𝑘))
2714nn0zd 11687 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
28 fzval3 12745 . . . . . . . 8 (𝑘 ∈ ℤ → (0...𝑘) = (0..^(𝑘 + 1)))
2927, 28syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (0...𝑘) = (0..^(𝑘 + 1)))
3026, 29eleqtrd 2852 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0..^(𝑘 + 1)))
3130biantrud 521 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3230biantrud 521 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3322, 31, 323bitr4d 300 . . . 4 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))
3433ex 397 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ℕ0 → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)))))
354, 10, 34pm5.21ndd 368 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))