Step | Hyp | Ref
| Expression |
1 | | brbtwn 24929 |
. 2
     
             
  ![[,] [,]](_icc.gif)                                |
2 | | fveere 24931 |
. . . . . . . . . 10
     
           |
3 | 2 | 3ad2antl2 1171 |
. . . . . . . . 9
                           |
4 | | fveere 24931 |
. . . . . . . . . 10
     
           |
5 | 4 | 3ad2antl3 1172 |
. . . . . . . . 9
                           |
6 | 3, 5 | jca 535 |
. . . . . . . 8
                                 |
7 | | resubcl 9938 |
. . . . . . . . . . . . . . 15
                       |
8 | 7 | 3adant3 1028 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)               |
9 | 8 | recnd 9669 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)               |
10 | 9 | sqvald 12413 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                                         |
11 | 10 | oveq2d 6306 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)                                                       |
12 | | 0re 9643 |
. . . . . . . . . . . . . . . 16
 |
13 | | 1re 9642 |
. . . . . . . . . . . . . . . 16
 |
14 | 12, 13 | elicc2i 11700 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif) 

   |
15 | 14 | simp1bi 1023 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)    |
16 | 15 | recnd 9669 |
. . . . . . . . . . . . 13
   ![[,] [,]](_icc.gif)    |
17 | 16 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)     |
18 | | resubcl 9938 |
. . . . . . . . . . . . . . . 16
 
     |
19 | 13, 15, 18 | sylancr 669 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)      |
20 | 19 | 3ad2ant3 1031 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)       |
21 | 20 | recnd 9669 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)       |
22 | 21 | negcld 9973 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)        |
23 | 17, 9, 22, 9 | mul4d 9845 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)                                                               |
24 | | recn 9629 |
. . . . . . . . . . . . . . 15
           |
25 | 24 | 3ad2ant1 1029 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)         |
26 | | recn 9629 |
. . . . . . . . . . . . . . 15
           |
27 | 26 | 3ad2ant2 1030 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)         |
28 | 17, 25, 27 | subdid 10074 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                               |
29 | | ax-1cn 9597 |
. . . . . . . . . . . . . . . . 17
 |
30 | | subdir 10053 |
. . . . . . . . . . . . . . . . 17
                                     |
31 | 29, 30 | mp3an1 1351 |
. . . . . . . . . . . . . . . 16
                                     |
32 | 21, 25, 31 | syl2anc 667 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                               |
33 | | nncan 9903 |
. . . . . . . . . . . . . . . . 17
 
       |
34 | 29, 17, 33 | sylancr 669 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)         |
35 | 34 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                     |
36 | 25 | mulid2d 9661 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)               |
37 | 36 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                                   |
38 | 32, 35, 37 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)                         |
39 | 38 | oveq1d 6305 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                                         |
40 | | simp1 1008 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)         |
41 | 20, 40 | remulcld 9671 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)             |
42 | 41 | recnd 9669 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)             |
43 | 15 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)     |
44 | | simp2 1009 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)         |
45 | 43, 44 | remulcld 9671 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)           |
46 | 45 | recnd 9669 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)           |
47 | 25, 42, 46 | subsub4d 10017 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                                                 |
48 | 28, 39, 47 | 3eqtrd 2489 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                                       |
49 | 21, 9 | mulneg1d 10071 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                                   |
50 | 21, 25, 27 | subdid 10074 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                                     |
51 | | subdir 10053 |
. . . . . . . . . . . . . . . . . . 19
 
                             |
52 | 29, 51 | mp3an1 1351 |
. . . . . . . . . . . . . . . . . 18
                               |
53 | 17, 27, 52 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
            ![[,] [,]](_icc.gif)                           |
54 | 27 | mulid2d 9661 |
. . . . . . . . . . . . . . . . . 18
            ![[,] [,]](_icc.gif)               |
55 | 54 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
            ![[,] [,]](_icc.gif)                               |
56 | 53, 55 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
            ![[,] [,]](_icc.gif)                         |
57 | 56 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                                             |
58 | 42, 27, 46 | subsub3d 10016 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                                                 |
59 | 50, 57, 58 | 3eqtrd 2489 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)                                         |
60 | 59 | negeqd 9869 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                                           |
61 | 41, 45 | readdcld 9670 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)                     |
62 | 61 | recnd 9669 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)                     |
63 | 62, 27 | negsubdi2d 10002 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                                                  |
64 | 49, 60, 63 | 3eqtrd 2489 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                                          |
65 | 48, 64 | oveq12d 6308 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)                                                                                |
66 | 11, 23, 65 | 3eqtr2rd 2492 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)                                                                        |
67 | 17, 21 | mulneg2d 10072 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)               |
68 | 67 | oveq1d 6305 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                                               |
69 | 43, 20 | remulcld 9671 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)         |
70 | 69 | recnd 9669 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)         |
71 | 8 | resqcld 12442 |
. . . . . . . . . . . . . 14
            ![[,] [,]](_icc.gif)                   |
72 | 71 | recnd 9669 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                   |
73 | 70, 72 | mulneg1d 10071 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                                               |
74 | 68, 73 | eqtrd 2485 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)                                               |
75 | 14 | simp2bi 1024 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
76 | 14 | simp3bi 1025 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)    |
77 | | subge0 10127 |
. . . . . . . . . . . . . . . . 17
 
   
   |
78 | 13, 15, 77 | sylancr 669 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)  
 
   |
79 | 76, 78 | mpbird 236 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)      |
80 | 15, 19, 75, 79 | mulge0d 10190 |
. . . . . . . . . . . . . 14
   ![[,] [,]](_icc.gif)        |
81 | 80 | 3ad2ant3 1031 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)         |
82 | 8 | sqge0d 12443 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                   |
83 | 69, 71, 81, 82 | mulge0d 10190 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)                         |
84 | 69, 71 | remulcld 9671 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)                         |
85 | 84 | le0neg2d 10186 |
. . . . . . . . . . . 12
            ![[,] [,]](_icc.gif)   
                   
                        |
86 | 83, 85 | mpbid 214 |
. . . . . . . . . . 11
            ![[,] [,]](_icc.gif)                          |
87 | 74, 86 | eqbrtrd 4423 |
. . . . . . . . . 10
            ![[,] [,]](_icc.gif)                          |
88 | 66, 87 | eqbrtrd 4423 |
. . . . . . . . 9
            ![[,] [,]](_icc.gif)                                                   |
89 | 88 | 3expa 1208 |
. . . . . . . 8
              ![[,] [,]](_icc.gif)  
                                                |
90 | 6, 89 | sylan 474 |
. . . . . . 7
       
                ![[,] [,]](_icc.gif)                                                   |
91 | 90 | an32s 813 |
. . . . . 6
       
           ![[,] [,]](_icc.gif)                                                        |
92 | 91 | ralrimiva 2802 |
. . . . 5
                  ![[,] [,]](_icc.gif)                                                         |
93 | | fveecn 24932 |
. . . . . . . . . . . 12
     
           |
94 | | fveecn 24932 |
. . . . . . . . . . . 12
     
           |
95 | 93, 94 | anim12i 570 |
. . . . . . . . . . 11
                                   |
96 | 95 | anandirs 840 |
. . . . . . . . . 10
                             |
97 | | fveecn 24932 |
. . . . . . . . . . . 12
     
           |
98 | | fveecn 24932 |
. . . . . . . . . . . 12
     
           |
99 | 97, 98 | anim12i 570 |
. . . . . . . . . . 11
                                   |
100 | 99 | anandirs 840 |
. . . . . . . . . 10
                             |
101 | 96, 100 | anim12dan 848 |
. . . . . . . . 9
                                               |
102 | 101 | 3adantl1 1164 |
. . . . . . . 8
                                                   |
103 | | subcl 9874 |
. . . . . . . . . . . . . 14
                       |
104 | 103 | 3ad2ant1 1029 |
. . . . . . . . . . . . 13
                                   |
105 | | subcl 9874 |
. . . . . . . . . . . . . . 15
                       |
106 | 105 | ancoms 455 |
. . . . . . . . . . . . . 14
                       |
107 | 106 | 3ad2ant2 1030 |
. . . . . . . . . . . . 13
                                   |
108 | 104, 107 | mulcomd 9664 |
. . . . . . . . . . . 12
                                                                     |
109 | | simp2r 1035 |
. . . . . . . . . . . . 13
                             |
110 | | simp2l 1034 |
. . . . . . . . . . . . 13
                             |
111 | | simp1l 1032 |
. . . . . . . . . . . . 13
                             |
112 | | simp1r 1033 |
. . . . . . . . . . . . 13
                             |
113 | | mulsub2 10062 |
. . . . . . . . . . . . 13
                                                                     |
114 | 109, 110,
111, 112, 113 | syl22anc 1269 |
. . . . . . . . . . . 12
                                                                     |
115 | 108, 114 | eqtrd 2485 |
. . . . . . . . . . 11
                                                                     |
116 | 115 | oveq2d 6306 |
. . . . . . . . . 10
                                                                                 |
117 | | simp3 1010 |
. . . . . . . . . . . 12
                         |
118 | | subcl 9874 |
. . . . . . . . . . . . . 14
 
     |
119 | 29, 118 | mpan 676 |
. . . . . . . . . . . . 13
     |
120 | 119 | 3ad2ant3 1031 |
. . . . . . . . . . . 12
                           |
121 | 117, 120,
104, 107 | mul4d 9845 |
. . . . . . . . . . 11
                                                                                 |
122 | 117, 111,
112 | subdid 10074 |
. . . . . . . . . . . . 13
                                                   |
123 | 120, 111,
31 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                                   |
124 | 29, 33 | mpan 676 |
. . . . . . . . . . . . . . . . 17
       |
125 | 124 | 3ad2ant3 1031 |
. . . . . . . . . . . . . . . 16
                             |
126 | 125 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                         |
127 | 111 | mulid2d 9661 |
. . . . . . . . . . . . . . . 16
                                   |
128 | 127 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                                       |
129 | 123, 126,
128 | 3eqtr3d 2493 |
. . . . . . . . . . . . . 14
                                             |
130 | 129 | oveq1d 6305 |
. . . . . . . . . . . . 13
                                                             |
131 | 120, 111 | mulcld 9663 |
. . . . . . . . . . . . . 14
                                 |
132 | 117, 112 | mulcld 9663 |
. . . . . . . . . . . . . 14
                               |
133 | 111, 131,
132 | subsub4d 10017 |
. . . . . . . . . . . . 13
                                                                     |
134 | 122, 130,
133 | 3eqtrd 2489 |
. . . . . . . . . . . 12
                                                           |
135 | 120, 109,
110 | subdid 10074 |
. . . . . . . . . . . . . 14
                                                         |
136 | | subdir 10053 |
. . . . . . . . . . . . . . . . . 18
 
                             |
137 | 29, 136 | mp3an1 1351 |
. . . . . . . . . . . . . . . . 17
                               |
138 | 117, 109,
137 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
                                               |
139 | 109 | mulid2d 9661 |
. . . . . . . . . . . . . . . . 17
                                   |
140 | 139 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                                                   |
141 | 138, 140 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
                                             |
142 | 141 | oveq1d 6305 |
. . . . . . . . . . . . . 14
                                                                 |
143 | 135, 142 | eqtrd 2485 |
. . . . . . . . . . . . 13
                                                             |
144 | 117, 109 | mulcld 9663 |
. . . . . . . . . . . . . 14
                               |
145 | 120, 110 | mulcld 9663 |
. . . . . . . . . . . . . 14
                                 |
146 | 109, 144,
145 | sub32d 10018 |
. . . . . . . . . . . . 13
                                                                     |
147 | 109, 145,
144 | subsub4d 10017 |
. . . . . . . . . . . . 13
                                                                     |
148 | 143, 146,
147 | 3eqtrd 2489 |
. . . . . . . . . . . 12
                                                             |
149 | 134, 148 | oveq12d 6308 |
. . . . . . . . . . 11
                                                                                                   |
150 | 121, 149 | eqtrd 2485 |
. . . . . . . . . 10
                                                                                                   |
151 | | subcl 9874 |
. . . . . . . . . . . . 13
                       |
152 | 151 | 3ad2ant2 1030 |
. . . . . . . . . . . 12
                                   |
153 | | subcl 9874 |
. . . . . . . . . . . . . 14
                       |
154 | 153 | ancoms 455 |
. . . . . . . . . . . . 13
                       |
155 | 154 | 3ad2ant1 1029 |
. . . . . . . . . . . 12
                                   |
156 | 117, 120,
152, 155 | mul4d 9845 |
. . . . . . . . . . 11
                                                                                 |
157 | 117, 110,
109 | subdid 10074 |
. . . . . . . . . . . . 13
                                                   |
158 | | subdir 10053 |
. . . . . . . . . . . . . . . . 17
                                     |
159 | 29, 158 | mp3an1 1351 |
. . . . . . . . . . . . . . . 16
                                     |
160 | 120, 110,
159 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                                   |
161 | 125 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                         |
162 | 110 | mulid2d 9661 |
. . . . . . . . . . . . . . . 16
                                   |
163 | 162 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                                       |
164 | 160, 161,
163 | 3eqtr3rd 2494 |
. . . . . . . . . . . . . 14
                                             |
165 | 164 | oveq1d 6305 |
. . . . . . . . . . . . 13
                                                             |
166 | 110, 145,
144 | subsub4d 10017 |
. . . . . . . . . . . . 13
                                                                     |
167 | 157, 165,
166 | 3eqtr2d 2491 |
. . . . . . . . . . . 12
                                                           |
168 | 120, 112,
111 | subdid 10074 |
. . . . . . . . . . . . 13
                                                         |
169 | 117, 112,
52 | syl2anc 667 |
. . . . . . . . . . . . . . 15
                                               |
170 | 112 | mulid2d 9661 |
. . . . . . . . . . . . . . . 16
                                   |
171 | 170 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                                                   |
172 | 169, 171 | eqtrd 2485 |
. . . . . . . . . . . . . 14
                                             |
173 | 172 | oveq1d 6305 |
. . . . . . . . . . . . 13
                                                                 |
174 | 112, 132,
131 | sub32d 10018 |
. . . . . . . . . . . . . 14
                                                                     |
175 | 112, 131,
132 | subsub4d 10017 |
. . . . . . . . . . . . . 14
                                                                     |
176 | 174, 175 | eqtrd 2485 |
. . . . . . . . . . . . 13
                                                                     |
177 | 168, 173,
176 | 3eqtrd 2489 |
. . . . . . . . . . . 12
                                                             |
178 | 167, 177 | oveq12d 6308 |
. . . . . . . . . . 11
                                                                                                   |
179 | 156, 178 | eqtrd 2485 |
. . . . . . . . . 10
                                                                                                   |
180 | 116, 150,
179 | 3eqtr3d 2493 |
. . . . . . . . 9
                                                                                                                     |
181 | 180 | 3expa 1208 |
. . . . . . . 8
                                                                                                                       |
182 | 102, 16, 181 | syl2an 480 |
. . . . . . 7
       
                   
  ![[,] [,]](_icc.gif)                                                                                                 |
183 | 182 | an32s 813 |
. . . . . 6
       
           ![[,] [,]](_icc.gif)       
     
                                                                                              |
184 | 183 | ralrimivva 2809 |
. . . . 5
                  ![[,] [,]](_icc.gif)                                                                                                             |
185 | | fveq2 5865 |
. . . . . . . . . . 11
           |
186 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
187 | 186 | oveq2d 6306 |
. . . . . . . . . . . 12
                   |
188 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
189 | 188 | oveq2d 6306 |
. . . . . . . . . . . 12
               |
190 | 187, 189 | oveq12d 6308 |
. . . . . . . . . . 11
                                   |
191 | 185, 190 | eqeq12d 2466 |
. . . . . . . . . 10
                     
                       |
192 | 191 | rspccva 3149 |
. . . . . . . . 9
                           
                           |
193 | | oveq2 6298 |
. . . . . . . . . . 11
                                                       |
194 | | oveq2 6298 |
. . . . . . . . . . 11
                                                       |
195 | 193, 194 | oveq12d 6308 |
. . . . . . . . . 10
                                                                                           |
196 | 195 | breq1d 4412 |
. . . . . . . . 9
                                           
                                                 |
197 | 192, 196 | syl 17 |
. . . . . . . 8
                           
                                                                             |
198 | 197 | ralbidva 2824 |
. . . . . . 7
 
                          
                          
                                                       |
199 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
200 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
201 | 200 | oveq2d 6306 |
. . . . . . . . . . . . 13
                   |
202 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
203 | 202 | oveq2d 6306 |
. . . . . . . . . . . . 13
               |
204 | 201, 203 | oveq12d 6308 |
. . . . . . . . . . . 12
                                   |
205 | 199, 204 | eqeq12d 2466 |
. . . . . . . . . . 11
                     
                       |
206 | 205 | rspccva 3149 |
. . . . . . . . . 10
                           
                           |
207 | | oveq2 6298 |
. . . . . . . . . . . 12
                                                       |
208 | 193, 207 | oveqan12d 6309 |
. . . . . . . . . . 11
                                                                                                                 |
209 | | oveq2 6298 |
. . . . . . . . . . . 12
                                                       |
210 | 209, 194 | oveqan12rd 6310 |
. . . . . . . . . . 11
                                                                                                                 |
211 | 208, 210 | eqeq12d 2466 |
. . . . . . . . . 10
                                                                                                                                                                                       |
212 | 192, 206,
211 | syl2an 480 |
. . . . . . . . 9
                                   
                                                                                                                                                                           |
213 | 212 | anandis 839 |
. . . . . . . 8
                                                                                   
                                                                                               |
214 | 213 | 2ralbidva 2830 |
. . . . . . 7
 
                          
     
                                                
                                                                                                           |
215 | 198, 214 | anbi12d 717 |
. . . . . 6
 
                                                                                                               
 
                                                   
     
                                                                                                     |
216 | 215 | biimprcd 229 |
. . . . 5
                                                     
      
                                                                                                                                                                                                                      |
217 | 92, 184, 216 | syl2anc 667 |
. . . 4
                  ![[,] [,]](_icc.gif)    
                          
                           
     
               |