Proof of Theorem axcontlem7
Step | Hyp | Ref
| Expression |
1 | | axcontlem7.1 |
. . . . . 6
|
2 | | ssrab2 3687 |
. . . . . 6
|
3 | 1, 2 | eqsstri 3635 |
. . . . 5
|
4 | 3 | sseli 3599 |
. . . 4
|
5 | 4 | ad2antrl 764 |
. . 3
|
6 | | simpll2 1101 |
. . 3
|
7 | 3 | sseli 3599 |
. . . 4
|
8 | 7 | ad2antll 765 |
. . 3
|
9 | | brbtwn 25779 |
. . 3
|
10 | 5, 6, 8, 9 | syl3anc 1326 |
. 2
|
11 | | axcontlem7.2 |
. . . . 5
|
12 | 1, 11 | axcontlem6 25849 |
. . . 4
|
13 | 1, 11 | axcontlem6 25849 |
. . . 4
|
14 | 12, 13 | anim12dan 882 |
. . 3
|
15 | | an4 865 |
. . . . 5
|
16 | | r19.26 3064 |
. . . . . 6
|
17 | 16 | anbi2i 730 |
. . . . 5
|
18 | 15, 17 | bitr4i 267 |
. . . 4
|
19 | | id 22 |
. . . . . . . . . 10
|
20 | | oveq2 6658 |
. . . . . . . . . . 11
|
21 | 20 | oveq2d 6666 |
. . . . . . . . . 10
|
22 | 19, 21 | eqeqan12d 2638 |
. . . . . . . . 9
|
23 | 22 | ralimi 2952 |
. . . . . . . 8
|
24 | | ralbi 3068 |
. . . . . . . 8
|
25 | 23, 24 | syl 17 |
. . . . . . 7
|
26 | 25 | rexbidv 3052 |
. . . . . 6
|
27 | | simpll2 1101 |
. . . . . . . . . . . . 13
|
28 | | fveecn 25782 |
. . . . . . . . . . . . 13
|
29 | 27, 28 | sylan 488 |
. . . . . . . . . . . 12
|
30 | | simpll3 1102 |
. . . . . . . . . . . . 13
|
31 | | fveecn 25782 |
. . . . . . . . . . . . 13
|
32 | 30, 31 | sylan 488 |
. . . . . . . . . . . 12
|
33 | | 0re 10040 |
. . . . . . . . . . . . . . . . 17
|
34 | | 1re 10039 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | elicc2i 12239 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | simp1bi 1076 |
. . . . . . . . . . . . . . 15
|
37 | 36 | recnd 10068 |
. . . . . . . . . . . . . 14
|
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . 13
|
39 | 38 | adantr 481 |
. . . . . . . . . . . 12
|
40 | | elrege0 12278 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
42 | 41 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
43 | 42 | adantr 481 |
. . . . . . . . . . . . . 14
|
44 | 43 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
|
46 | | elrege0 12278 |
. . . . . . . . . . . . . . . . 17
|
47 | 46 | simplbi 476 |
. . . . . . . . . . . . . . . 16
|
48 | 47 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . 14
|
50 | 49 | ad2antrl 764 |
. . . . . . . . . . . . 13
|
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
|
52 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . 17
|
53 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . 18
|
54 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . 18
|
55 | 53, 54 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
|
56 | | subcl 10280 |
. . . . . . . . . . . . . . . . 17
|
57 | 52, 55, 56 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
58 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 52, 58 | mpan 706 |
. . . . . . . . . . . . . . . . . 18
|
60 | 59 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
62 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
63 | 57, 61, 62 | subdird 10487 |
. . . . . . . . . . . . . . 15
|
64 | | simpr2 1068 |
. . . . . . . . . . . . . . . . 17
|
65 | | nnncan1 10317 |
. . . . . . . . . . . . . . . . . 18
|
66 | 52, 65 | mp3an1 1411 |
. . . . . . . . . . . . . . . . 17
|
67 | 55, 64, 66 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
68 | 67 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
69 | | subdi 10463 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | 52, 69 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . 22
|
71 | | mulid1 10037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | 72 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 70, 73 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 53, 54, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 75 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
77 | | npncan 10302 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 52, 77 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 53, 55, 78 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 76, 79 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
|
81 | 80 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
82 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | 52, 82 | mpan 706 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 83 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
86 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 52, 86 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
90 | 53, 89 | mulcld 10060 |
. . . . . . . . . . . . . . . . . 18
|
91 | 85, 90, 62 | adddird 10065 |
. . . . . . . . . . . . . . . . 17
|
92 | 53, 89, 62 | mulassd 10063 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
94 | 81, 91, 93 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
96 | 63, 68, 95 | 3eqtr3d 2664 |
. . . . . . . . . . . . . 14
|
97 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
98 | 64, 55, 97 | subdird 10487 |
. . . . . . . . . . . . . . 15
|
99 | 53, 54, 97 | mulassd 10063 |
. . . . . . . . . . . . . . . 16
|
100 | 99 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
101 | 98, 100 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
102 | 96, 101 | eqeq12d 2637 |
. . . . . . . . . . . . 13
|
103 | 61, 62 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
104 | 64, 97 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
105 | 85, 62 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
106 | 89, 62 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
|
107 | 53, 106 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
108 | 105, 107 | addcld 10059 |
. . . . . . . . . . . . . 14
|
109 | 54, 97 | mulcld 10060 |
. . . . . . . . . . . . . . 15
|
110 | 53, 109 | mulcld 10060 |
. . . . . . . . . . . . . 14
|
111 | 103, 104,
108, 110 | addsubeq4d 10443 |
. . . . . . . . . . . . 13
|
112 | 105, 107,
110 | addassd 10062 |
. . . . . . . . . . . . . . 15
|
113 | 53, 106, 109 | adddid 10064 |
. . . . . . . . . . . . . . . 16
|
114 | 113 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
115 | 112, 114 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
116 | 115 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
117 | 102, 111,
116 | 3bitr2rd 297 |
. . . . . . . . . . . 12
|
118 | 29, 32, 39, 45, 51, 117 | syl23anc 1333 |
. . . . . . . . . . 11
|
119 | 118 | ralbidva 2985 |
. . . . . . . . . 10
|
120 | 39, 51 | mulcld 10060 |
. . . . . . . . . . . . 13
|
121 | 45, 120 | subcld 10392 |
. . . . . . . . . . . 12
|
122 | | mulcan1g 10680 |
. . . . . . . . . . . 12
|
123 | 121, 29, 32, 122 | syl3anc 1326 |
. . . . . . . . . . 11
|
124 | 123 | ralbidva 2985 |
. . . . . . . . . 10
|
125 | | r19.32v 3083 |
. . . . . . . . . . 11
|
126 | | simplr 792 |
. . . . . . . . . . . . . 14
|
127 | 126 | neneqd 2799 |
. . . . . . . . . . . . 13
|
128 | | biorf 420 |
. . . . . . . . . . . . . 14
|
129 | | orcom 402 |
. . . . . . . . . . . . . 14
|
130 | 128, 129 | syl6bb 276 |
. . . . . . . . . . . . 13
|
131 | 127, 130 | syl 17 |
. . . . . . . . . . . 12
|
132 | 38, 50 | mulcld 10060 |
. . . . . . . . . . . . 13
|
133 | 44, 132 | subeq0ad 10402 |
. . . . . . . . . . . 12
|
134 | | eqeefv 25783 |
. . . . . . . . . . . . . . . 16
|
135 | 134 | 3adant1 1079 |
. . . . . . . . . . . . . . 15
|
136 | 135 | adantr 481 |
. . . . . . . . . . . . . 14
|
137 | 136 | adantr 481 |
. . . . . . . . . . . . 13
|
138 | 137 | orbi2d 738 |
. . . . . . . . . . . 12
|
139 | 131, 133,
138 | 3bitr3rd 299 |
. . . . . . . . . . 11
|
140 | 125, 139 | syl5bb 272 |
. . . . . . . . . 10
|
141 | 119, 124,
140 | 3bitrd 294 |
. . . . . . . . 9
|
142 | 141 | anassrs 680 |
. . . . . . . 8
|
143 | 142 | rexbidva 3049 |
. . . . . . 7
|
144 | 36 | adantl 482 |
. . . . . . . . . . . . 13
|
145 | | 1red 10055 |
. . . . . . . . . . . . 13
|
146 | 46 | biimpi 206 |
. . . . . . . . . . . . . 14
|
147 | 146 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
148 | 35 | simp3bi 1078 |
. . . . . . . . . . . . . 14
|
149 | 148 | adantl 482 |
. . . . . . . . . . . . 13
|
150 | | lemul1a 10877 |
. . . . . . . . . . . . 13
|
151 | 144, 145,
147, 149, 150 | syl31anc 1329 |
. . . . . . . . . . . 12
|
152 | 48 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
153 | 152 | mulid2d 10058 |
. . . . . . . . . . . 12
|
154 | 151, 153 | breqtrd 4679 |
. . . . . . . . . . 11
|
155 | | breq1 4656 |
. . . . . . . . . . 11
|
156 | 154, 155 | syl5ibrcom 237 |
. . . . . . . . . 10
|
157 | 156 | rexlimdva 3031 |
. . . . . . . . 9
|
158 | | 0elunit 12290 |
. . . . . . . . . . . . . 14
|
159 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
160 | 48 | mul02d 10234 |
. . . . . . . . . . . . . . . 16
|
161 | 160 | adantl 482 |
. . . . . . . . . . . . . . 15
|
162 | 159, 161 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
163 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
164 | 163 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
165 | 164 | rspcev 3309 |
. . . . . . . . . . . . . 14
|
166 | 158, 162,
165 | sylancr 695 |
. . . . . . . . . . . . 13
|
167 | 166 | adantrl 752 |
. . . . . . . . . . . 12
|
168 | 167 | a1d 25 |
. . . . . . . . . . 11
|
169 | 168 | ex 450 |
. . . . . . . . . 10
|
170 | | simp3 1063 |
. . . . . . . . . . . . 13
|
171 | 41 | adantr 481 |
. . . . . . . . . . . . . . 15
|
172 | 171 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
173 | 40 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
174 | 173 | adantr 481 |
. . . . . . . . . . . . . . 15
|
175 | 174 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
176 | 47 | adantl 482 |
. . . . . . . . . . . . . . 15
|
177 | 176 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
178 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
179 | | simp1 1061 |
. . . . . . . . . . . . . . . 16
|
180 | 172, 175,
179 | ne0gt0d 10174 |
. . . . . . . . . . . . . . 15
|
181 | 178, 172,
177, 180, 170 | ltletrd 10197 |
. . . . . . . . . . . . . 14
|
182 | | divelunit 12314 |
. . . . . . . . . . . . . 14
|
183 | 172, 175,
177, 181, 182 | syl22anc 1327 |
. . . . . . . . . . . . 13
|
184 | 170, 183 | mpbird 247 |
. . . . . . . . . . . 12
|
185 | 43 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
186 | 49 | 3ad2ant2 1083 |
. . . . . . . . . . . . . 14
|
187 | 181 | gt0ne0d 10592 |
. . . . . . . . . . . . . 14
|
188 | 185, 186,
187 | divcan1d 10802 |
. . . . . . . . . . . . 13
|
189 | 188 | eqcomd 2628 |
. . . . . . . . . . . 12
|
190 | | oveq1 6657 |
. . . . . . . . . . . . . 14
|
191 | 190 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
192 | 191 | rspcev 3309 |
. . . . . . . . . . . 12
|
193 | 184, 189,
192 | syl2anc 693 |
. . . . . . . . . . 11
|
194 | 193 | 3exp 1264 |
. . . . . . . . . 10
|
195 | 169, 194 | pm2.61ine 2877 |
. . . . . . . . 9
|
196 | 157, 195 | impbid 202 |
. . . . . . . 8
|
197 | 196 | adantl 482 |
. . . . . . 7
|
198 | 143, 197 | bitrd 268 |
. . . . . 6
|
199 | 26, 198 | sylan9bbr 737 |
. . . . 5
|
200 | 199 | anasss 679 |
. . . 4
|
201 | 18, 200 | sylan2b 492 |
. . 3
|
202 | 14, 201 | syldan 487 |
. 2
|
203 | 10, 202 | bitrd 268 |
1
|