Step | Hyp | Ref
| Expression |
1 | | hoiqssbllem3.x |
. . . . . . 7
|
2 | | qex 11800 |
. . . . . . . . 9
|
3 | 2 | inex1 4799 |
. . . . . . . 8
|
4 | 3 | a1i 11 |
. . . . . . 7
|
5 | | hoiqssbllem3.y |
. . . . . . . . . . . . 13
|
6 | | elmapi 7879 |
. . . . . . . . . . . . 13
|
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
|
8 | 7 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
9 | | hoiqssbllem3.e |
. . . . . . . . . . . . 13
|
10 | | 2rp 11837 |
. . . . . . . . . . . . . . 15
|
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
|
12 | | hoiqssbllem3.n |
. . . . . . . . . . . . . . . . 17
|
13 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . . 18
|
14 | 1, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
15 | 12, 14 | mpbird 247 |
. . . . . . . . . . . . . . . 16
|
16 | | nnrp 11842 |
. . . . . . . . . . . . . . . 16
|
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . 15
|
18 | 17 | rpsqrtcld 14150 |
. . . . . . . . . . . . . 14
|
19 | 11, 18 | rpmulcld 11888 |
. . . . . . . . . . . . 13
|
20 | 9, 19 | rpdivcld 11889 |
. . . . . . . . . . . 12
|
21 | 20 | adantr 481 |
. . . . . . . . . . 11
|
22 | 8, 21 | ltsubrpd 11904 |
. . . . . . . . . 10
|
23 | 21 | rpred 11872 |
. . . . . . . . . . . 12
|
24 | 8, 23 | resubcld 10458 |
. . . . . . . . . . 11
|
25 | 24, 8 | ltnled 10184 |
. . . . . . . . . 10
|
26 | 22, 25 | mpbid 222 |
. . . . . . . . 9
|
27 | 24 | rexrd 10089 |
. . . . . . . . . 10
|
28 | 8 | rexrd 10089 |
. . . . . . . . . 10
|
29 | 27, 28 | qinioo 39762 |
. . . . . . . . 9
|
30 | 26, 29 | mtbird 315 |
. . . . . . . 8
|
31 | 30 | neqned 2801 |
. . . . . . 7
|
32 | 1, 4, 31 | choicefi 39392 |
. . . . . 6
|
33 | | simpl 473 |
. . . . . . . . . . . . 13
|
34 | | nfra1 2941 |
. . . . . . . . . . . . . . 15
|
35 | | rspa 2930 |
. . . . . . . . . . . . . . . . 17
|
36 | | elinel1 3799 |
. . . . . . . . . . . . . . . . 17
|
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | ex 450 |
. . . . . . . . . . . . . . 15
|
39 | 34, 38 | ralrimi 2957 |
. . . . . . . . . . . . . 14
|
40 | 39 | adantl 482 |
. . . . . . . . . . . . 13
|
41 | 33, 40 | jca 554 |
. . . . . . . . . . . 12
|
42 | 41 | adantl 482 |
. . . . . . . . . . 11
|
43 | | ffnfv 6388 |
. . . . . . . . . . 11
|
44 | 42, 43 | sylibr 224 |
. . . . . . . . . 10
|
45 | 2 | a1i 11 |
. . . . . . . . . . . 12
|
46 | | elmapg 7870 |
. . . . . . . . . . . 12
|
47 | 45, 1, 46 | syl2anc 693 |
. . . . . . . . . . 11
|
48 | 47 | adantr 481 |
. . . . . . . . . 10
|
49 | 44, 48 | mpbird 247 |
. . . . . . . . 9
|
50 | | simprr 796 |
. . . . . . . . 9
|
51 | 49, 50 | jca 554 |
. . . . . . . 8
|
52 | 51 | ex 450 |
. . . . . . 7
|
53 | 52 | eximdv 1846 |
. . . . . 6
|
54 | 32, 53 | mpd 15 |
. . . . 5
|
55 | | df-rex 2918 |
. . . . 5
|
56 | 54, 55 | sylibr 224 |
. . . 4
|
57 | 2 | inex1 4799 |
. . . . . . . 8
|
58 | 57 | a1i 11 |
. . . . . . 7
|
59 | 8, 21 | ltaddrpd 11905 |
. . . . . . . . . 10
|
60 | 8, 23 | readdcld 10069 |
. . . . . . . . . . 11
|
61 | 8, 60 | ltnled 10184 |
. . . . . . . . . 10
|
62 | 59, 61 | mpbid 222 |
. . . . . . . . 9
|
63 | 60 | rexrd 10089 |
. . . . . . . . . 10
|
64 | 28, 63 | qinioo 39762 |
. . . . . . . . 9
|
65 | 62, 64 | mtbird 315 |
. . . . . . . 8
|
66 | 65 | neqned 2801 |
. . . . . . 7
|
67 | 1, 58, 66 | choicefi 39392 |
. . . . . 6
|
68 | | simpl 473 |
. . . . . . . . . . . . 13
|
69 | | nfra1 2941 |
. . . . . . . . . . . . . . 15
|
70 | | rspa 2930 |
. . . . . . . . . . . . . . . . 17
|
71 | | elinel1 3799 |
. . . . . . . . . . . . . . . . 17
|
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
|
73 | 72 | ex 450 |
. . . . . . . . . . . . . . 15
|
74 | 69, 73 | ralrimi 2957 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantl 482 |
. . . . . . . . . . . . 13
|
76 | 68, 75 | jca 554 |
. . . . . . . . . . . 12
|
77 | 76 | adantl 482 |
. . . . . . . . . . 11
|
78 | | ffnfv 6388 |
. . . . . . . . . . 11
|
79 | 77, 78 | sylibr 224 |
. . . . . . . . . 10
|
80 | | elmapg 7870 |
. . . . . . . . . . . 12
|
81 | 45, 1, 80 | syl2anc 693 |
. . . . . . . . . . 11
|
82 | 81 | adantr 481 |
. . . . . . . . . 10
|
83 | 79, 82 | mpbird 247 |
. . . . . . . . 9
|
84 | | simprr 796 |
. . . . . . . . 9
|
85 | 83, 84 | jca 554 |
. . . . . . . 8
|
86 | 85 | ex 450 |
. . . . . . 7
|
87 | 86 | eximdv 1846 |
. . . . . 6
|
88 | 67, 87 | mpd 15 |
. . . . 5
|
89 | | df-rex 2918 |
. . . . 5
|
90 | 88, 89 | sylibr 224 |
. . . 4
|
91 | 56, 90 | jca 554 |
. . 3
|
92 | | reeanv 3107 |
. . 3
|
93 | 91, 92 | sylibr 224 |
. 2
|
94 | | nfv 1843 |
. . . . . . . 8
|
95 | 34, 69 | nfan 1828 |
. . . . . . . 8
|
96 | 94, 95 | nfan 1828 |
. . . . . . 7
|
97 | 1 | ad3antrrr 766 |
. . . . . . 7
|
98 | 12 | ad3antrrr 766 |
. . . . . . 7
|
99 | 5 | ad3antrrr 766 |
. . . . . . 7
|
100 | | elmapi 7879 |
. . . . . . . . . 10
|
101 | | qssre 11798 |
. . . . . . . . . . 11
|
102 | 101 | a1i 11 |
. . . . . . . . . 10
|
103 | 100, 102 | fssd 6057 |
. . . . . . . . 9
|
104 | 103 | adantl 482 |
. . . . . . . 8
|
105 | 104 | ad2antrr 762 |
. . . . . . 7
|
106 | | elmapi 7879 |
. . . . . . . . 9
|
107 | 101 | a1i 11 |
. . . . . . . . 9
|
108 | 106, 107 | fssd 6057 |
. . . . . . . 8
|
109 | 108 | ad2antlr 763 |
. . . . . . 7
|
110 | 9 | ad3antrrr 766 |
. . . . . . 7
|
111 | 35 | elin2d 3803 |
. . . . . . . . 9
|
112 | 111 | adantlr 751 |
. . . . . . . 8
|
113 | 112 | adantll 750 |
. . . . . . 7
|
114 | 70 | elin2d 3803 |
. . . . . . . . 9
|
115 | 114 | adantll 750 |
. . . . . . . 8
|
116 | 115 | adantll 750 |
. . . . . . 7
|
117 | 96, 97, 98, 99, 105, 109, 110, 113, 116 | hoiqssbllem1 40836 |
. . . . . 6
|
118 | | simpl 473 |
. . . . . . 7
|
119 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
120 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
121 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
122 | 121, 120 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
123 | 122 | ineq2d 3814 |
. . . . . . . . . . . . 13
|
124 | 119, 123 | eleq12d 2695 |
. . . . . . . . . . . 12
|
125 | 124 | cbvralv 3171 |
. . . . . . . . . . 11
|
126 | 125 | biimpi 206 |
. . . . . . . . . 10
|
127 | 126 | adantr 481 |
. . . . . . . . 9
|
128 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
129 | 120 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
130 | 120, 129 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
131 | 130 | ineq2d 3814 |
. . . . . . . . . . . . 13
|
132 | 128, 131 | eleq12d 2695 |
. . . . . . . . . . . 12
|
133 | 132 | cbvralv 3171 |
. . . . . . . . . . 11
|
134 | 133 | biimpi 206 |
. . . . . . . . . 10
|
135 | 134 | adantl 482 |
. . . . . . . . 9
|
136 | 127, 135 | jca 554 |
. . . . . . . 8
|
137 | 136 | adantl 482 |
. . . . . . 7
|
138 | | nfv 1843 |
. . . . . . . 8
|
139 | 1 | ad3antrrr 766 |
. . . . . . . 8
|
140 | 12 | ad3antrrr 766 |
. . . . . . . 8
|
141 | 5 | ad3antrrr 766 |
. . . . . . . 8
|
142 | 104 | ad2antrr 762 |
. . . . . . . 8
|
143 | 108 | ad2antlr 763 |
. . . . . . . 8
|
144 | 9 | ad3antrrr 766 |
. . . . . . . 8
|
145 | 125, 111 | sylanbr 490 |
. . . . . . . . . 10
|
146 | 145 | adantlr 751 |
. . . . . . . . 9
|
147 | 146 | adantll 750 |
. . . . . . . 8
|
148 | 133, 114 | sylanbr 490 |
. . . . . . . . . 10
|
149 | 148 | adantll 750 |
. . . . . . . . 9
|
150 | 149 | adantll 750 |
. . . . . . . 8
|
151 | 138, 139,
140, 141, 142, 143, 144, 147, 150 | hoiqssbllem2 40837 |
. . . . . . 7
ℝ^ |
152 | 118, 137,
151 | syl2anc 693 |
. . . . . 6
ℝ^ |
153 | 117, 152 | jca 554 |
. . . . 5
ℝ^ |
154 | 153 | ex 450 |
. . . 4
ℝ^ |
155 | 154 | reximdva 3017 |
. . 3
ℝ^ |
156 | 155 | reximdva 3017 |
. 2
ℝ^ |
157 | 93, 156 | mpd 15 |
1
ℝ^ |