Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  pjhthlem1 Structured version   Unicode version

Theorem pjhthlem1 26981
 Description: Lemma for pjhth 26983. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
pjhth.1
pjhth.2
pjhth.3
pjhth.4
pjhth.5
pjhth.6
Assertion
Ref Expression
pjhthlem1
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem pjhthlem1
StepHypRef Expression
1 pjhth.2 . . . 4
2 pjhth.3 . . . . 5
3 pjhth.1 . . . . . 6
43cheli 26822 . . . . 5
52, 4syl 17 . . . 4
6 hvsubcl 26607 . . . 4
71, 5, 6syl2anc 665 . . 3
8 pjhth.4 . . . 4
93cheli 26822 . . . 4
108, 9syl 17 . . 3
11 hicl 26670 . . 3
127, 10, 11syl2anc 665 . 2
1312abscld 13436 . . . 4
1413recnd 9615 . . 3
1513resqcld 12387 . . . . . . 7
1615renegcld 9992 . . . . . 6
17 hiidrcl 26685 . . . . . . . 8
1810, 17syl 17 . . . . . . 7
19 2re 10625 . . . . . . 7
20 readdcl 9568 . . . . . . 7
2118, 19, 20sylancl 666 . . . . . 6
22 0red 9590 . . . . . . 7
23 peano2re 9752 . . . . . . . 8
2418, 23syl 17 . . . . . . 7
25 hiidge0 26688 . . . . . . . . 9
2610, 25syl 17 . . . . . . . 8
2718ltp1d 10483 . . . . . . . 8
2822, 18, 24, 26, 27lelttrd 9739 . . . . . . 7
2924ltp1d 10483 . . . . . . . 8
3018recnd 9615 . . . . . . . . . 10
31 ax-1cn 9543 . . . . . . . . . . 11
32 addass 9572 . . . . . . . . . . 11
3331, 31, 32mp3an23 1352 . . . . . . . . . 10
3430, 33syl 17 . . . . . . . . 9
35 df-2 10614 . . . . . . . . . 10
3635oveq2i 6255 . . . . . . . . 9
3734, 36syl6reqr 2476 . . . . . . . 8
3829, 37breqtrrd 4388 . . . . . . 7
3922, 24, 21, 28, 38lttrd 9742 . . . . . 6
403chshii 26817 . . . . . . . . . . . . . . 15
4140a1i 11 . . . . . . . . . . . . . 14
42 pjhth.6 . . . . . . . . . . . . . . . 16
4324recnd 9615 . . . . . . . . . . . . . . . . 17
4418, 26ge0p1rpd 11314 . . . . . . . . . . . . . . . . . 18
4544rpne0d 11292 . . . . . . . . . . . . . . . . 17
4612, 43, 45divcld 10329 . . . . . . . . . . . . . . . 16
4742, 46syl5eqel 2505 . . . . . . . . . . . . . . 15
48 shmulcl 26808 . . . . . . . . . . . . . . 15
4941, 47, 8, 48syl3anc 1264 . . . . . . . . . . . . . 14
50 shaddcl 26807 . . . . . . . . . . . . . 14
5141, 2, 49, 50syl3anc 1264 . . . . . . . . . . . . 13
52 pjhth.5 . . . . . . . . . . . . 13
53 oveq2 6252 . . . . . . . . . . . . . . . 16
5453fveq2d 5824 . . . . . . . . . . . . . . 15
5554breq2d 4373 . . . . . . . . . . . . . 14
5655rspcv 3116 . . . . . . . . . . . . 13
5751, 52, 56sylc 62 . . . . . . . . . . . 12
583cheli 26822 . . . . . . . . . . . . . . 15
5949, 58syl 17 . . . . . . . . . . . . . 14
60 hvsubass 26634 . . . . . . . . . . . . . 14
611, 5, 59, 60syl3anc 1264 . . . . . . . . . . . . 13
6261fveq2d 5824 . . . . . . . . . . . 12
6357, 62breqtrrd 4388 . . . . . . . . . . 11
64 normcl 26715 . . . . . . . . . . . . 13
657, 64syl 17 . . . . . . . . . . . 12
66 hvsubcl 26607 . . . . . . . . . . . . . 14
677, 59, 66syl2anc 665 . . . . . . . . . . . . 13
68 normcl 26715 . . . . . . . . . . . . 13
6967, 68syl 17 . . . . . . . . . . . 12
70 normge0 26716 . . . . . . . . . . . . 13
717, 70syl 17 . . . . . . . . . . . 12
7222, 65, 69, 71, 63letrd 9738 . . . . . . . . . . . 12
7365, 69, 71, 72le2sqd 12396 . . . . . . . . . . 11
7463, 73mpbid 213 . . . . . . . . . 10
7569resqcld 12387 . . . . . . . . . . 11
7665resqcld 12387 . . . . . . . . . . 11
7775, 76subge0d 10149 . . . . . . . . . 10
7874, 77mpbird 235 . . . . . . . . 9
79 2z 10915 . . . . . . . . . . . . . . . 16
80 rpexpcl 12236 . . . . . . . . . . . . . . . 16
8144, 79, 80sylancl 666 . . . . . . . . . . . . . . 15
8215, 81rerpdivcld 11315 . . . . . . . . . . . . . 14
8382, 21remulcld 9617 . . . . . . . . . . . . 13
8483recnd 9615 . . . . . . . . . . . 12
8584negcld 9919 . . . . . . . . . . 11
86 hicl 26670 . . . . . . . . . . . 12
877, 7, 86syl2anc 665 . . . . . . . . . . 11
8885, 87pncand 9933 . . . . . . . . . 10
89 normsq 26724 . . . . . . . . . . . . . 14
9067, 89syl 17 . . . . . . . . . . . . 13
91 his2sub 26682 . . . . . . . . . . . . . 14
927, 59, 67, 91syl3anc 1264 . . . . . . . . . . . . 13
93 his2sub2 26683 . . . . . . . . . . . . . . . 16
947, 7, 59, 93syl3anc 1264 . . . . . . . . . . . . . . 15
9594oveq1d 6259 . . . . . . . . . . . . . 14
96 hicl 26670 . . . . . . . . . . . . . . . 16
977, 59, 96syl2anc 665 . . . . . . . . . . . . . . 15
98 his2sub2 26683 . . . . . . . . . . . . . . . . 17
9959, 7, 59, 98syl3anc 1264 . . . . . . . . . . . . . . . 16
100 hicl 26670 . . . . . . . . . . . . . . . . . 18
10159, 7, 100syl2anc 665 . . . . . . . . . . . . . . . . 17
102 hicl 26670 . . . . . . . . . . . . . . . . . 18
10359, 59, 102syl2anc 665 . . . . . . . . . . . . . . . . 17
104101, 103subcld 9932 . . . . . . . . . . . . . . . 16
10599, 104eqeltrd 2501 . . . . . . . . . . . . . . 15
10687, 97, 105subsub4d 9963 . . . . . . . . . . . . . 14
10782recnd 9615 . . . . . . . . . . . . . . . . 17
10831a1i 11 . . . . . . . . . . . . . . . . 17
109107, 43, 108adddid 9613 . . . . . . . . . . . . . . . 16
11037oveq2d 6260 . . . . . . . . . . . . . . . 16
111 his5 26676 . . . . . . . . . . . . . . . . . . . 20
11247, 7, 10, 111syl3anc 1264 . . . . . . . . . . . . . . . . . . 19
11347cjcld 13198 . . . . . . . . . . . . . . . . . . . 20
114113, 12mulcomd 9610 . . . . . . . . . . . . . . . . . . 19
11512cjcld 13198 . . . . . . . . . . . . . . . . . . . . 21
11612, 115, 43, 45divassd 10364 . . . . . . . . . . . . . . . . . . . 20
11712absvalsqd 13442 . . . . . . . . . . . . . . . . . . . . 21
118117oveq1d 6259 . . . . . . . . . . . . . . . . . . . 20
11942fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . 22
12012, 43, 45cjdivd 13225 . . . . . . . . . . . . . . . . . . . . . . 23
12124cjred 13228 . . . . . . . . . . . . . . . . . . . . . . . 24
122121oveq2d 6260 . . . . . . . . . . . . . . . . . . . . . . 23
123120, 122eqtrd 2457 . . . . . . . . . . . . . . . . . . . . . 22
124119, 123syl5eq 2469 . . . . . . . . . . . . . . . . . . . . 21
125124oveq2d 6260 . . . . . . . . . . . . . . . . . . . 20
126116, 118, 1253eqtr4rd 2468 . . . . . . . . . . . . . . . . . . 19
127112, 114, 1263eqtrd 2461 . . . . . . . . . . . . . . . . . 18
12815recnd 9615 . . . . . . . . . . . . . . . . . . . . 21
129128, 43mulcomd 9610 . . . . . . . . . . . . . . . . . . . 20
13043sqvald 12358 . . . . . . . . . . . . . . . . . . . 20
131129, 130oveq12d 6262 . . . . . . . . . . . . . . . . . . 19
132128, 43, 43, 45, 45divcan5d 10355 . . . . . . . . . . . . . . . . . . 19
133131, 132eqtr2d 2458 . . . . . . . . . . . . . . . . . 18
13424resqcld 12387 . . . . . . . . . . . . . . . . . . . 20
135134recnd 9615 . . . . . . . . . . . . . . . . . . 19
13681rpne0d 11292 . . . . . . . . . . . . . . . . . . 19
137128, 43, 135, 136div23d 10366 . . . . . . . . . . . . . . . . . 18
138127, 133, 1373eqtrd 2461 . . . . . . . . . . . . . . . . 17
13982, 24remulcld 9617 . . . . . . . . . . . . . . . . . . . . . 22
140138, 139eqeltrd 2501 . . . . . . . . . . . . . . . . . . . . 21
141 hire 26684 . . . . . . . . . . . . . . . . . . . . . 22
1427, 59, 141syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21
143140, 142mpbid 213 . . . . . . . . . . . . . . . . . . . 20
144143, 138eqtr3d 2459 . . . . . . . . . . . . . . . . . . 19
145 his35 26678 . . . . . . . . . . . . . . . . . . . . 21
14647, 47, 10, 10, 145syl22anc 1265 . . . . . . . . . . . . . . . . . . . 20
14742fveq2i 5823 . . . . . . . . . . . . . . . . . . . . . . . 24
14812, 43, 45absdivd 13455 . . . . . . . . . . . . . . . . . . . . . . . . 25
14944rpge0d 11291 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15024, 149absidd 13423 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151150oveq2d 6260 . . . . . . . . . . . . . . . . . . . . . . . . 25
152148, 151eqtrd 2457 . . . . . . . . . . . . . . . . . . . . . . . 24
153147, 152syl5eq 2469 . . . . . . . . . . . . . . . . . . . . . . 23
154153oveq1d 6259 . . . . . . . . . . . . . . . . . . . . . 22
15547absvalsqd 13442 . . . . . . . . . . . . . . . . . . . . . 22
15614, 43, 45sqdivd 12374 . . . . . . . . . . . . . . . . . . . . . 22
157154, 155, 1563eqtr3d 2465 . . . . . . . . . . . . . . . . . . . . 21
158157oveq1d 6259 . . . . . . . . . . . . . . . . . . . 20
159146, 158eqtrd 2457 . . . . . . . . . . . . . . . . . . 19
160144, 159oveq12d 6262 . . . . . . . . . . . . . . . . . 18
161 pncan2 9828 . . . . . . . . . . . . . . . . . . . . 21
16230, 31, 161sylancl 666 . . . . . . . . . . . . . . . . . . . 20
163162oveq2d 6260 . . . . . . . . . . . . . . . . . . 19
164107, 43, 30subdid 10020 . . . . . . . . . . . . . . . . . . 19
165163, 164eqtr3d 2459 . . . . . . . . . . . . . . . . . 18
166160, 99, 1653eqtr4d 2467 . . . . . . . . . . . . . . . . 17
167138, 166oveq12d 6262 . . . . . . . . . . . . . . . 16
168109, 110, 1673eqtr4rd 2468 . . . . . . . . . . . . . . 15
169168oveq2d 6260 . . . . . . . . . . . . . 14
17095, 106, 1693eqtrd 2461 . . . . . . . . . . . . 13
17190, 92, 1703eqtrd 2461 . . . . . . . . . . . 12
17287, 84negsubd 9938 . . . . . . . . . . . 12
17387, 85addcomd 9781 . . . . . . . . . . . 12
174171, 172, 1733eqtr2d 2463 . . . . . . . . . . 11
175 normsq 26724 . . . . . . . . . . . 12
1767, 175syl 17 . . . . . . . . . . 11
177174, 176oveq12d 6262 . . . . . . . . . 10
17821renegcld 9992 . . . . . . . . . . . . 13
179178recnd 9615 . . . . . . . . . . . 12
180128, 179, 135, 136div23d 10366 . . . . . . . . . . 11
18121recnd 9615 . . . . . . . . . . . 12
182107, 181mulneg2d 10018 . . . . . . . . . . 11
183180, 182eqtrd 2457 . . . . . . . . . 10
18488, 177, 1833eqtr4rd 2468 . . . . . . . . 9
18578, 184breqtrrd 4388 . . . . . . . 8
18615, 178remulcld 9617 . . . . . . . . 9
187186, 81ge0divd 11322 . . . . . . . 8
188185, 187mpbird 235 . . . . . . 7
189 mulneg12 10003 . . . . . . . 8
190128, 181, 189syl2anc 665 . . . . . . 7
191188, 190breqtrrd 4388 . . . . . 6
192 prodge02 10399 . . . . . 6
19316, 21, 39, 191, 192syl22anc 1265 . . . . 5
19415le0neg1d 10131 . . . . 5
195193, 194mpbird 235 . . . 4
19613sqge0d 12388 . . . 4
197 0re 9589 . . . . 5
198 letri3 9665 . . . . 5
19915, 197, 198sylancl 666 . . . 4
200195, 196, 199mpbir2and 930 . . 3
20114, 200sqeq0d 12360 . 2
20212, 201abs00d 13446 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1872  wral 2709   class class class wbr 4361  cfv 5539  (class class class)co 6244  cc 9483  cr 9484  cc0 9485  c1 9486   caddc 9488   cmul 9490   clt 9621   cle 9622   cmin 9806  cneg 9807   cdiv 10215  c2 10605  cz 10883  crp 11248  cexp 12217  ccj 13098  cabs 13236  chil 26509   cva 26510   csm 26511   csp 26512  cno 26513   cmv 26515  csh 26518  cch 26519 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563  ax-hilex 26589  ax-hfvadd 26590  ax-hvass 26592  ax-hv0cl 26593  ax-hfvmul 26595  ax-hvdistr1 26598  ax-hvmul0 26600  ax-hfi 26669  ax-his1 26672  ax-his2 26673  ax-his3 26674  ax-his4 26675 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-2nd 6747  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-sup 7904  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-3 10615  df-n0 10816  df-z 10884  df-uz 11106  df-rp 11249  df-seq 12159  df-exp 12218  df-cj 13101  df-re 13102  df-im 13103  df-sqrt 13237  df-abs 13238  df-hnorm 26558  df-hvsub 26561  df-sh 26797  df-ch 26811 This theorem is referenced by:  pjhthlem2  26982
 Copyright terms: Public domain W3C validator