Step | Hyp | Ref
| Expression |
1 | | chscl.1 |
. . . . 5
|
2 | | chscl.2 |
. . . . 5
|
3 | | chscl.3 |
. . . . 5
|
4 | | chscl.4 |
. . . . 5
|
5 | | chscl.5 |
. . . . 5
|
6 | | chscl.6 |
. . . . 5
|
7 | 1, 2, 3, 4, 5, 6 | chscllem1 28496 |
. . . 4
|
8 | | chss 28086 |
. . . . 5
|
9 | 1, 8 | syl 17 |
. . . 4
|
10 | 7, 9 | fssd 6057 |
. . 3
|
11 | | hlimcaui 28093 |
. . . . . . 7
|
12 | 5, 11 | syl 17 |
. . . . . 6
|
13 | | hcaucvg 28043 |
. . . . . 6
|
14 | 12, 13 | sylan 488 |
. . . . 5
|
15 | | eluznn 11758 |
. . . . . . . . 9
|
16 | 15 | adantll 750 |
. . . . . . . 8
|
17 | | chsh 28081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
18 | 1, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
19 | | chsh 28081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
20 | 2, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
21 | | shscl 28177 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
22 | 18, 20, 21 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
|
23 | | shss 28067 |
. . . . . . . . . . . . . . . . . . . . . 22
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 25, 26 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 27 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
|
29 | 4, 24 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . 20
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
31 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 30, 31 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
|
33 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . . 18
|
34 | 28, 32, 33 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
35 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 7 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 35, 36 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 37 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
|
39 | 9 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40, 31 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 39, 41 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
|
43 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . . 18
|
44 | 38, 42, 43 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
|
45 | | hvsubcl 27874 |
. . . . . . . . . . . . . . . . 17
|
46 | 34, 44, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
47 | | normcl 27982 |
. . . . . . . . . . . . . . . 16
|
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
|
49 | 48 | sqge0d 13036 |
. . . . . . . . . . . . . 14
|
50 | | normcl 27982 |
. . . . . . . . . . . . . . . . 17
|
51 | 44, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
|
52 | 51 | resqcld 13035 |
. . . . . . . . . . . . . . 15
|
53 | 48 | resqcld 13035 |
. . . . . . . . . . . . . . 15
|
54 | 52, 53 | addge01d 10615 |
. . . . . . . . . . . . . 14
|
55 | 49, 54 | mpbid 222 |
. . . . . . . . . . . . 13
|
56 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
57 | 36 | adantrr 753 |
. . . . . . . . . . . . . . . . 17
|
58 | | shsubcl 28077 |
. . . . . . . . . . . . . . . . 17
|
59 | 56, 57, 41, 58 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
60 | | hvsubsub4 27917 |
. . . . . . . . . . . . . . . . . 18
|
61 | 28, 32, 38, 42, 60 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
|
62 | | ocsh 28142 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 39, 62 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
64 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
66 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
67 | 65, 6, 66 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
68 | 67 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
71 | 9, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
72 | | shless 28218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
73 | 20, 71, 18, 3, 72 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
74 | | shscom 28178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
75 | 18, 20, 74 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
76 | | shscom 28178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
77 | 18, 71, 76 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
78 | 73, 75, 77 | 3sstr4d 3648 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
80 | 79, 26 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
81 | | pjpreeq 28257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 70, 80, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 69, 82 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 83 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
86 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
87 | | shss 28067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
88 | 71, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
89 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
90 | 89 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
91 | | hvsubadd 27934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 85, 86, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 92, 93, 94 | 3bitr4g 303 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 95 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 84, 96 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | | risset 3062 |
. . . . . . . . . . . . . . . . . . . 20
|
99 | 97, 98 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
|
100 | 99 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
|
101 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 101 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
104 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
105 | 103, 104 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
|
106 | 105 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
|
107 | 102, 106 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 107, 99 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | adantrl 752 |
. . . . . . . . . . . . . . . . . 18
|
110 | | shsubcl 28077 |
. . . . . . . . . . . . . . . . . 18
|
111 | 63, 100, 109, 110 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
112 | 61, 111 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
|
113 | | shocorth 28151 |
. . . . . . . . . . . . . . . . 17
|
114 | 56, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
|
115 | 59, 112, 114 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
116 | | normpyth 28002 |
. . . . . . . . . . . . . . . 16
|
117 | 44, 46, 116 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
118 | 115, 117 | mpd 15 |
. . . . . . . . . . . . . 14
|
119 | | hvpncan3 27899 |
. . . . . . . . . . . . . . . . 17
|
120 | 44, 34, 119 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
123 | 118, 122 | eqtr3d 2658 |
. . . . . . . . . . . . 13
|
124 | 55, 123 | breqtrd 4679 |
. . . . . . . . . . . 12
|
125 | | normcl 27982 |
. . . . . . . . . . . . . 14
|
126 | 34, 125 | syl 17 |
. . . . . . . . . . . . 13
|
127 | | normge0 27983 |
. . . . . . . . . . . . . 14
|
128 | 44, 127 | syl 17 |
. . . . . . . . . . . . 13
|
129 | | normge0 27983 |
. . . . . . . . . . . . . 14
|
130 | 34, 129 | syl 17 |
. . . . . . . . . . . . 13
|
131 | 51, 126, 128, 130 | le2sqd 13044 |
. . . . . . . . . . . 12
|
132 | 124, 131 | mpbird 247 |
. . . . . . . . . . 11
|
133 | 132 | adantlr 751 |
. . . . . . . . . 10
|
134 | 51 | adantlr 751 |
. . . . . . . . . . 11
|
135 | 126 | adantlr 751 |
. . . . . . . . . . 11
|
136 | | rpre 11839 |
. . . . . . . . . . . 12
|
137 | 136 | ad2antlr 763 |
. . . . . . . . . . 11
|
138 | | lelttr 10128 |
. . . . . . . . . . 11
|
139 | 134, 135,
137, 138 | syl3anc 1326 |
. . . . . . . . . 10
|
140 | 133, 139 | mpand 711 |
. . . . . . . . 9
|
141 | 140 | anassrs 680 |
. . . . . . . 8
|
142 | 16, 141 | syldan 487 |
. . . . . . 7
|
143 | 142 | ralimdva 2962 |
. . . . . 6
|
144 | 143 | reximdva 3017 |
. . . . 5
|
145 | 14, 144 | mpd 15 |
. . . 4
|
146 | 145 | ralrimiva 2966 |
. . 3
|
147 | | hcau 28041 |
. . 3
|
148 | 10, 146, 147 | sylanbrc 698 |
. 2
|
149 | | ax-hcompl 28059 |
. 2
|
150 | | hlimf 28094 |
. . . . 5
|
151 | | ffn 6045 |
. . . . 5
|
152 | 150, 151 | ax-mp 5 |
. . . 4
|
153 | | fnbr 5993 |
. . . 4
|
154 | 152, 153 | mpan 706 |
. . 3
|
155 | 154 | rexlimivw 3029 |
. 2
|
156 | 148, 149,
155 | 3syl 18 |
1
|