Step | Hyp | Ref
| Expression |
1 | | simp21 1063 |
. . 3
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
  ![[,] [,]](_icc.gif)    |
2 | | simp22 1064 |
. . 3
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
  ![[,] [,]](_icc.gif)    |
3 | | fveere 25010 |
. . . . . . . . . . . . 13
     
           |
4 | 3 | expcom 442 |
. . . . . . . . . . . 12
     
           |
5 | | fveere 25010 |
. . . . . . . . . . . . 13
     
           |
6 | 5 | expcom 442 |
. . . . . . . . . . . 12
     
           |
7 | 4, 6 | anim12d 572 |
. . . . . . . . . . 11
               
             |
8 | | fveere 25010 |
. . . . . . . . . . . . 13
     
           |
9 | 8 | expcom 442 |
. . . . . . . . . . . 12
     
           |
10 | | fveere 25010 |
. . . . . . . . . . . . 13
     
           |
11 | 10 | expcom 442 |
. . . . . . . . . . . 12
     
           |
12 | 9, 11 | anim12d 572 |
. . . . . . . . . . 11
               
             |
13 | 7, 12 | anim12d 572 |
. . . . . . . . . 10
           
                                         |
14 | 13 | impcom 437 |
. . . . . . . . 9
       
               
                             |
15 | | unitssre 11805 |
. . . . . . . . . . . . . . . 16
  ![[,] [,]](_icc.gif)   |
16 | 15 | sseli 3414 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
17 | 16 | 3ad2ant1 1051 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)  
  |
18 | 17 | adantl 473 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
 
  |
19 | | peano2rem 9961 |
. . . . . . . . . . . . 13
 
   |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
      |
21 | | simplll 776 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
22 | 20, 21 | remulcld 9689 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
            |
23 | | simpllr 777 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
24 | 22, 23 | readdcld 9688 |
. . . . . . . . . 10
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                  |
25 | | simpr3 1038 |
. . . . . . . . . 10
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
    |
26 | 24, 18, 25 | redivcld 10457 |
. . . . . . . . 9
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
27 | 14, 26 | sylan 479 |
. . . . . . . 8
              
         
        ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
28 | 27 | an32s 821 |
. . . . . . 7
              
          
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                           |
29 | 28 | ralrimiva 2809 |
. . . . . 6
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                            |
30 | | eleenn 25005 |
. . . . . . . 8
       |
31 | 30 | ad3antrrr 744 |
. . . . . . 7
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)      |
32 | | mptelee 25004 |
. . . . . . 7
                            
                        |
33 | 31, 32 | syl 17 |
. . . . . 6
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                               
                        |
34 | 29, 33 | mpbird 240 |
. . . . 5
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                |
35 | 34 | 3adant3 1050 |
. . . 4
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
                            |
36 | | simplrl 778 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
37 | 22, 36 | readdcld 9688 |
. . . . . . . . . 10
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                  |
38 | 37, 18, 25 | redivcld 10457 |
. . . . . . . . 9
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
39 | 14, 38 | sylan 479 |
. . . . . . . 8
              
         
        ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
40 | 39 | an32s 821 |
. . . . . . 7
              
          
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                           |
41 | 40 | ralrimiva 2809 |
. . . . . 6
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                            |
42 | | mptelee 25004 |
. . . . . . 7
                            
                        |
43 | 31, 42 | syl 17 |
. . . . . 6
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                               
                        |
44 | 41, 43 | mpbird 240 |
. . . . 5
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                |
45 | 44 | 3adant3 1050 |
. . . 4
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
                            |
46 | | fveecn 25011 |
. . . . . . . . . . . 12
     
           |
47 | 46 | expcom 442 |
. . . . . . . . . . 11
     
           |
48 | | fveecn 25011 |
. . . . . . . . . . . 12
     
           |
49 | 48 | expcom 442 |
. . . . . . . . . . 11
     
           |
50 | 47, 49 | anim12d 572 |
. . . . . . . . . 10
               
             |
51 | | fveecn 25011 |
. . . . . . . . . . . 12
     
           |
52 | 51 | expcom 442 |
. . . . . . . . . . 11
     
           |
53 | | fveecn 25011 |
. . . . . . . . . . . 12
     
           |
54 | 53 | expcom 442 |
. . . . . . . . . . 11
     
           |
55 | 52, 54 | anim12d 572 |
. . . . . . . . . 10
               
             |
56 | 50, 55 | anim12d 572 |
. . . . . . . . 9
           
                                         |
57 | 56 | impcom 437 |
. . . . . . . 8
       
               
                             |
58 | | eqcom 2478 |
. . . . . . . . . . . . . 14
                                                
                                                  |
59 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . . . . 19
 |
60 | | simpr2 1037 |
. . . . . . . . . . . . . . . . . . . 20
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
 
  ![[,] [,]](_icc.gif)    |
61 | 15 | sseli 3414 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)    |
62 | 61 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)    |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
 
  |
64 | | subcl 9894 |
. . . . . . . . . . . . . . . . . . 19
 
     |
65 | 59, 63, 64 | sylancr 676 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
      |
66 | | simpr1 1036 |
. . . . . . . . . . . . . . . . . . . . 21
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
 
  ![[,] [,]](_icc.gif)    |
67 | 16 | recnd 9687 |
. . . . . . . . . . . . . . . . . . . . 21
   ![[,] [,]](_icc.gif)    |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
 
  |
69 | | subcl 9894 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
70 | 68, 59, 69 | sylancl 675 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
      |
71 | | simplll 776 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
72 | 70, 71 | mulcld 9681 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
            |
73 | 65, 72 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                |
74 | 63, 72 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
              |
75 | 73, 74 | addcld 9680 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                            |
76 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
77 | 65, 76 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
            |
78 | | simplrl 778 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
79 | 63, 78 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
          |
80 | 77, 79 | addcld 9680 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
81 | 75, 80 | addcld 9680 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                              |
82 | | simplrr 779 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
83 | | simpr3 1038 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
    |
84 | 81, 68, 82, 83 | divmuld 10427 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                      |
85 | 58, 84 | syl5bb 265 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                      |
86 | | negsubdi2 9953 |
. . . . . . . . . . . . . . . . . . . 20
 
        |
87 | 59, 68, 86 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
         |
88 | 87 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                     |
89 | | subcl 9894 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
90 | 59, 68, 89 | sylancr 676 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
      |
91 | 90, 71 | mulneg1d 10092 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                      |
92 | | npcan 9904 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
93 | 59, 63, 92 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
        |
94 | 93 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                            |
95 | 65, 63, 72 | adddird 9686 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                          |
96 | 72 | mulid2d 9679 |
. . . . . . . . . . . . . . . . . . 19
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                      |
97 | 94, 95, 96 | 3eqtr3rd 2514 |
. . . . . . . . . . . . . . . . . 18
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                    |
98 | 88, 91, 97 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                     |
99 | 98 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                         |
100 | 90, 71 | mulcld 9681 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
            |
101 | 80, 100 | negsubd 10011 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                         |
102 | 80, 75 | addcomd 9853 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                        |
103 | 99, 101, 102 | 3eqtr3d 2513 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                        |
104 | 103 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  
                                                   |
105 | | eqcom 2478 |
. . . . . . . . . . . . . 14
                                                                                                   |
106 | 104, 105 | syl6bb 269 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  
                                                   |
107 | 85, 106 | bitr4d 264 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                      |
108 | 73, 74, 77, 79 | add4d 9878 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                        |
109 | 65, 72, 76 | adddid 9685 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                            |
110 | 63, 72, 78 | adddid 9685 |
. . . . . . . . . . . . . . . . 17
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                      |
111 | 109, 110 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                  |
112 | 108, 111 | eqtr4d 2508 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                  |
113 | 112 | oveq1d 6323 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                      |
114 | 72, 76 | addcld 9680 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                  |
115 | 65, 114 | mulcld 9681 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                      |
116 | 72, 78 | addcld 9680 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                  |
117 | 63, 116 | mulcld 9681 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                    |
118 | 115, 117,
68, 83 | divdird 10443 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                  |
119 | 65, 114, 68, 83 | divassd 10440 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                            |
120 | 63, 116, 68, 83 | divassd 10440 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                        |
121 | 119, 120 | oveq12d 6326 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                    |
122 | 113, 118,
121 | 3eqtrd 2509 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                        |
123 | 122 | eqeq2d 2481 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                  |
124 | 68, 82 | mulcld 9681 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
          |
125 | 80, 100, 124 | subaddd 10023 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  
                                   |
126 | 107, 123,
125 | 3bitr3rd 292 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                  |
127 | 126 | biimpd 212 |
. . . . . . . . . 10
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                  |
128 | | npncan2 9921 |
. . . . . . . . . . . . . . . . 17
 
         |
129 | 59, 68, 128 | sylancr 676 |
. . . . . . . . . . . . . . . 16
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
          |
130 | 129 | oveq1d 6323 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                      |
131 | 90, 70, 71 | adddird 9686 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  |
132 | | mul02 9829 |
. . . . . . . . . . . . . . . 16
             |
133 | 132 | ad3antrrr 744 |
. . . . . . . . . . . . . . 15
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
          |
134 | 130, 131,
133 | 3eqtr3d 2513 |
. . . . . . . . . . . . . 14
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                      |
135 | 134 | oveq1d 6323 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  |
136 | 100, 72, 76 | addassd 9683 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                    |
137 | 76 | addid2d 9852 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
              |
138 | 135, 136,
137 | 3eqtr3rd 2514 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                |
139 | 114, 68, 83 | divcan2d 10407 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                    |
140 | 139 | oveq2d 6324 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                        |
141 | 138, 140 | eqtr4d 2508 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                    |
142 | 134 | oveq1d 6323 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                  |
143 | 100, 72, 78 | addassd 9683 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                    |
144 | 78 | addid2d 9852 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
              |
145 | 142, 143,
144 | 3eqtr3rd 2514 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                |
146 | 116, 68, 83 | divcan2d 10407 |
. . . . . . . . . . . . 13
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                    |
147 | 146 | oveq2d 6324 |
. . . . . . . . . . . 12
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                        |
148 | 145, 147 | eqtr4d 2508 |
. . . . . . . . . . 11
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                    |
149 | 141, 148 | jca 541 |
. . . . . . . . . 10
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                      |
150 | 127, 149 | jctild 552 |
. . . . . . . . 9
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                                                                      |
151 | | df-3an 1009 |
. . . . . . . . 9
                                                                                                              
                                                                                                                  |
152 | 150, 151 | syl6ibr 235 |
. . . . . . . 8
                           ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                                                                    |
153 | 57, 152 | sylan 479 |
. . . . . . 7
              
         
        ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif) 
                                                                                                                                                    |
154 | 153 | an32s 821 |
. . . . . 6
              
          
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)                                                                                                                                                           |
155 | 154 | ralimdva 2805 |
. . . . 5
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     
                                                                                                                                                            |
156 | 155 | 3impia 1228 |
. . . 4
       
                
  ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)  
                                      
                                                                                                                      |
157 | | fveq1 5878 |
. . . . . . . 8
                                                       |
158 | | fveq2 5879 |
. . . . . . . . . . . 12
           |
159 | 158 | oveq2d 6324 |
. . . . . . . . . . 11
                   |
160 | | fveq2 5879 |
. . . . . . . . . . 11
           |
161 | 159, 160 | oveq12d 6326 |
. . . . . . . . . 10
                               |
162 | 161 | oveq1d 6323 |
. . . . . . . . 9
                                   |
163 | | eqid 2471 |
. . . . . . . . 9
                                             |
164 | | ovex 6336 |
. . . . . . . . 9
                 |
165 | 162, 163,
164 | fvmpt 5963 |
. . . . . . . 8
                                                 |
166 | 157, 165 | sylan9eq 2525 |
. . . . . . 7
                            
                      |
167 | | oveq2 6316 |
. . . . . . . . . 10
                     
                         |
168 | 167 | oveq2d 6324 |
. . . . . . . . 9
           |