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 𝐶 ) ) )