Step | Hyp | Ref
| Expression |
1 | | simplr1 1103 |
. 2
|
2 | | n0 3931 |
. . . . . 6
|
3 | | idd 24 |
. . . . . . . . . 10
|
4 | | ssel 3597 |
. . . . . . . . . . 11
|
5 | 4 | com12 32 |
. . . . . . . . . 10
|
6 | | opeq2 4403 |
. . . . . . . . . . . . 13
|
7 | 6 | breq2d 4665 |
. . . . . . . . . . . 12
|
8 | 7 | rspcv 3305 |
. . . . . . . . . . 11
|
9 | 8 | ralimdv 2963 |
. . . . . . . . . 10
|
10 | 3, 5, 9 | 3anim123d 1406 |
. . . . . . . . 9
|
11 | 10 | anim2d 589 |
. . . . . . . 8
|
12 | | simplr1 1103 |
. . . . . . . . . . . . . . . 16
|
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . 15
|
14 | | simplr2 1104 |
. . . . . . . . . . . . . . 15
|
15 | 13, 14 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
16 | | simpr3 1069 |
. . . . . . . . . . . . . . . 16
|
17 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
|
18 | | breq1 4656 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
|
20 | 16, 17, 19 | syl2an 494 |
. . . . . . . . . . . . . . 15
|
21 | 20 | adantr 481 |
. . . . . . . . . . . . . 14
|
22 | 15, 21 | jca 554 |
. . . . . . . . . . . . 13
|
23 | 12 | sselda 3603 |
. . . . . . . . . . . . 13
|
24 | 16 | adantr 481 |
. . . . . . . . . . . . . 14
|
25 | | breq1 4656 |
. . . . . . . . . . . . . . 15
|
26 | 25 | rspccva 3308 |
. . . . . . . . . . . . . 14
|
27 | 24, 26 | sylan 488 |
. . . . . . . . . . . . 13
|
28 | 22, 23, 27 | jca32 558 |
. . . . . . . . . . . 12
|
29 | | an4 865 |
. . . . . . . . . . . 12
|
30 | 28, 29 | sylib 208 |
. . . . . . . . . . 11
|
31 | | simp2 1062 |
. . . . . . . . . . . . . 14
|
32 | | simpl2r 1115 |
. . . . . . . . . . . . . . . . . . . . . 22
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 34 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
37 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
38 | | 1m0e1 11131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
39 | 37, 38 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
40 | 39 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
41 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
42 | 40, 41 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
43 | 42 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
44 | 36, 43 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
45 | 44 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
46 | 45 | biimpac 503 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
47 | | simpl2l 1114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
48 | | simpl3l 1116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
49 | | eqeefv 25783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
50 | 47, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
51 | | fveecn 25782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
52 | 47, 51 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
53 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
54 | 53 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
55 | | fveecn 25782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
56 | 54, 55 | sylancom 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
57 | | mulid2 10038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
58 | | mul02 10214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
59 | 57, 58 | oveqan12d 6669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
60 | | addid1 10216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
62 | 59, 61 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
63 | 52, 56, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
64 | 63 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
65 | 64 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
66 | 50, 65 | bitr4d 271 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
67 | 46, 66 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
68 | 67 | expdimp 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
69 | 35, 68 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 69 | necon3d 2815 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 33, 70 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
73 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
74 | 72, 73, 53 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . 22
|
75 | | simp2l 1087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
76 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
77 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
78 | 76, 77 | elicc2i 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
79 | 78 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
80 | 75, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
81 | | simp2r 1088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
82 | 76, 77 | elicc2i 12239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
83 | 82 | simp1bi 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
84 | 81, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
85 | 80, 84 | letrid 10189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
86 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
87 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
88 | 78 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
89 | 75, 88 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
91 | 84 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
92 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
93 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
94 | 80, 89, 93 | ne0gt0d 10174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
95 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
96 | 92, 87, 91, 95, 86 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
97 | | divelunit 12314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
98 | 87, 90, 91, 96, 97 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
99 | 86, 98 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
100 | | simp12 1092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
101 | 100 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
102 | 101, 51 | sylancom 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
103 | | simp13 1093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
104 | 103 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
105 | 104, 55 | sylancom 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
106 | 79 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
107 | 75, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
108 | 107 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
109 | 83 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
110 | 81, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
111 | 110 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
112 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
113 | 80 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
114 | 84 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
115 | 89 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
116 | | simpll3 1102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
117 | 113, 115,
116 | ne0gt0d 10174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
118 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
119 | 112, 113,
114, 117, 118 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
120 | 119 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
121 | | divcl 10691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
122 | 121 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
123 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
124 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
125 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
126 | 123, 124,
125 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
127 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
128 | 126, 127 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
129 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
130 | 124, 129 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
131 | 122, 128,
130 | adddid 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
132 | 131 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
133 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
134 | 123, 122,
133 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
135 | 134, 127 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
136 | 122, 128 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
137 | 122, 130 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
138 | 135, 136,
137 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
139 | 122, 126 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
140 | 134, 139,
127 | adddird 10065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
141 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
142 | | subdi 10463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
143 | 123, 142 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
144 | 121, 141,
143 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
145 | 121 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
146 | | divcan1 10694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
147 | 145, 146 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
148 | 144, 147 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
149 | 148 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
150 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
151 | | npncan 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
152 | 123, 151 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
153 | 121, 150,
152 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
154 | 149, 153 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
155 | 154 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
156 | 155 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
157 | 122, 126,
127 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
158 | 157 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
159 | 140, 156,
158 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
160 | 122, 124,
129 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
161 | 146 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
162 | 161 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
163 | 160, 162 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
164 | 159, 163 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
165 | 132, 138,
164 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
166 | 102, 105,
108, 111, 120, 165 | syl23anc 1333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
167 | 166 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
168 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
169 | 168 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
170 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
171 | 169, 170 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
172 | 171 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
173 | 172 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
174 | 173 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
175 | 99, 167, 174 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
176 | 175 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
177 | 82 | simp2bi 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
178 | 81, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
179 | | divelunit 12314 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
180 | 84, 178, 80, 94, 179 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
181 | 180 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
182 | | simp112 1191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
183 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
184 | 182, 183,
51 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
185 | | simp113 1192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
186 | 185, 183,
55 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
187 | | simp12r 1175 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
188 | 187, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
189 | | simp12l 1174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
190 | 189, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
191 | | simp13 1093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
192 | | divcl 10691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
193 | 192 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
194 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
195 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
196 | 123, 194,
195 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
197 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
198 | 196, 197 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
199 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
200 | 194, 199 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
201 | 193, 198,
200 | adddid 10064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
202 | 201 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
203 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
204 | 123, 193,
203 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
205 | 204, 197 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
206 | 193, 198 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
207 | 193, 200 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
208 | 205, 206,
207 | addassd 10062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
209 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
210 | | subdi 10463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
|
211 | 123, 210 | mp3an2 1412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
212 | 192, 209,
211 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
213 | 192 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
214 | | divcan1 10694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
|
215 | 213, 214 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
216 | 212, 215 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
217 | 216 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
218 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
219 | | npncan 10302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
|
220 | 123, 219 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
|
221 | 192, 218,
220 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
|
222 | 217, 221 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
223 | 222 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
224 | 223 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
225 | 193, 196 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
226 | 204, 225,
197 | adddird 10065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
227 | 193, 196,
197 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
228 | 227 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
229 | 224, 226,
228 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
230 | 193, 194,
199 | mulassd 10063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
231 | 214 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
232 | 231 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
233 | 230, 232 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
234 | 229, 233 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
235 | 202, 208,
234 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
236 | 184, 186,
188, 190, 191, 235 | syl23anc 1333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
237 | 236 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
238 | 237 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
239 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
240 | 239 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
241 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
242 | 240, 241 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
243 | 242 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
244 | 243 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
245 | 244 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
246 | 181, 238,
245 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
247 | 246 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
248 | 176, 247 | orim12d 883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
249 | | r19.43 3093 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
250 | 248, 249 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
251 | 85, 250 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
252 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
253 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
254 | 253 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
255 | 252, 254 | eqeqan12d 2638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
256 | 255 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
257 | | ralbi 3068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
259 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
260 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
261 | 260 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
262 | 259, 261 | eqeqan12rd 2640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
263 | 262 | ralimi 2952 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
264 | | ralbi 3068 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
265 | 263, 264 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
266 | 258, 265 | orbi12d 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
267 | 266 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
268 | 251, 267 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
269 | 268 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
270 | 269 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
|
271 | 74, 270 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
|
272 | 271 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
|
273 | 71, 272 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
|
274 | 273 | ex 450 |
. . . . . . . . . . . . . . . . . 18
|
275 | 274 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . 17
|
276 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . . 20
|
277 | | brbtwn 25779 |
. . . . . . . . . . . . . . . . . . . 20
|
278 | 276, 73, 53, 277 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
279 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . 20
|
280 | | brbtwn 25779 |
. . . . . . . . . . . . . . . . . . . 20
|
281 | 279, 73, 53, 280 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
282 | 278, 281 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
|
283 | | r19.26 3064 |
. . . . . . . . . . . . . . . . . . . 20
|
284 | 283 | 2rexbii 3042 |
. . . . . . . . . . . . . . . . . . 19
|
285 | | reeanv 3107 |
. . . . . . . . . . . . . . . . . . 19
|
286 | 284, 285 | bitri 264 |
. . . . . . . . . . . . . . . . . 18
|
287 | 282, 286 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
|
288 | | brbtwn 25779 |
. . . . . . . . . . . . . . . . . . . 20
|
289 | 276, 73, 279, 288 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
290 | | brbtwn 25779 |
. . . . . . . . . . . . . . . . . . . 20
|
291 | 279, 73, 276, 290 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
292 | 289, 291 | orbi12d 746 |
. . . . . . . . . . . . . . . . . 18
|
293 | | r19.43 3093 |
. . . . . . . . . . . . . . . . . 18
|
294 | 292, 293 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
|
295 | 275, 287,
294 | 3imtr4d 283 |
. . . . . . . . . . . . . . . 16
|
296 | 295 | 3expia 1267 |
. . . . . . . . . . . . . . 15
|
297 | 296 | impd 447 |
. . . . . . . . . . . . . 14
|
298 | 31, 297 | sylanl2 683 |
. . . . . . . . . . . . 13
|
299 | 298 | 3adantr2 1221 |
. . . . . . . . . . . 12
|
300 | 299 | adantr 481 |
. . . . . . . . . . 11
|
301 | 30, 300 | mpd 15 |
. . . . . . . . . 10
|
302 | 301 | ralrimiva 2966 |
. . . . . . . . 9
|
303 | 302 | 3exp2 1285 |
. . . . . . . 8
|
304 | 11, 303 | syl6 35 |
. . . . . . 7
|
305 | 304 | exlimiv 1858 |
. . . . . 6
|
306 | 2, 305 | sylbi 207 |
. . . . 5
|
307 | 306 | com4l 92 |
. . . 4
|
308 | 307 | 3impd 1281 |
. . 3
|
309 | 308 | imp32 449 |
. 2
|
310 | | axcontlem4.1 |
. . . 4
|
311 | 310 | sseq2i 3630 |
. . 3
|
312 | | ssrab 3680 |
. . 3
|
313 | 311, 312 | bitri 264 |
. 2
|
314 | 1, 309, 313 | sylanbrc 698 |
1
|