Metamath Proof Explorer


Theorem sadass

Description: Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Assertion sadass ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) = ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 sadcl ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0 ) → ( 𝐴 sadd 𝐵 ) ⊆ ℕ0 )
2 sadcl ( ( ( 𝐴 sadd 𝐵 ) ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ⊆ ℕ0 )
3 1 2 stoic3 ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ⊆ ℕ0 )
4 3 sseld ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) → 𝑘 ∈ ℕ0 ) )
5 simp1 ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → 𝐴 ⊆ ℕ0 )
6 sadcl ( ( 𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 )
7 6 3adant1 ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 )
8 sadcl ( ( 𝐴 ⊆ ℕ0 ∧ ( 𝐵 sadd 𝐶 ) ⊆ ℕ0 ) → ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ⊆ ℕ0 )
9 5 7 8 syl2anc ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ⊆ ℕ0 )
10 9 sseld ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) → 𝑘 ∈ ℕ0 ) )
11 simpl1 ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ⊆ ℕ0 )
12 simpl2 ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ⊆ ℕ0 )
13 simpl3 ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ⊆ ℕ0 )
14 simpr ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
15 1nn0 1 ∈ ℕ0
16 15 a1i ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℕ0 )
17 14 16 nn0addcld ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 + 1 ) ∈ ℕ0 )
18 11 12 13 17 sadasslem ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) = ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) )
19 18 eleq2d ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ↔ 𝑘 ∈ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) )
20 elin ( 𝑘 ∈ ( ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ↔ ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) )
21 elin ( 𝑘 ∈ ( ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∩ ( 0 ..^ ( 𝑘 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) )
22 19 20 21 3bitr3g ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) )
23 nn0uz 0 = ( ℤ ‘ 0 )
24 14 23 eleqtrdi ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ( ℤ ‘ 0 ) )
25 eluzfz2 ( 𝑘 ∈ ( ℤ ‘ 0 ) → 𝑘 ∈ ( 0 ... 𝑘 ) )
26 24 25 syl ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ( 0 ... 𝑘 ) )
27 14 nn0zd ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
28 fzval3 ( 𝑘 ∈ ℤ → ( 0 ... 𝑘 ) = ( 0 ..^ ( 𝑘 + 1 ) ) )
29 27 28 syl ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) = ( 0 ..^ ( 𝑘 + 1 ) ) )
30 26 29 eleqtrd ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) )
31 30 biantrud ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ↔ ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) )
32 30 biantrud ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ↔ ( 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ∧ 𝑘 ∈ ( 0 ..^ ( 𝑘 + 1 ) ) ) ) )
33 22 31 32 3bitr4d ( ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ↔ 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ) )
34 33 ex ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝑘 ∈ ℕ0 → ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ↔ 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ) ) )
35 4 10 34 pm5.21ndd ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( 𝑘 ∈ ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) ↔ 𝑘 ∈ ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) ) )
36 35 eqrdv ( ( 𝐴 ⊆ ℕ0𝐵 ⊆ ℕ0𝐶 ⊆ ℕ0 ) → ( ( 𝐴 sadd 𝐵 ) sadd 𝐶 ) = ( 𝐴 sadd ( 𝐵 sadd 𝐶 ) ) )