Proof of Theorem isosctrlem2
Step | Hyp | Ref
| Expression |
1 | | 1cnd 9677 |
. . . . . . 7
                    |
2 | | simpl1 1033 |
. . . . . . 7
                 
  |
3 | 1, 2 | negsubd 10011 |
. . . . . 6
                         |
4 | | 1rp 11329 |
. . . . . . . 8
 |
5 | 4 | a1i 11 |
. . . . . . 7
                    |
6 | | simpl3 1035 |
. . . . . . . . 9
                 
  |
7 | | simpl2 1034 |
. . . . . . . . . . 11
                        |
8 | 1, 2, 1 | sub32d 10037 |
. . . . . . . . . . . . . . 15
                            |
9 | | 1m1e0 10700 |
. . . . . . . . . . . . . . . . 17
   |
10 | 9 | oveq1i 6318 |
. . . . . . . . . . . . . . . 16
       |
11 | | df-neg 9883 |
. . . . . . . . . . . . . . . 16
    |
12 | 10, 11 | eqtr4i 2496 |
. . . . . . . . . . . . . . 15
      |
13 | 8, 12 | syl6eq 2521 |
. . . . . . . . . . . . . 14
                         |
14 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . . 19
     
   |
15 | | simp1 1030 |
. . . . . . . . . . . . . . . . . . 19
     
   |
16 | 14, 15 | subcld 10005 |
. . . . . . . . . . . . . . . . . 18
     
     |
17 | 16 | adantr 472 |
. . . . . . . . . . . . . . . . 17
                      |
18 | | ax-1cn 9615 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
19 | | subeq0 9920 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       |
20 | 18, 19 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
21 | 20 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . 21
       |
22 | 21 | con3dimp 448 |
. . . . . . . . . . . . . . . . . . . 20
 

    |
23 | 22 | neqned 2650 |
. . . . . . . . . . . . . . . . . . 19
 

    |
24 | 23 | 3adant2 1049 |
. . . . . . . . . . . . . . . . . 18
     
     |
25 | 24 | adantr 472 |
. . . . . . . . . . . . . . . . 17
                      |
26 | 17, 25 | recrecd 10402 |
. . . . . . . . . . . . . . . 16
                            |
27 | 14, 16, 24 | div2negd 10420 |
. . . . . . . . . . . . . . . . . . 19
     
             |
28 | 27 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
                              |
29 | 15 | negcld 9992 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
    |
30 | 29, 16, 24 | cjdivd 13363 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                         |
31 | 15 | cjnegd 13351 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
             |
32 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
33 | | abs0 13425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
34 | 32, 33 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       |
35 | | eqtr2 2491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
36 | 34, 35 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
37 | | ax-1ne0 9626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
39 | 38 | neneqd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31

  |
40 | 37, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
  |
41 | 36, 40 | pm2.65da 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
    
  |
42 | 41 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
  |
43 | | df-ne 2643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
44 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                   |
45 | | sq1 12407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
46 | 44, 45 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
               |
47 | 46 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                 |
48 | | absvalsq 13420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
49 | 48 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                       |
50 | 47, 49 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
51 | 50 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
               |
52 | 51 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                   |
53 | | simp1 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
54 | 53 | cjcld 13336 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
55 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
56 | 54, 53, 55 | divcan3d 10410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     |
57 | 52, 56 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
58 | 43, 57 | syl3an3br 1333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
         |
59 | 42, 58 | mpd3an3 1391 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
60 | 59 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
61 | 60 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
         |
62 | 61 | negeqd 9889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           |
63 | 31, 62 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           |
64 | 63 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                           |
65 | | cjsub 13289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                   |
66 | 18, 65 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
67 | | 1red 9676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
68 | 67 | cjred 13366 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       |
69 | 68 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                   |
70 | 66, 69 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
71 | 70 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
72 | 60 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
73 | 71, 72 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
74 | 73 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
             |
75 | 74 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                       |
76 | 30, 64, 75 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . . 21
     
                     |
77 | 41 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
78 | 77 | neqned 2650 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
   |
79 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
80 | | simpl 464 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
  |
81 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
82 | 79, 80, 81 | divnegd 10418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
83 | 82 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . 23
                       |
84 | 15, 78, 83 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                     |
85 | 14 | negcld 9992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
    |
86 | 85, 15, 78 | divcld 10405 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
      |
87 | 15, 78 | reccld 10398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
     |
88 | 14, 87 | subcld 10005 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       |
89 | 16, 24 | cjne0d 13343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
         |
90 | 74, 89 | eqnetrrd 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       |
91 | 86, 88, 15, 90, 78 | divcan5d 10431 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
                 |
92 | 85, 15, 78 | divcan2d 10407 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
93 | 15, 14, 87 | subdid 10095 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
                 |
94 | 15 | mulid1d 9678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
     |
95 | 15, 78 | recidd 10400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
       |
96 | 94, 95 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
    
        |
97 | 93, 96 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
           |
98 | 92, 97 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       
             |
99 | 84, 91, 98 | 3eqtr2d 2511 |
. . . . . . . . . . . . . . . . . . . . 21
     
            
    |
100 | | subcl 9894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
101 | 100 | negnegd 9996 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
         |
102 | | negsubdi2 9953 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        |
103 | 102 | negeqd 9889 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
          |
104 | 101, 103 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        |
105 | 15, 14, 104 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . 22
     
        |
106 | 105 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . . . . 21
     
              |
107 | 76, 99, 106 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . . . . . 20
     
                  |
108 | 107 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                                   |
109 | 29, 16, 24 | divcld 10405 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
        |
110 | 109 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
                         |
111 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . 22
                             |
112 | 110, 111 | reim0bd 13340 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
113 | 112 | cjred 13366 |
. . . . . . . . . . . . . . . . . . . 20
                                  |
114 | 113, 112 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . 19
                             |
115 | 108, 114 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . 18
                          |
116 | 28, 115 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
                        |
117 | 16, 24 | recne0d 10399 |
. . . . . . . . . . . . . . . . . 18
     
       |
118 | 117 | adantr 472 |
. . . . . . . . . . . . . . . . 17
                        |
119 | 116, 118 | rereccld 10456 |
. . . . . . . . . . . . . . . 16
                          |
120 | 26, 119 | eqeltrrd 2550 |
. . . . . . . . . . . . . . 15
                      |
121 | | 1red 9676 |
. . . . . . . . . . . . . . 15
                    |
122 | 120, 121 | resubcld 10068 |
. . . . . . . . . . . . . 14
                        |
123 | 13, 122 | eqeltrrd 2550 |
. . . . . . . . . . . . 13
                     |
124 | 2, 123 | negrebd 10004 |
. . . . . . . . . . . 12
                 
  |
125 | 124 | absord 13554 |
. . . . . . . . . . 11
                               |
126 | | eqeq1 2475 |
. . . . . . . . . . . . 13
         
   |
127 | 126 | biimpd 212 |
. . . . . . . . . . . 12
             |
128 | | eqeq1 2475 |
. . . . . . . . . . . . 13
               |
129 | 128 | biimpd 212 |
. . . . . . . . . . . 12
               |
130 | 127, 129 | orim12d 856 |
. . . . . . . . . . 11
                       |
131 | 7, 125, 130 | sylc 61 |
. . . . . . . . . 10
                       |
132 | 131 | ord 384 |
. . . . . . . . 9
                  
    |
133 | 6, 132 | mpd 15 |
. . . . . . . 8
                     |
134 | 133, 5 | eqeltrrd 2550 |
. . . . . . 7
                     |
135 | 5, 134 | rpaddcld 11379 |
. . . . . 6
                       |
136 | 3, 135 | eqeltrrd 2550 |
. . . . 5
                      |
137 | 136 | relogcld 23651 |
. . . 4
                          |
138 | 137 | reim0d 13365 |
. . 3
                              |
139 | 134, 136 | rpdivcld 11381 |
. . . . 5
                         |
140 | 139 | relogcld 23651 |
. . . 4
                             |
141 | 140 | reim0d 13365 |
. . 3
                                 |
142 | 138, 141 | eqtr4d 2508 |
. 2
                                           |
143 | 16, 24 | logcld 23599 |
. . . . . 6
     
         |
144 | 143 | adantr 472 |
. . . . 5
                          |
145 | 144 | imcld 13335 |
. . . 4
                              |
146 | 145 | recnd 9687 |
. . 3
                              |
147 | 109 | adantr 472 |
. . . . . 6
                         |
148 | 15, 78 | negne0d 10003 |
. . . . . . . 8
     
    |
149 | 29, 16, 148, 24 | divne0d 10421 |
. . . . . . 7
     
        |
150 | 149 | adantr 472 |
. . . . . 6
                         |
151 | 147, 150 | logcld 23599 |
. . . . 5
                             |
152 | 151 | imcld 13335 |
. . . 4
                                 |
153 | 152 | recnd 9687 |
. . 3
                                 |
154 | 107 | fveq2d 5883 |
. . . . . . 7
     
                          |
155 | 154 | adantr 472 |
. . . . . 6
                                           |
156 | | logcj 23634 |
. . . . . . 7
                                             |
157 | 109, 156 | sylan 479 |
. . . . . 6
                                              |
158 | 16, 24 | reccld 10398 |
. . . . . . . . . 10
     
       |
159 | 158, 117 | logcld 23599 |
. . . . . . . . 9
     
           |
160 | 159 | negnegd 9996 |
. . . . . . . 8
     
                     |
161 | | isosctrlem1 23826 |
. . . . . . . . . 10
     
             |
162 | | logrec 23779 |
. . . . . . . . . 10
                                  |
163 | 16, 24, 161, 162 | syl3anc 1292 |
. . . . . . . . 9
     
                  |
164 | 163 | negeqd 9889 |
. . . . . . . 8
     
                    |
165 | 27 | fveq2d 5883 |
. . . . . . . 8
     
                     |
166 | 160, 164,
165 | 3eqtr4rd 2516 |
. . . . . . 7
     
                    |
167 | 166 | adantr 472 |
. . . . . 6
                                     |
168 | 155, 157,
167 | 3eqtr3rd 2514 |
. . . . 5
                                        |
169 | 168 | fveq2d 5883 |
. . . 4
                                                |
170 | 144 | imnegd 13350 |
. . . 4
                                          |
171 | 151 | imcjd 13345 |
. . . 4
                                                   |
172 | 169, 170,
171 | 3eqtr3d 2513 |
. . 3
                                             |
173 | 146, 153,
172 | neg11d 10017 |
. 2
                                           |
174 | 142, 173 | pm2.61dane 2730 |
1
     
                          |