Step | Hyp | Ref
| Expression |
1 | | qndenserrnbllem.i |
. . . 4
β’ (π β πΌ β Fin) |
2 | | inss1 4189 |
. . . . . 6
β’ (β
β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β
β |
3 | | qex 12891 |
. . . . . 6
β’ β
β V |
4 | | ssexg 5281 |
. . . . . 6
β’
(((β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β β β§
β β V) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β
V) |
5 | 2, 3, 4 | mp2an 691 |
. . . . 5
β’ (β
β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β V |
6 | 5 | a1i 11 |
. . . 4
β’ ((π β§ π β πΌ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β
V) |
7 | | qndenserrnbllem.x |
. . . . . . . . . . . 12
β’ (π β π β (β βm πΌ)) |
8 | | elmapi 8790 |
. . . . . . . . . . . 12
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
β’ (π β π:πΌβΆβ) |
10 | 9 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β π:πΌβΆβ) |
11 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β π β πΌ) |
12 | 10, 11 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (πβπ) β β) |
13 | 12 | rexrd 11210 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (πβπ) β
β*) |
14 | | qndenserrnbllem.e |
. . . . . . . . . . . . 13
β’ (π β πΈ β
β+) |
15 | 14 | rpred 12962 |
. . . . . . . . . . . 12
β’ (π β πΈ β β) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β πΈ β β) |
17 | | ne0i 4295 |
. . . . . . . . . . . . . . 15
β’ (π β πΌ β πΌ β β
) |
18 | 17 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β πΌ β β
) |
19 | | hashnncl 14272 |
. . . . . . . . . . . . . . . 16
β’ (πΌ β Fin β
((β―βπΌ) β
β β πΌ β
β
)) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β―βπΌ) β β β πΌ β β
)) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β ((β―βπΌ) β β β πΌ β β
)) |
22 | 18, 21 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (β―βπΌ) β β) |
23 | 22 | nnred 12173 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β (β―βπΌ) β β) |
24 | | 0red 11163 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β 0 β β) |
25 | 22 | nngt0d 12207 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β 0 < (β―βπΌ)) |
26 | 24, 23, 25 | ltled 11308 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β 0 β€ (β―βπΌ)) |
27 | 23, 26 | resqrtcld 15308 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (ββ(β―βπΌ)) β
β) |
28 | 23, 25 | elrpd 12959 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (β―βπΌ) β
β+) |
29 | 28 | sqrtgt0d 15303 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β 0 <
(ββ(β―βπΌ))) |
30 | 24, 29 | gtned 11295 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (ββ(β―βπΌ)) β 0) |
31 | 16, 27, 30 | redivcld 11988 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (πΈ / (ββ(β―βπΌ))) β
β) |
32 | 12, 31 | readdcld 11189 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β) |
33 | 32 | rexrd 11210 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β*) |
34 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β πΈ β
β+) |
35 | 27, 29 | elrpd 12959 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (ββ(β―βπΌ)) β
β+) |
36 | 34, 35 | rpdivcld 12979 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (πΈ / (ββ(β―βπΌ))) β
β+) |
37 | 12, 36 | ltaddrpd 12995 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (πβπ) < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) |
38 | | qbtwnxr 13125 |
. . . . . . . 8
β’ (((πβπ) β β* β§ ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β β*
β§ (πβπ) < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) β βπ β β ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
39 | 13, 33, 37, 38 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β πΌ) β βπ β β ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
40 | | df-rex 3071 |
. . . . . . 7
β’
(βπ β
β ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) β βπ(π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
41 | 39, 40 | sylib 217 |
. . . . . 6
β’ ((π β§ π β πΌ) β βπ(π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
42 | | simprl 770 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π β
β) |
43 | 13 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β (πβπ) β
β*) |
44 | 33 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β*) |
45 | | qre 12883 |
. . . . . . . . . . 11
β’ (π β β β π β
β) |
46 | 45 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π β
β) |
47 | | simprrl 780 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β (πβπ) < π) |
48 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) |
49 | 43, 44, 46, 47, 48 | eliood 43822 |
. . . . . . . . 9
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
50 | 42, 49 | elind 4155 |
. . . . . . . 8
β’ (((π β§ π β πΌ) β§ (π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
51 | 50 | ex 414 |
. . . . . . 7
β’ ((π β§ π β πΌ) β ((π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) |
52 | 51 | eximdv 1921 |
. . . . . 6
β’ ((π β§ π β πΌ) β (βπ(π β β β§ ((πβπ) < π β§ π < ((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β βπ π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) |
53 | 41, 52 | mpd 15 |
. . . . 5
β’ ((π β§ π β πΌ) β βπ π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
54 | | n0 4307 |
. . . . 5
β’ ((β
β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β β
β
βπ π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
55 | 53, 54 | sylibr 233 |
. . . 4
β’ ((π β§ π β πΌ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β
β
) |
56 | 1, 6, 55 | choicefi 43508 |
. . 3
β’ (π β βπ¦(π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) |
57 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ Fn πΌ β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β
β) |
58 | 57 | sseld 3944 |
. . . . . . . . . . 11
β’ (π¦ Fn πΌ β ((π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β (π¦βπ) β β)) |
59 | 58 | ralimdv 3163 |
. . . . . . . . . 10
β’ (π¦ Fn πΌ β (βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β βπ β πΌ (π¦βπ) β β)) |
60 | 59 | imdistani 570 |
. . . . . . . . 9
β’ ((π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β β)) |
61 | | ffnfv 7067 |
. . . . . . . . 9
β’ (π¦:πΌβΆβ β (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β β)) |
62 | 60, 61 | sylibr 233 |
. . . . . . . 8
β’ ((π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β π¦:πΌβΆβ) |
63 | 62 | adantl 483 |
. . . . . . 7
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β π¦:πΌβΆβ) |
64 | 3 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
V) |
65 | | elmapg 8781 |
. . . . . . . . 9
β’ ((β
β V β§ πΌ β
Fin) β (π¦ β
(β βm πΌ) β π¦:πΌβΆβ)) |
66 | 64, 1, 65 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π¦ β (β βm πΌ) β π¦:πΌβΆβ)) |
67 | 66 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (π¦ β (β
βm πΌ)
β π¦:πΌβΆβ)) |
68 | 63, 67 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β π¦ β (β
βm πΌ)) |
69 | | reex 11147 |
. . . . . . . . . . 11
β’ β
β V |
70 | 45 | ssriv 3949 |
. . . . . . . . . . 11
β’ β
β β |
71 | | mapss 8830 |
. . . . . . . . . . 11
β’ ((β
β V β§ β β β) β (β βm
πΌ) β (β
βm πΌ)) |
72 | 69, 70, 71 | mp2an 691 |
. . . . . . . . . 10
β’ (β
βm πΌ)
β (β βm πΌ) |
73 | 72 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (β
βm πΌ)
β (β βm πΌ)) |
74 | 73, 68 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β π¦ β (β
βm πΌ)) |
75 | 1 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β πΌ β Fin) |
76 | | qndenserrnbllem.n |
. . . . . . . . . . 11
β’ (π β πΌ β β
) |
77 | 76 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β πΌ β β
) |
78 | | eqid 2733 |
. . . . . . . . . 10
β’
(β―βπΌ) =
(β―βπΌ) |
79 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β π β (β
βm πΌ)) |
80 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β§ π β πΌ) β π) |
81 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (π¦βπ) = (π¦βπ)) |
82 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβπ) = (πβπ)) |
83 | 82 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) = ((πβπ) + (πΈ / (ββ(β―βπΌ))))) |
84 | 82, 83 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) = ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
85 | 84 | ineq2d 4173 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) = (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
86 | 81, 85 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) |
87 | 86 | cbvralvw 3224 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
88 | 87 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
((βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β§ π β πΌ) β βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
90 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
((βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β§ π β πΌ) β π β πΌ) |
91 | | rspa 3230 |
. . . . . . . . . . . . . . 15
β’
((βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β§ π β πΌ) β (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
92 | 89, 90, 91 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
((βπ β
πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β§ π β πΌ) β (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
93 | 92 | adantll 713 |
. . . . . . . . . . . . 13
β’ (((π β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β§ π β πΌ) β (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) |
94 | | elinel2 4157 |
. . . . . . . . . . . . 13
β’ ((π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β§ π β πΌ) β (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
96 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β§ π β πΌ) β π β πΌ) |
97 | 9 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΌ) β (πβπ) β β) |
98 | 97 | 3adant2 1132 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πβπ) β β) |
99 | | simp2 1138 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) |
100 | 99 | elioored 43873 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (π¦βπ) β β) |
101 | 98 | rexrd 11210 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πβπ) β
β*) |
102 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β πΈ β β) |
103 | 76, 20 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (β―βπΌ) β
β) |
104 | 103 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (β―βπΌ) β
β) |
105 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β (β―βπΌ) β β) |
106 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 β
β) |
107 | 103 | nngt0d 12207 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β 0 <
(β―βπΌ)) |
108 | 106, 104,
107 | ltled 11308 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β 0 β€
(β―βπΌ)) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΌ) β 0 β€ (β―βπΌ)) |
110 | 105, 109 | resqrtcld 15308 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β (ββ(β―βπΌ)) β
β) |
111 | | sqrtgt0 15149 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β―βπΌ)
β β β§ 0 < (β―βπΌ)) β 0 <
(ββ(β―βπΌ))) |
112 | 104, 107,
111 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β 0 <
(ββ(β―βπΌ))) |
113 | 106, 112 | gtned 11295 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(ββ(β―βπΌ)) β 0) |
114 | 113 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΌ) β (ββ(β―βπΌ)) β 0) |
115 | 102, 110,
114 | redivcld 11988 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΌ) β (πΈ / (ββ(β―βπΌ))) β
β) |
116 | 97, 115 | readdcld 11189 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β) |
117 | 116 | rexrd 11210 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β*) |
118 | 117 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β*) |
119 | | ioogtlb 43819 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ) β β* β§ ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β β*
β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β (πβπ) < (π¦βπ)) |
120 | 101, 118,
99, 119 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πβπ) < (π¦βπ)) |
121 | 98, 100, 120 | ltled 11308 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πβπ) β€ (π¦βπ)) |
122 | 98, 100, 121 | abssuble0d 15323 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (absβ((πβπ) β (π¦βπ))) = ((π¦βπ) β (πβπ))) |
123 | 116 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β
β) |
124 | | iooltub 43834 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ) β β* β§ ((πβπ) + (πΈ / (ββ(β―βπΌ)))) β β*
β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))) β (π¦βπ) < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) |
125 | 101, 118,
99, 124 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (π¦βπ) < ((πβπ) + (πΈ / (ββ(β―βπΌ))))) |
126 | 100, 123,
98, 125 | ltsub1dd 11772 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β ((π¦βπ) β (πβπ)) < (((πβπ) + (πΈ / (ββ(β―βπΌ)))) β (πβπ))) |
127 | 98 | recnd 11188 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πβπ) β β) |
128 | 104, 108 | resqrtcld 15308 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(ββ(β―βπΌ)) β β) |
129 | 15, 128, 113 | redivcld 11988 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΈ / (ββ(β―βπΌ))) β
β) |
130 | 129 | recnd 11188 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΈ / (ββ(β―βπΌ))) β
β) |
131 | 130 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (πΈ / (ββ(β―βπΌ))) β
β) |
132 | 127, 131 | pncan2d 11519 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (((πβπ) + (πΈ / (ββ(β―βπΌ)))) β (πβπ)) = (πΈ / (ββ(β―βπΌ)))) |
133 | 126, 132 | breqtrd 5132 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β ((π¦βπ) β (πβπ)) < (πΈ / (ββ(β―βπΌ)))) |
134 | 122, 133 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦βπ) β ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))) β§ π β πΌ) β (absβ((πβπ) β (π¦βπ))) < (πΈ / (ββ(β―βπΌ)))) |
135 | 80, 95, 96, 134 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β§ π β πΌ) β (absβ((πβπ) β (π¦βπ))) < (πΈ / (ββ(β―βπΌ)))) |
136 | 135 | adantlrl 719 |
. . . . . . . . . 10
β’ (((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β§ π β πΌ) β (absβ((πβπ) β (π¦βπ))) < (πΈ / (ββ(β―βπΌ)))) |
137 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β πΈ β
β+) |
138 | 104, 107 | elrpd 12959 |
. . . . . . . . . . . . 13
β’ (π β (β―βπΌ) β
β+) |
139 | 138 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
(β―βπΌ) β
β+) |
140 | 139 | rpsqrtcld 15302 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
(ββ(β―βπΌ)) β
β+) |
141 | 137, 140 | rpdivcld 12979 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (πΈ /
(ββ(β―βπΌ))) β
β+) |
142 | | qndenserrnbllem.d |
. . . . . . . . . 10
β’ π· =
(distβ(β^βπΌ)) |
143 | 75, 77, 78, 79, 74, 136, 141, 142 | rrndistlt 44617 |
. . . . . . . . 9
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (ππ·π¦) < ((ββ(β―βπΌ)) Β· (πΈ / (ββ(β―βπΌ))))) |
144 | 137 | rpcnd 12964 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β πΈ β
β) |
145 | 139 | rpcnd 12964 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
(β―βπΌ) β
β) |
146 | 145 | sqrtcld 15328 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
(ββ(β―βπΌ)) β β) |
147 | 140 | rpne0d 12967 |
. . . . . . . . . 10
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
(ββ(β―βπΌ)) β 0) |
148 | 144, 146,
147 | divcan2d 11938 |
. . . . . . . . 9
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β
((ββ(β―βπΌ)) Β· (πΈ / (ββ(β―βπΌ)))) = πΈ) |
149 | 143, 148 | breqtrd 5132 |
. . . . . . . 8
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (ππ·π¦) < πΈ) |
150 | 74, 149 | jca 513 |
. . . . . . 7
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (π¦ β (β
βm πΌ) β§
(ππ·π¦) < πΈ)) |
151 | 142 | rrxmetfi 24792 |
. . . . . . . . . . 11
β’ (πΌ β Fin β π· β (Metβ(β
βm πΌ))) |
152 | 1, 151 | syl 17 |
. . . . . . . . . 10
β’ (π β π· β (Metβ(β
βm πΌ))) |
153 | | metxmet 23703 |
. . . . . . . . . 10
β’ (π· β (Metβ(β
βm πΌ))
β π· β
(βMetβ(β βm πΌ))) |
154 | 152, 153 | syl 17 |
. . . . . . . . 9
β’ (π β π· β (βMetβ(β
βm πΌ))) |
155 | 15 | rexrd 11210 |
. . . . . . . . 9
β’ (π β πΈ β
β*) |
156 | | elbl 23757 |
. . . . . . . . 9
β’ ((π· β
(βMetβ(β βm πΌ)) β§ π β (β βm πΌ) β§ πΈ β β*) β (π¦ β (π(ballβπ·)πΈ) β (π¦ β (β βm πΌ) β§ (ππ·π¦) < πΈ))) |
157 | 154, 7, 155, 156 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π¦ β (π(ballβπ·)πΈ) β (π¦ β (β βm πΌ) β§ (ππ·π¦) < πΈ))) |
158 | 157 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (π¦ β (π(ballβπ·)πΈ) β (π¦ β (β βm πΌ) β§ (ππ·π¦) < πΈ))) |
159 | 150, 158 | mpbird 257 |
. . . . . 6
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β π¦ β (π(ballβπ·)πΈ)) |
160 | 68, 159 | jca 513 |
. . . . 5
β’ ((π β§ (π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ)))))))) β (π¦ β (β
βm πΌ) β§
π¦ β (π(ballβπ·)πΈ))) |
161 | 160 | ex 414 |
. . . 4
β’ (π β ((π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β (π¦ β (β
βm πΌ) β§
π¦ β (π(ballβπ·)πΈ)))) |
162 | 161 | eximdv 1921 |
. . 3
β’ (π β (βπ¦(π¦ Fn πΌ β§ βπ β πΌ (π¦βπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (ββ(β―βπΌ))))))) β βπ¦(π¦ β (β βm πΌ) β§ π¦ β (π(ballβπ·)πΈ)))) |
163 | 56, 162 | mpd 15 |
. 2
β’ (π β βπ¦(π¦ β (β βm πΌ) β§ π¦ β (π(ballβπ·)πΈ))) |
164 | | df-rex 3071 |
. 2
β’
(βπ¦ β
(β βm πΌ)π¦ β (π(ballβπ·)πΈ) β βπ¦(π¦ β (β βm πΌ) β§ π¦ β (π(ballβπ·)πΈ))) |
165 | 163, 164 | sylibr 233 |
1
β’ (π β βπ¦ β (β βm πΌ)π¦ β (π(ballβπ·)πΈ)) |