Step | Hyp | Ref
| Expression |
1 | | hoiqssbllem1.y |
. . . 4
β’ (π β π β (β βm π)) |
2 | 1 | elexd 3479 |
. . 3
β’ (π β π β V) |
3 | | elmapfn 8825 |
. . . 4
β’ (π β (β
βm π)
β π Fn π) |
4 | 1, 3 | syl 17 |
. . 3
β’ (π β π Fn π) |
5 | | hoiqssbllem1.i |
. . . 4
β’
β²ππ |
6 | | hoiqssbllem1.c |
. . . . . . . 8
β’ (π β πΆ:πβΆβ) |
7 | 6 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (πΆβπ) β β) |
8 | 7 | rexrd 11229 |
. . . . . 6
β’ ((π β§ π β π) β (πΆβπ) β
β*) |
9 | | hoiqssbllem1.d |
. . . . . . . 8
β’ (π β π·:πβΆβ) |
10 | 9 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (π·βπ) β β) |
11 | 10 | rexrd 11229 |
. . . . . 6
β’ ((π β§ π β π) β (π·βπ) β
β*) |
12 | | elmapi 8809 |
. . . . . . . . 9
β’ (π β (β
βm π)
β π:πβΆβ) |
13 | 1, 12 | syl 17 |
. . . . . . . 8
β’ (π β π:πβΆβ) |
14 | 13 | ffvelcdmda 7055 |
. . . . . . 7
β’ ((π β§ π β π) β (πβπ) β β) |
15 | 14 | rexrd 11229 |
. . . . . 6
β’ ((π β§ π β π) β (πβπ) β
β*) |
16 | | hoiqssbllem1.e |
. . . . . . . . . . . . 13
β’ (π β πΈ β
β+) |
17 | | 2rp 12944 |
. . . . . . . . . . . . . . 15
β’ 2 β
β+ |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β+) |
19 | | hoiqssbllem1.n |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β β
) |
20 | | hoiqssbllem1.x |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β Fin) |
21 | | hashnncl 14291 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((β―βπ) β β β π β β
)) |
23 | 19, 22 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β―βπ) β
β) |
24 | 23 | nnred 12192 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―βπ) β
β) |
25 | 23 | nngt0d 12226 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 <
(β―βπ)) |
26 | 24, 25 | elrpd 12978 |
. . . . . . . . . . . . . . 15
β’ (π β (β―βπ) β
β+) |
27 | 26 | rpsqrtcld 15323 |
. . . . . . . . . . . . . 14
β’ (π β
(ββ(β―βπ)) β
β+) |
28 | 18, 27 | rpmulcld 12997 |
. . . . . . . . . . . . 13
β’ (π β (2 Β·
(ββ(β―βπ))) β
β+) |
29 | 16, 28 | rpdivcld 12998 |
. . . . . . . . . . . 12
β’ (π β (πΈ / (2 Β·
(ββ(β―βπ)))) β
β+) |
30 | 29 | rpred 12981 |
. . . . . . . . . . 11
β’ (π β (πΈ / (2 Β·
(ββ(β―βπ)))) β β) |
31 | 30 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΈ / (2 Β·
(ββ(β―βπ)))) β β) |
32 | 14, 31 | resubcld 11607 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) β β) |
33 | 32 | rexrd 11229 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) β
β*) |
34 | | hoiqssbllem1.l |
. . . . . . . 8
β’ ((π β§ π β π) β (πΆβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
35 | | iooltub 43901 |
. . . . . . . 8
β’ ((((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) β β* β§
(πβπ) β β* β§ (πΆβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β (πΆβπ) < (πβπ)) |
36 | 33, 15, 34, 35 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ π β π) β (πΆβπ) < (πβπ)) |
37 | 7, 14, 36 | ltled 11327 |
. . . . . 6
β’ ((π β§ π β π) β (πΆβπ) β€ (πβπ)) |
38 | 14, 31 | readdcld 11208 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β β) |
39 | 38 | rexrd 11229 |
. . . . . . 7
β’ ((π β§ π β π) β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β
β*) |
40 | | hoiqssbllem1.r |
. . . . . . 7
β’ ((π β§ π β π) β (π·βπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
41 | | ioogtlb 43886 |
. . . . . . 7
β’ (((πβπ) β β* β§ ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β β* β§
(π·βπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β (πβπ) < (π·βπ)) |
42 | 15, 39, 40, 41 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π β π) β (πβπ) < (π·βπ)) |
43 | 8, 11, 15, 37, 42 | elicod 13339 |
. . . . 5
β’ ((π β§ π β π) β (πβπ) β ((πΆβπ)[,)(π·βπ))) |
44 | 43 | ex 413 |
. . . 4
β’ (π β (π β π β (πβπ) β ((πΆβπ)[,)(π·βπ)))) |
45 | 5, 44 | ralrimi 3251 |
. . 3
β’ (π β βπ β π (πβπ) β ((πΆβπ)[,)(π·βπ))) |
46 | 2, 4, 45 | 3jca 1128 |
. 2
β’ (π β (π β V β§ π Fn π β§ βπ β π (πβπ) β ((πΆβπ)[,)(π·βπ)))) |
47 | | elixp2 8861 |
. 2
β’ (π β Xπ β
π ((πΆβπ)[,)(π·βπ)) β (π β V β§ π Fn π β§ βπ β π (πβπ) β ((πΆβπ)[,)(π·βπ)))) |
48 | 46, 47 | sylibr 233 |
1
β’ (π β π β Xπ β π ((πΆβπ)[,)(π·βπ))) |