Proof of Theorem tanarg
Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . 8
|
2 | | re0 13892 |
. . . . . . . 8
|
3 | 1, 2 | syl6eq 2672 |
. . . . . . 7
|
4 | 3 | necon3i 2826 |
. . . . . 6
|
5 | | logcl 24315 |
. . . . . 6
|
6 | 4, 5 | sylan2 491 |
. . . . 5
|
7 | 6 | imcld 13935 |
. . . 4
|
8 | 7 | recnd 10068 |
. . 3
|
9 | | sqcl 12925 |
. . . . . . 7
|
10 | 9 | adantr 481 |
. . . . . 6
|
11 | | abscl 14018 |
. . . . . . . . 9
|
12 | 11 | adantr 481 |
. . . . . . . 8
|
13 | 12 | recnd 10068 |
. . . . . . 7
|
14 | 13 | sqcld 13006 |
. . . . . 6
|
15 | | absrpcl 14028 |
. . . . . . . . 9
|
16 | 4, 15 | sylan2 491 |
. . . . . . . 8
|
17 | 16 | rpne0d 11877 |
. . . . . . 7
|
18 | | sqne0 12930 |
. . . . . . . 8
|
19 | 13, 18 | syl 17 |
. . . . . . 7
|
20 | 17, 19 | mpbird 247 |
. . . . . 6
|
21 | 10, 14, 14, 20 | divdird 10839 |
. . . . 5
|
22 | | ax-icn 9995 |
. . . . . . . . 9
|
23 | | mulcl 10020 |
. . . . . . . . 9
|
24 | 22, 8, 23 | sylancr 695 |
. . . . . . . 8
|
25 | | 2z 11409 |
. . . . . . . 8
|
26 | | efexp 14831 |
. . . . . . . 8
|
27 | 24, 25, 26 | sylancl 694 |
. . . . . . 7
|
28 | | efiarg 24353 |
. . . . . . . . 9
|
29 | 4, 28 | sylan2 491 |
. . . . . . . 8
|
30 | 29 | oveq1d 6665 |
. . . . . . 7
|
31 | | simpl 473 |
. . . . . . . 8
|
32 | 31, 13, 17 | sqdivd 13021 |
. . . . . . 7
|
33 | 27, 30, 32 | 3eqtrrd 2661 |
. . . . . 6
|
34 | 14, 20 | dividd 10799 |
. . . . . 6
|
35 | 33, 34 | oveq12d 6668 |
. . . . 5
|
36 | 21, 35 | eqtr2d 2657 |
. . . 4
|
37 | 10, 14 | addcld 10059 |
. . . . 5
|
38 | 22 | a1i 11 |
. . . . . . . . . 10
|
39 | | 2cn 11091 |
. . . . . . . . . . 11
|
40 | | recl 13850 |
. . . . . . . . . . . . . 14
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . 13
|
42 | 41 | recnd 10068 |
. . . . . . . . . . . 12
|
43 | 42 | sqcld 13006 |
. . . . . . . . . . 11
|
44 | | mulcl 10020 |
. . . . . . . . . . 11
|
45 | 39, 43, 44 | sylancr 695 |
. . . . . . . . . 10
|
46 | 39 | a1i 11 |
. . . . . . . . . . . . 13
|
47 | | imcl 13851 |
. . . . . . . . . . . . . . . 16
|
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . 15
|
49 | 48 | recnd 10068 |
. . . . . . . . . . . . . 14
|
50 | 42, 49 | mulcld 10060 |
. . . . . . . . . . . . 13
|
51 | 38, 46, 50 | mul12d 10245 |
. . . . . . . . . . . 12
|
52 | 38, 42, 49 | mul12d 10245 |
. . . . . . . . . . . . 13
|
53 | 52 | oveq2d 6666 |
. . . . . . . . . . . 12
|
54 | 51, 53 | eqtrd 2656 |
. . . . . . . . . . 11
|
55 | | mulcl 10020 |
. . . . . . . . . . . . . 14
|
56 | 22, 49, 55 | sylancr 695 |
. . . . . . . . . . . . 13
|
57 | 42, 56 | mulcld 10060 |
. . . . . . . . . . . 12
|
58 | | mulcl 10020 |
. . . . . . . . . . . 12
|
59 | 39, 57, 58 | sylancr 695 |
. . . . . . . . . . 11
|
60 | 54, 59 | eqeltrd 2701 |
. . . . . . . . . 10
|
61 | 38, 45, 60 | adddid 10064 |
. . . . . . . . 9
|
62 | | mulcl 10020 |
. . . . . . . . . . . . 13
|
63 | 42, 22, 62 | sylancl 694 |
. . . . . . . . . . . 12
|
64 | 46, 63, 42 | mulassd 10063 |
. . . . . . . . . . 11
|
65 | 42 | sqvald 13005 |
. . . . . . . . . . . . . 14
|
66 | 65 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
67 | | mulcom 10022 |
. . . . . . . . . . . . . 14
|
68 | 43, 22, 67 | sylancl 694 |
. . . . . . . . . . . . 13
|
69 | 42, 42, 38 | mul32d 10246 |
. . . . . . . . . . . . 13
|
70 | 66, 68, 69 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
|
71 | 70 | oveq2d 6666 |
. . . . . . . . . . 11
|
72 | 46, 38, 43 | mul12d 10245 |
. . . . . . . . . . 11
|
73 | 64, 71, 72 | 3eqtr2d 2662 |
. . . . . . . . . 10
|
74 | | ixi 10656 |
. . . . . . . . . . . . 13
|
75 | 74 | oveq1i 6660 |
. . . . . . . . . . . 12
|
76 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
|
77 | 39, 49, 76 | sylancr 695 |
. . . . . . . . . . . . . 14
|
78 | 77, 42 | mulcld 10060 |
. . . . . . . . . . . . 13
|
79 | 38, 38, 78 | mulassd 10063 |
. . . . . . . . . . . 12
|
80 | 75, 79 | syl5eqr 2670 |
. . . . . . . . . . 11
|
81 | 78 | mulm1d 10482 |
. . . . . . . . . . 11
|
82 | 46, 49, 42 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
83 | 49, 42 | mulcomd 10061 |
. . . . . . . . . . . . . . 15
|
84 | 83 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
85 | 82, 84 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . 12
|
87 | 86 | oveq2d 6666 |
. . . . . . . . . . 11
|
88 | 80, 81, 87 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
89 | 73, 88 | oveq12d 6668 |
. . . . . . . . 9
|
90 | | mulcl 10020 |
. . . . . . . . . . . 12
|
91 | 39, 63, 90 | sylancr 695 |
. . . . . . . . . . 11
|
92 | 91, 42 | mulcld 10060 |
. . . . . . . . . 10
|
93 | 92, 78 | negsubd 10398 |
. . . . . . . . 9
|
94 | 61, 89, 93 | 3eqtr2d 2662 |
. . . . . . . 8
|
95 | 49 | sqcld 13006 |
. . . . . . . . . . . 12
|
96 | 59, 95 | subcld 10392 |
. . . . . . . . . . 11
|
97 | 43, 96, 43, 95 | add4d 10264 |
. . . . . . . . . 10
|
98 | | replim 13856 |
. . . . . . . . . . . . . 14
|
99 | 98 | adantr 481 |
. . . . . . . . . . . . 13
|
100 | 99 | oveq1d 6665 |
. . . . . . . . . . . 12
|
101 | | binom2 12979 |
. . . . . . . . . . . . . 14
|
102 | 42, 56, 101 | syl2anc 693 |
. . . . . . . . . . . . 13
|
103 | | sqmul 12926 |
. . . . . . . . . . . . . . . . 17
|
104 | 22, 49, 103 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
105 | | i2 12965 |
. . . . . . . . . . . . . . . . 17
|
106 | 105 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
107 | 104, 106 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
108 | 95 | mulm1d 10482 |
. . . . . . . . . . . . . . 15
|
109 | 107, 108 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
111 | 43, 59 | addcld 10059 |
. . . . . . . . . . . . . 14
|
112 | 111, 95 | negsubd 10398 |
. . . . . . . . . . . . 13
|
113 | 102, 110,
112 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
114 | 43, 59, 95 | addsubassd 10412 |
. . . . . . . . . . . 12
|
115 | 100, 113,
114 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
116 | | absvalsq2 14021 |
. . . . . . . . . . . 12
|
117 | 116 | adantr 481 |
. . . . . . . . . . 11
|
118 | 115, 117 | oveq12d 6668 |
. . . . . . . . . 10
|
119 | 43 | 2timesd 11275 |
. . . . . . . . . . 11
|
120 | 59, 95 | npcand 10396 |
. . . . . . . . . . . 12
|
121 | 53, 51, 120 | 3eqtr4d 2666 |
. . . . . . . . . . 11
|
122 | 119, 121 | oveq12d 6668 |
. . . . . . . . . 10
|
123 | 97, 118, 122 | 3eqtr4d 2666 |
. . . . . . . . 9
|
124 | 123 | oveq2d 6666 |
. . . . . . . 8
|
125 | 91, 77, 42 | subdird 10487 |
. . . . . . . 8
|
126 | 94, 124, 125 | 3eqtr4d 2666 |
. . . . . . 7
|
127 | 91, 77 | subcld 10392 |
. . . . . . . 8
|
128 | | mulcom 10022 |
. . . . . . . . . . 11
|
129 | 42, 22, 128 | sylancl 694 |
. . . . . . . . . 10
|
130 | | simpr 477 |
. . . . . . . . . . 11
|
131 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
132 | 48, 131 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
|
133 | | rimul 11011 |
. . . . . . . . . . . . 13
|
134 | 41, 132, 133 | syl6an 568 |
. . . . . . . . . . . 12
|
135 | 134 | necon3d 2815 |
. . . . . . . . . . 11
|
136 | 130, 135 | mpd 15 |
. . . . . . . . . 10
|
137 | 129, 136 | eqnetrd 2861 |
. . . . . . . . 9
|
138 | 91, 77 | subeq0ad 10402 |
. . . . . . . . . . 11
|
139 | | 2ne0 11113 |
. . . . . . . . . . . . 13
|
140 | 139 | a1i 11 |
. . . . . . . . . . . 12
|
141 | 63, 49, 46, 140 | mulcand 10660 |
. . . . . . . . . . 11
|
142 | 138, 141 | bitrd 268 |
. . . . . . . . . 10
|
143 | 142 | necon3bid 2838 |
. . . . . . . . 9
|
144 | 137, 143 | mpbird 247 |
. . . . . . . 8
|
145 | 127, 42, 144, 130 | mulne0d 10679 |
. . . . . . 7
|
146 | 126, 145 | eqnetrd 2861 |
. . . . . 6
|
147 | | oveq2 6658 |
. . . . . . . 8
|
148 | | it0e0 11254 |
. . . . . . . 8
|
149 | 147, 148 | syl6eq 2672 |
. . . . . . 7
|
150 | 149 | necon3i 2826 |
. . . . . 6
|
151 | 146, 150 | syl 17 |
. . . . 5
|
152 | 37, 14, 151, 20 | divne0d 10817 |
. . . 4
|
153 | 36, 152 | eqnetrd 2861 |
. . 3
|
154 | | tanval3 14864 |
. . 3
|
155 | 8, 153, 154 | syl2anc 693 |
. 2
|
156 | 10, 14, 14, 20 | divsubdird 10840 |
. . . 4
|
157 | 33, 34 | oveq12d 6668 |
. . . 4
|
158 | 156, 157 | eqtr2d 2657 |
. . 3
|
159 | 36 | oveq2d 6666 |
. . . 4
|
160 | 38, 37, 14, 20 | divassd 10836 |
. . . 4
|
161 | 159, 160 | eqtr4d 2659 |
. . 3
|
162 | 158, 161 | oveq12d 6668 |
. 2
|
163 | 10, 14 | subcld 10392 |
. . . 4
|
164 | | mulcl 10020 |
. . . . 5
|
165 | 22, 37, 164 | sylancr 695 |
. . . 4
|
166 | 163, 165,
14, 146, 20 | divcan7d 10829 |
. . 3
|
167 | 115, 117 | oveq12d 6668 |
. . . . 5
|
168 | 43, 96, 95 | pnpcand 10429 |
. . . . 5
|
169 | 59, 95, 95 | subsub4d 10423 |
. . . . . 6
|
170 | 95 | 2timesd 11275 |
. . . . . . 7
|
171 | 170 | oveq2d 6666 |
. . . . . 6
|
172 | 46, 63, 49 | mulassd 10063 |
. . . . . . . . 9
|
173 | 42, 38, 49 | mulassd 10063 |
. . . . . . . . . 10
|
174 | 173 | oveq2d 6666 |
. . . . . . . . 9
|
175 | 172, 174 | eqtr2d 2657 |
. . . . . . . 8
|
176 | 49 | sqvald 13005 |
. . . . . . . . . 10
|
177 | 176 | oveq2d 6666 |
. . . . . . . . 9
|
178 | 46, 49, 49 | mulassd 10063 |
. . . . . . . . 9
|
179 | 177, 178 | eqtr4d 2659 |
. . . . . . . 8
|
180 | 175, 179 | oveq12d 6668 |
. . . . . . 7
|
181 | 91, 77, 49 | subdird 10487 |
. . . . . . 7
|
182 | 180, 181 | eqtr4d 2659 |
. . . . . 6
|
183 | 169, 171,
182 | 3eqtr2d 2662 |
. . . . 5
|
184 | 167, 168,
183 | 3eqtrd 2660 |
. . . 4
|
185 | 184, 126 | oveq12d 6668 |
. . 3
|
186 | 49, 42, 127, 130, 144 | divcan5d 10827 |
. . 3
|
187 | 166, 185,
186 | 3eqtrd 2660 |
. 2
|
188 | 155, 162,
187 | 3eqtrd 2660 |
1
|