Step | Hyp | Ref
| Expression |
1 | | repswlen 12874 |
. . . . . 6
 
     repeatS     |
2 | 1 | 3adant3 1027 |
. . . . 5
 
     repeatS     |
3 | | repswlen 12874 |
. . . . . 6
 
     repeatS     |
4 | 3 | 3adant2 1026 |
. . . . 5
 
     repeatS     |
5 | 2, 4 | oveq12d 6306 |
. . . 4
 
      repeatS       repeatS        |
6 | 5 | oveq2d 6304 |
. . 3
 
  ..^     repeatS
      repeatS
     ..^     |
7 | | simp1 1007 |
. . . . . . . 8
 
   |
8 | 7 | adantr 467 |
. . . . . . 7
  

 ..^    repeatS    
  |
9 | | simpl2 1011 |
. . . . . . 7
  

 ..^    repeatS    
  |
10 | 2 | oveq2d 6304 |
. . . . . . . . 9
 
  ..^    repeatS     ..^   |
11 | 10 | eleq2d 2513 |
. . . . . . . 8
 
   ..^    repeatS     ..^    |
12 | 11 | biimpa 487 |
. . . . . . 7
  

 ..^    repeatS    
 ..^   |
13 | 8, 9, 12 | 3jca 1187 |
. . . . . 6
  

 ..^    repeatS    

 ..^    |
14 | 13 | adantlr 720 |
. . . . 5
   
  ..^     repeatS       repeatS       ..^    repeatS
    
 ..^    |
15 | | repswsymb 12872 |
. . . . 5
 
 ..^ 
  repeatS       |
16 | 14, 15 | syl 17 |
. . . 4
   
  ..^     repeatS       repeatS       ..^    repeatS
      repeatS       |
17 | 7 | ad2antrr 731 |
. . . . 5
   
  ..^     repeatS       repeatS       ..^    repeatS
   
  |
18 | | simpll3 1048 |
. . . . 5
   
  ..^     repeatS       repeatS       ..^    repeatS
   
  |
19 | 2, 4 | jca 535 |
. . . . . . 7
 
      repeatS       repeatS
     |
20 | | simpr 463 |
. . . . . . . . . . . 12
   
 ..^     ..^     |
21 | 20 | anim1i 571 |
. . . . . . . . . . 11
   
  ..^     ..^ 
  ..^    ..^    |
22 | | nn0z 10957 |
. . . . . . . . . . . . 13

  |
23 | | nn0z 10957 |
. . . . . . . . . . . . 13

  |
24 | 22, 23 | anim12i 569 |
. . . . . . . . . . . 12
 
     |
25 | 24 | ad2antrr 731 |
. . . . . . . . . . 11
   
  ..^     ..^ 
    |
26 | | fzocatel 11975 |
. . . . . . . . . . 11
    ..^  
 ..^        ..^   |
27 | 21, 25, 26 | syl2anc 666 |
. . . . . . . . . 10
   
  ..^     ..^ 
   ..^   |
28 | 27 | exp31 608 |
. . . . . . . . 9
 
   ..^     ..^    ..^     |
29 | 28 | 3adant1 1025 |
. . . . . . . 8
 
   ..^   
 ..^    ..^     |
30 | | oveq12 6297 |
. . . . . . . . . . 11
      repeatS       repeatS
        repeatS
      repeatS
       |
31 | 30 | oveq2d 6304 |
. . . . . . . . . 10
      repeatS       repeatS
    ..^     repeatS       repeatS      ..^     |
32 | 31 | eleq2d 2513 |
. . . . . . . . 9
      repeatS       repeatS
     ..^     repeatS       repeatS      ..^      |
33 | | oveq2 6296 |
. . . . . . . . . . . . 13
     repeatS    ..^    repeatS     ..^   |
34 | 33 | eleq2d 2513 |
. . . . . . . . . . . 12
     repeatS     ..^    repeatS
  
 ..^    |
35 | 34 | notbid 296 |
. . . . . . . . . . 11
     repeatS     ..^    repeatS
  
 ..^    |
36 | 35 | adantr 467 |
. . . . . . . . . 10
      repeatS       repeatS
     ..^    repeatS
  
 ..^    |
37 | | oveq2 6296 |
. . . . . . . . . . . 12
     repeatS        repeatS        |
38 | 37 | eleq1d 2512 |
. . . . . . . . . . 11
     repeatS         repeatS     ..^    ..^    |
39 | 38 | adantr 467 |
. . . . . . . . . 10
      repeatS       repeatS
         repeatS     ..^    ..^    |
40 | 36, 39 | imbi12d 322 |
. . . . . . . . 9
      repeatS       repeatS
      ..^    repeatS         repeatS     ..^ 

 ..^    ..^     |
41 | 32, 40 | imbi12d 322 |
. . . . . . . 8
      repeatS       repeatS
      ..^     repeatS       repeatS    

 ..^    repeatS         repeatS     ..^  
  ..^     ..^    ..^      |
42 | 29, 41 | syl5ibr 225 |
. . . . . . 7
      repeatS       repeatS
        ..^     repeatS       repeatS    

 ..^    repeatS         repeatS     ..^      |
43 | 19, 42 | mpcom 37 |
. . . . . 6
 
   ..^     repeatS       repeatS    

 ..^    repeatS         repeatS     ..^     |
44 | 43 | imp31 434 |
. . . . 5
   
  ..^     repeatS       repeatS       ..^    repeatS
         repeatS     ..^   |
45 | | repswsymb 12872 |
. . . . 5
 
     repeatS
    ..^    repeatS         repeatS
      |
46 | 17, 18, 44, 45 | syl3anc 1267 |
. . . 4
   
  ..^     repeatS       repeatS       ..^    repeatS
      repeatS         repeatS       |
47 | 16, 46 | ifeqda 3913 |
. . 3
  

 ..^     repeatS
      repeatS
        ..^    repeatS       repeatS        repeatS         repeatS
       |
48 | 6, 47 | mpteq12dva 4479 |
. 2
 
   ..^     repeatS       repeatS        ..^    repeatS       repeatS        repeatS         repeatS
        ..^      |
49 | | ovex 6316 |
. . . 4
 repeatS   |
50 | | ovex 6316 |
. . . 4
 repeatS   |
51 | 49, 50 | pm3.2i 457 |
. . 3
  repeatS   repeatS
   |
52 | | ccatfval 12716 |
. . 3
   repeatS
  repeatS     repeatS  ++
 repeatS     ..^     repeatS       repeatS        ..^    repeatS       repeatS        repeatS         repeatS
        |
53 | 51, 52 | mp1i 13 |
. 2
 
   repeatS
 ++ 
repeatS     ..^     repeatS       repeatS        ..^    repeatS
      repeatS
       repeatS
        repeatS         |
54 | | nn0addcl 10902 |
. . . 4
 
     |
55 | 54 | 3adant1 1025 |
. . 3
 
 
   |
56 | | reps 12868 |
. . 3
  
   repeatS
     ..^      |
57 | 7, 55, 56 | syl2anc 666 |
. 2
 
  repeatS      ..^      |
58 | 48, 53, 57 | 3eqtr4d 2494 |
1
 
   repeatS
 ++ 
repeatS    repeatS 
    |