Metamath Proof Explorer

Theorem sadass

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

Ref Expression
Assertion sadass 
|- ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( ( A sadd B ) sadd C ) = ( A sadd ( B sadd C ) ) )

Proof

Step Hyp Ref Expression
1 sadcl 
 |-  ( ( A C_ NN0 /\ B C_ NN0 ) -> ( A sadd B ) C_ NN0 )
2 sadcl 
 |-  ( ( ( A sadd B ) C_ NN0 /\ C C_ NN0 ) -> ( ( A sadd B ) sadd C ) C_ NN0 )
3 1 2 stoic3 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( ( A sadd B ) sadd C ) C_ NN0 )
4 3 sseld 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( k e. ( ( A sadd B ) sadd C ) -> k e. NN0 ) )
5 simp1 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> A C_ NN0 )
6 sadcl 
 |-  ( ( B C_ NN0 /\ C C_ NN0 ) -> ( B sadd C ) C_ NN0 )
7 6 3adant1 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( B sadd C ) C_ NN0 )
8 sadcl 
 |-  ( ( A C_ NN0 /\ ( B sadd C ) C_ NN0 ) -> ( A sadd ( B sadd C ) ) C_ NN0 )
9 5 7 8 syl2anc 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( A sadd ( B sadd C ) ) C_ NN0 )
10 9 sseld 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( k e. ( A sadd ( B sadd C ) ) -> k e. NN0 ) )
11 simpl1 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> A C_ NN0 )
12 simpl2 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> B C_ NN0 )
13 simpl3 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> C C_ NN0 )
14 simpr 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> k e. NN0 )
15 1nn0 
 |-  1 e. NN0
16 15 a1i 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> 1 e. NN0 )
17 14 16 nn0addcld 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( k + 1 ) e. NN0 )
18 11 12 13 17 sadasslem 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ ( k + 1 ) ) ) = ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ ( k + 1 ) ) ) )
19 18 eleq2d 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( k e. ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> k e. ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ ( k + 1 ) ) ) ) )
20 elin 
 |-  ( k e. ( ( ( A sadd B ) sadd C ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( ( A sadd B ) sadd C ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) )
21 elin 
 |-  ( k e. ( ( A sadd ( B sadd C ) ) i^i ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( A sadd ( B sadd C ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) )
22 19 20 21 3bitr3g 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( ( k e. ( ( A sadd B ) sadd C ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) <-> ( k e. ( A sadd ( B sadd C ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) )
23 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
24 14 23 eleqtrdi 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) )
25 eluzfz2 
 |-  ( k e. ( ZZ>= ` 0 ) -> k e. ( 0 ... k ) )
26 24 25 syl 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> k e. ( 0 ... k ) )
27 14 nn0zd 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> k e. ZZ )
28 fzval3 
 |-  ( k e. ZZ -> ( 0 ... k ) = ( 0 ..^ ( k + 1 ) ) )
29 27 28 syl 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( 0 ... k ) = ( 0 ..^ ( k + 1 ) ) )
30 26 29 eleqtrd 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> k e. ( 0 ..^ ( k + 1 ) ) )
31 30 biantrud 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( k e. ( ( A sadd B ) sadd C ) <-> ( k e. ( ( A sadd B ) sadd C ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) )
32 30 biantrud 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( k e. ( A sadd ( B sadd C ) ) <-> ( k e. ( A sadd ( B sadd C ) ) /\ k e. ( 0 ..^ ( k + 1 ) ) ) ) )
33 22 31 32 3bitr4d 
 |-  ( ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) /\ k e. NN0 ) -> ( k e. ( ( A sadd B ) sadd C ) <-> k e. ( A sadd ( B sadd C ) ) ) )
34 33 ex 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( k e. NN0 -> ( k e. ( ( A sadd B ) sadd C ) <-> k e. ( A sadd ( B sadd C ) ) ) ) )
35 4 10 34 pm5.21ndd 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( k e. ( ( A sadd B ) sadd C ) <-> k e. ( A sadd ( B sadd C ) ) ) )
36 35 eqrdv 
 |-  ( ( A C_ NN0 /\ B C_ NN0 /\ C C_ NN0 ) -> ( ( A sadd B ) sadd C ) = ( A sadd ( B sadd C ) ) )