Proof of Theorem pjhthlem1
Step | Hyp | Ref
| Expression |
1 | | pjhth.2 |
. . . 4
|
2 | | pjhth.3 |
. . . . 5
|
3 | | pjhth.1 |
. . . . . 6
|
4 | 3 | cheli 28089 |
. . . . 5
|
5 | 2, 4 | syl 17 |
. . . 4
|
6 | | hvsubcl 27874 |
. . . 4
|
7 | 1, 5, 6 | syl2anc 693 |
. . 3
|
8 | | pjhth.4 |
. . . 4
|
9 | 3 | cheli 28089 |
. . . 4
|
10 | 8, 9 | syl 17 |
. . 3
|
11 | | hicl 27937 |
. . 3
|
12 | 7, 10, 11 | syl2anc 693 |
. 2
|
13 | 12 | abscld 14175 |
. . . 4
|
14 | 13 | recnd 10068 |
. . 3
|
15 | 13 | resqcld 13035 |
. . . . . . 7
|
16 | 15 | renegcld 10457 |
. . . . . 6
|
17 | | hiidrcl 27952 |
. . . . . . . 8
|
18 | 10, 17 | syl 17 |
. . . . . . 7
|
19 | | 2re 11090 |
. . . . . . 7
|
20 | | readdcl 10019 |
. . . . . . 7
|
21 | 18, 19, 20 | sylancl 694 |
. . . . . 6
|
22 | | 0red 10041 |
. . . . . . 7
|
23 | | peano2re 10209 |
. . . . . . . 8
|
24 | 18, 23 | syl 17 |
. . . . . . 7
|
25 | | hiidge0 27955 |
. . . . . . . . 9
|
26 | 10, 25 | syl 17 |
. . . . . . . 8
|
27 | 18 | ltp1d 10954 |
. . . . . . . 8
|
28 | 22, 18, 24, 26, 27 | lelttrd 10195 |
. . . . . . 7
|
29 | 24 | ltp1d 10954 |
. . . . . . . 8
|
30 | 18 | recnd 10068 |
. . . . . . . . . 10
|
31 | | ax-1cn 9994 |
. . . . . . . . . . 11
|
32 | | addass 10023 |
. . . . . . . . . . 11
|
33 | 31, 31, 32 | mp3an23 1416 |
. . . . . . . . . 10
|
34 | 30, 33 | syl 17 |
. . . . . . . . 9
|
35 | | df-2 11079 |
. . . . . . . . . 10
|
36 | 35 | oveq2i 6661 |
. . . . . . . . 9
|
37 | 34, 36 | syl6reqr 2675 |
. . . . . . . 8
|
38 | 29, 37 | breqtrrd 4681 |
. . . . . . 7
|
39 | 22, 24, 21, 28, 38 | lttrd 10198 |
. . . . . 6
|
40 | 3 | chshii 28084 |
. . . . . . . . . . . . . . 15
|
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
|
42 | | pjhth.6 |
. . . . . . . . . . . . . . . 16
|
43 | 24 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
44 | 18, 26 | ge0p1rpd 11902 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | rpne0d 11877 |
. . . . . . . . . . . . . . . . 17
|
46 | 12, 43, 45 | divcld 10801 |
. . . . . . . . . . . . . . . 16
|
47 | 42, 46 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
|
48 | | shmulcl 28075 |
. . . . . . . . . . . . . . 15
|
49 | 41, 47, 8, 48 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
50 | | shaddcl 28074 |
. . . . . . . . . . . . . 14
|
51 | 41, 2, 49, 50 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
52 | | pjhth.5 |
. . . . . . . . . . . . 13
|
53 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
55 | 54 | breq2d 4665 |
. . . . . . . . . . . . . 14
|
56 | 55 | rspcv 3305 |
. . . . . . . . . . . . 13
|
57 | 51, 52, 56 | sylc 65 |
. . . . . . . . . . . 12
|
58 | 3 | cheli 28089 |
. . . . . . . . . . . . . . 15
|
59 | 49, 58 | syl 17 |
. . . . . . . . . . . . . 14
|
60 | | hvsubass 27901 |
. . . . . . . . . . . . . 14
|
61 | 1, 5, 59, 60 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
62 | 61 | fveq2d 6195 |
. . . . . . . . . . . 12
|
63 | 57, 62 | breqtrrd 4681 |
. . . . . . . . . . 11
|
64 | | normcl 27982 |
. . . . . . . . . . . . 13
|
65 | 7, 64 | syl 17 |
. . . . . . . . . . . 12
|
66 | | hvsubcl 27874 |
. . . . . . . . . . . . . 14
|
67 | 7, 59, 66 | syl2anc 693 |
. . . . . . . . . . . . 13
|
68 | | normcl 27982 |
. . . . . . . . . . . . 13
|
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
|
70 | | normge0 27983 |
. . . . . . . . . . . . 13
|
71 | 7, 70 | syl 17 |
. . . . . . . . . . . 12
|
72 | 22, 65, 69, 71, 63 | letrd 10194 |
. . . . . . . . . . . 12
|
73 | 65, 69, 71, 72 | le2sqd 13044 |
. . . . . . . . . . 11
|
74 | 63, 73 | mpbid 222 |
. . . . . . . . . 10
|
75 | 69 | resqcld 13035 |
. . . . . . . . . . 11
|
76 | 65 | resqcld 13035 |
. . . . . . . . . . 11
|
77 | 75, 76 | subge0d 10617 |
. . . . . . . . . 10
|
78 | 74, 77 | mpbird 247 |
. . . . . . . . 9
|
79 | | 2z 11409 |
. . . . . . . . . . . . . . . 16
|
80 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . 16
|
81 | 44, 79, 80 | sylancl 694 |
. . . . . . . . . . . . . . 15
|
82 | 15, 81 | rerpdivcld 11903 |
. . . . . . . . . . . . . 14
|
83 | 82, 21 | remulcld 10070 |
. . . . . . . . . . . . 13
|
84 | 83 | recnd 10068 |
. . . . . . . . . . . 12
|
85 | 84 | negcld 10379 |
. . . . . . . . . . 11
|
86 | | hicl 27937 |
. . . . . . . . . . . 12
|
87 | 7, 7, 86 | syl2anc 693 |
. . . . . . . . . . 11
|
88 | 85, 87 | pncand 10393 |
. . . . . . . . . 10
|
89 | | normsq 27991 |
. . . . . . . . . . . . . 14
|
90 | 67, 89 | syl 17 |
. . . . . . . . . . . . 13
|
91 | | his2sub 27949 |
. . . . . . . . . . . . . 14
|
92 | 7, 59, 67, 91 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
93 | | his2sub2 27950 |
. . . . . . . . . . . . . . . 16
|
94 | 7, 7, 59, 93 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
|
95 | 94 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
96 | | hicl 27937 |
. . . . . . . . . . . . . . . 16
|
97 | 7, 59, 96 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
98 | | his2sub2 27950 |
. . . . . . . . . . . . . . . . 17
|
99 | 59, 7, 59, 98 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
100 | | hicl 27937 |
. . . . . . . . . . . . . . . . . 18
|
101 | 59, 7, 100 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
102 | | hicl 27937 |
. . . . . . . . . . . . . . . . . 18
|
103 | 59, 59, 102 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
104 | 101, 103 | subcld 10392 |
. . . . . . . . . . . . . . . 16
|
105 | 99, 104 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
106 | 87, 97, 105 | subsub4d 10423 |
. . . . . . . . . . . . . 14
|
107 | 82 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
108 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
109 | 107, 43, 108 | adddid 10064 |
. . . . . . . . . . . . . . . 16
|
110 | 37 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
111 | | his5 27943 |
. . . . . . . . . . . . . . . . . . . 20
|
112 | 47, 7, 10, 111 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
|
113 | 47 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . . 20
|
114 | 113, 12 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . 19
|
115 | 12 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . . . 21
|
116 | 12, 115, 43, 45 | divassd 10836 |
. . . . . . . . . . . . . . . . . . . 20
|
117 | 12 | absvalsqd 14181 |
. . . . . . . . . . . . . . . . . . . . 21
|
118 | 117 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
119 | 42 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
|
120 | 12, 43, 45 | cjdivd 13963 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
121 | 24 | cjred 13966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
122 | 121 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
123 | 120, 122 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
124 | 119, 123 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . 21
|
125 | 124 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
|
126 | 116, 118,
125 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . . . . . 19
|
127 | 112, 114,
126 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
|
128 | 15 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . 21
|
129 | 128, 43 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . . . 20
|
130 | 43 | sqvald 13005 |
. . . . . . . . . . . . . . . . . . . 20
|
131 | 129, 130 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
132 | 128, 43, 43, 45, 45 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . 19
|
133 | 131, 132 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
|
134 | 24 | resqcld 13035 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 134 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
|
136 | 81 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . . 19
|
137 | 128, 43, 135, 136 | div23d 10838 |
. . . . . . . . . . . . . . . . . 18
|
138 | 127, 133,
137 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
|
139 | 82, 24 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . . . 22
|
140 | 138, 139 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
|
141 | | hire 27951 |
. . . . . . . . . . . . . . . . . . . . . 22
|
142 | 7, 59, 141 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
|
143 | 140, 142 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
|
144 | 143, 138 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . 19
|
145 | | his35 27945 |
. . . . . . . . . . . . . . . . . . . . 21
|
146 | 47, 47, 10, 10, 145 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . 20
|
147 | 42 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
148 | 12, 43, 45 | absdivd 14194 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
149 | 44 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
150 | 24, 149 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
151 | 150 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
152 | 148, 151 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
153 | 147, 152 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
154 | 153 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
155 | 47 | absvalsqd 14181 |
. . . . . . . . . . . . . . . . . . . . . 22
|
156 | 14, 43, 45 | sqdivd 13021 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | 154, 155,
156 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . . . . . . 21
|
158 | 157 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . 20
|
159 | 146, 158 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
160 | 144, 159 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
161 | | pncan2 10288 |
. . . . . . . . . . . . . . . . . . . . 21
|
162 | 30, 31, 161 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . 20
|
163 | 162 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
164 | 107, 43, 30 | subdid 10486 |
. . . . . . . . . . . . . . . . . . 19
|
165 | 163, 164 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . 18
|
166 | 160, 99, 165 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
|
167 | 138, 166 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
168 | 109, 110,
167 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . 15
|
169 | 168 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
170 | 95, 106, 169 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
|
171 | 90, 92, 170 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
172 | 87, 84 | negsubd 10398 |
. . . . . . . . . . . 12
|
173 | 87, 85 | addcomd 10238 |
. . . . . . . . . . . 12
|
174 | 171, 172,
173 | 3eqtr2d 2662 |
. . . . . . . . . . 11
|
175 | | normsq 27991 |
. . . . . . . . . . . 12
|
176 | 7, 175 | syl 17 |
. . . . . . . . . . 11
|
177 | 174, 176 | oveq12d 6668 |
. . . . . . . . . 10
|
178 | 21 | renegcld 10457 |
. . . . . . . . . . . . 13
|
179 | 178 | recnd 10068 |
. . . . . . . . . . . 12
|
180 | 128, 179,
135, 136 | div23d 10838 |
. . . . . . . . . . 11
|
181 | 21 | recnd 10068 |
. . . . . . . . . . . 12
|
182 | 107, 181 | mulneg2d 10484 |
. . . . . . . . . . 11
|
183 | 180, 182 | eqtrd 2656 |
. . . . . . . . . 10
|
184 | 88, 177, 183 | 3eqtr4rd 2667 |
. . . . . . . . 9
|
185 | 78, 184 | breqtrrd 4681 |
. . . . . . . 8
|
186 | 15, 178 | remulcld 10070 |
. . . . . . . . 9
|
187 | 186, 81 | ge0divd 11910 |
. . . . . . . 8
|
188 | 185, 187 | mpbird 247 |
. . . . . . 7
|
189 | | mulneg12 10468 |
. . . . . . . 8
|
190 | 128, 181,
189 | syl2anc 693 |
. . . . . . 7
|
191 | 188, 190 | breqtrrd 4681 |
. . . . . 6
|
192 | | prodge02 10871 |
. . . . . 6
|
193 | 16, 21, 39, 191, 192 | syl22anc 1327 |
. . . . 5
|
194 | 15 | le0neg1d 10599 |
. . . . 5
|
195 | 193, 194 | mpbird 247 |
. . . 4
|
196 | 13 | sqge0d 13036 |
. . . 4
|
197 | | 0re 10040 |
. . . . 5
|
198 | | letri3 10123 |
. . . . 5
|
199 | 15, 197, 198 | sylancl 694 |
. . . 4
|
200 | 195, 196,
199 | mpbir2and 957 |
. . 3
|
201 | 14, 200 | sqeq0d 13007 |
. 2
|
202 | 12, 201 | abs00d 14185 |
1
|