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 15809 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
2 sadcl 15809 . . . . 5 (((𝐴 sadd 𝐵) ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
31, 2stoic3 1778 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) ⊆ ℕ0)
43sseld 3952 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) → 𝑘 ∈ ℕ0))
5 simp1 1133 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → 𝐴 ⊆ ℕ0)
6 sadcl 15809 . . . . . 6 ((𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
763adant1 1127 . . . . 5 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐵 sadd 𝐶) ⊆ ℕ0)
8 sadcl 15809 . . . . 5 ((𝐴 ⊆ ℕ0 ∧ (𝐵 sadd 𝐶) ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
95, 7, 8syl2anc 587 . . . 4 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝐴 sadd (𝐵 sadd 𝐶)) ⊆ ℕ0)
109sseld 3952 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) → 𝑘 ∈ ℕ0))
11 simpl1 1188 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐴 ⊆ ℕ0)
12 simpl2 1189 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆ ℕ0)
13 simpl3 1190 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝐶 ⊆ ℕ0)
14 simpr 488 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
15 1nn0 11910 . . . . . . . . . 10 1 ∈ ℕ0
1615a1i 11 . . . . . . . . 9 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 1 ∈ ℕ0)
1714, 16nn0addcld 11956 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ0)
1811, 12, 13, 17sadasslem 15817 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))))
1918eleq2d 2901 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ 𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1)))))
20 elin 3935 . . . . . 6 (𝑘 ∈ (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
21 elin 3935 . . . . . 6 (𝑘 ∈ ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1))))
2219, 20, 213bitr3g 316 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → ((𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1))) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
23 nn0uz 12277 . . . . . . . . 9 0 = (ℤ‘0)
2414, 23eleqtrdi 2926 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (ℤ‘0))
25 eluzfz2 12919 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ (0...𝑘))
2624, 25syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0...𝑘))
2714nn0zd 12082 . . . . . . . 8 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
28 fzval3 13110 . . . . . . . 8 (𝑘 ∈ ℤ → (0...𝑘) = (0..^(𝑘 + 1)))
2927, 28syl 17 . . . . . . 7 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (0...𝑘) = (0..^(𝑘 + 1)))
3026, 29eleqtrd 2918 . . . . . 6 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ (0..^(𝑘 + 1)))
3130biantrud 535 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3230biantrud 535 . . . . 5 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ↔ (𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)) ∧ 𝑘 ∈ (0..^(𝑘 + 1)))))
3322, 31, 323bitr4d 314 . . . 4 (((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) ∧ 𝑘 ∈ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))
3433ex 416 . . 3 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ℕ0 → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶)))))
354, 10, 34pm5.21ndd 384 . 2 ((𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0) → (𝑘 ∈ ((𝐴 sadd 𝐵) sadd 𝐶) ↔ 𝑘 ∈ (𝐴 sadd (𝐵 sadd 𝐶))))