Step | Hyp | Ref
| Expression |
1 | | hoiqssbllem3.x |
. . . . . . 7
β’ (π β π β Fin) |
2 | | qex 12891 |
. . . . . . . . 9
β’ β
β V |
3 | 2 | inex1 5275 |
. . . . . . . 8
β’ (β
β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β V |
4 | 3 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β V) |
5 | | hoiqssbllem3.y |
. . . . . . . . . . . . 13
β’ (π β π β (β βm π)) |
6 | | elmapi 8790 |
. . . . . . . . . . . . 13
β’ (π β (β
βm π)
β π:πβΆβ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π:πβΆβ) |
8 | 7 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πβπ) β β) |
9 | | hoiqssbllem3.e |
. . . . . . . . . . . . 13
β’ (π β πΈ β
β+) |
10 | | 2rp 12925 |
. . . . . . . . . . . . . . 15
β’ 2 β
β+ |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 2 β
β+) |
12 | | hoiqssbllem3.n |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β
) |
13 | | hashnncl 14272 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
14 | 1, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((β―βπ) β β β π β β
)) |
15 | 12, 14 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (π β (β―βπ) β
β) |
16 | | nnrp 12931 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ)
β β β (β―βπ) β
β+) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (β―βπ) β
β+) |
18 | 17 | rpsqrtcld 15302 |
. . . . . . . . . . . . . 14
β’ (π β
(ββ(β―βπ)) β
β+) |
19 | 11, 18 | rpmulcld 12978 |
. . . . . . . . . . . . 13
β’ (π β (2 Β·
(ββ(β―βπ))) β
β+) |
20 | 9, 19 | rpdivcld 12979 |
. . . . . . . . . . . 12
β’ (π β (πΈ / (2 Β·
(ββ(β―βπ)))) β
β+) |
21 | 20 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΈ / (2 Β·
(ββ(β―βπ)))) β
β+) |
22 | 8, 21 | ltsubrpd 12994 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) < (πβπ)) |
23 | 21 | rpred 12962 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΈ / (2 Β·
(ββ(β―βπ)))) β β) |
24 | 8, 23 | resubcld 11588 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) β β) |
25 | 24, 8 | ltnled 11307 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) < (πβπ) β Β¬ (πβπ) β€ ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))))) |
26 | 22, 25 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β π) β Β¬ (πβπ) β€ ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))) |
27 | 24 | rexrd 11210 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) β
β*) |
28 | 8 | rexrd 11210 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πβπ) β
β*) |
29 | 27, 28 | qinioo 43859 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) = β
β (πβπ) β€ ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))))) |
30 | 26, 29 | mtbird 325 |
. . . . . . . 8
β’ ((π β§ π β π) β Β¬ (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) = β
) |
31 | 30 | neqned 2947 |
. . . . . . 7
β’ ((π β§ π β π) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β β
) |
32 | 1, 4, 31 | choicefi 43508 |
. . . . . 6
β’ (π β βπ(π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) |
33 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) β π Fn π) |
34 | | nfra1 3266 |
. . . . . . . . . . . . . . 15
β’
β²πβπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
35 | | rspa 3230 |
. . . . . . . . . . . . . . . . 17
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ π β π) β (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
36 | | elinel1 4156 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β (πβπ) β β) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ π β π) β (πβπ) β β) |
38 | 37 | ex 414 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β (π β π β (πβπ) β β)) |
39 | 34, 38 | ralrimi 3239 |
. . . . . . . . . . . . . 14
β’
(βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β βπ β π (πβπ) β β) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) β βπ β π (πβπ) β β) |
41 | 33, 40 | jca 513 |
. . . . . . . . . . . 12
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) β (π Fn π β§ βπ β π (πβπ) β β)) |
42 | 41 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β (π Fn π β§ βπ β π (πβπ) β β)) |
43 | | ffnfv 7067 |
. . . . . . . . . . 11
β’ (π:πβΆβ β (π Fn π β§ βπ β π (πβπ) β β)) |
44 | 42, 43 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β π:πβΆβ) |
45 | 2 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
V) |
46 | | elmapg 8781 |
. . . . . . . . . . . 12
β’ ((β
β V β§ π β
Fin) β (π β
(β βm π) β π:πβΆβ)) |
47 | 45, 1, 46 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π β (β βm π) β π:πβΆβ)) |
48 | 47 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β (π β (β βm π) β π:πβΆβ)) |
49 | 44, 48 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β π β (β βm π)) |
50 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
51 | 49, 50 | jca 513 |
. . . . . . . 8
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) β (π β (β βm π) β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) |
52 | 51 | ex 414 |
. . . . . . 7
β’ (π β ((π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) β (π β (β βm π) β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))))) |
53 | 52 | eximdv 1921 |
. . . . . 6
β’ (π β (βπ(π Fn π β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))))) |
54 | 32, 53 | mpd 15 |
. . . . 5
β’ (π β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) |
55 | | df-rex 3071 |
. . . . 5
β’
(βπ β
(β βm π)βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) |
56 | 54, 55 | sylibr 233 |
. . . 4
β’ (π β βπ β (β βm π)βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
57 | 2 | inex1 5275 |
. . . . . . . 8
β’ (β
β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β V |
58 | 57 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β V) |
59 | 8, 21 | ltaddrpd 12995 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πβπ) < ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))) |
60 | 8, 23 | readdcld 11189 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β β) |
61 | 8, 60 | ltnled 11307 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((πβπ) < ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β Β¬ ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β€ (πβπ))) |
62 | 59, 61 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β π) β Β¬ ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β€ (πβπ)) |
63 | 60 | rexrd 11210 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β
β*) |
64 | 28, 63 | qinioo 43859 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) = β
β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) β€ (πβπ))) |
65 | 62, 64 | mtbird 325 |
. . . . . . . 8
β’ ((π β§ π β π) β Β¬ (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) = β
) |
66 | 65 | neqned 2947 |
. . . . . . 7
β’ ((π β§ π β π) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β β
) |
67 | 1, 58, 66 | choicefi 43508 |
. . . . . 6
β’ (π β βπ(π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
68 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β π Fn π) |
69 | | nfra1 3266 |
. . . . . . . . . . . . . . 15
β’
β²πβπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
70 | | rspa 3230 |
. . . . . . . . . . . . . . . . 17
β’
((βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β§ π β π) β (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
71 | | elinel1 4156 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β (πβπ) β β) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β§ π β π) β (πβπ) β β) |
73 | 72 | ex 414 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β (π β π β (πβπ) β β)) |
74 | 69, 73 | ralrimi 3239 |
. . . . . . . . . . . . . 14
β’
(βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β βπ β π (πβπ) β β) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ β π (πβπ) β β) |
76 | 68, 75 | jca 513 |
. . . . . . . . . . . 12
β’ ((π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β (π Fn π β§ βπ β π (πβπ) β β)) |
77 | 76 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β (π Fn π β§ βπ β π (πβπ) β β)) |
78 | | ffnfv 7067 |
. . . . . . . . . . 11
β’ (π:πβΆβ β (π Fn π β§ βπ β π (πβπ) β β)) |
79 | 77, 78 | sylibr 233 |
. . . . . . . . . 10
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π:πβΆβ) |
80 | | elmapg 8781 |
. . . . . . . . . . . 12
β’ ((β
β V β§ π β
Fin) β (π β
(β βm π) β π:πβΆβ)) |
81 | 45, 1, 80 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (π β (β βm π) β π:πβΆβ)) |
82 | 81 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β (π β (β βm π) β π:πβΆβ)) |
83 | 79, 82 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β (β βm π)) |
84 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
85 | 83, 84 | jca 513 |
. . . . . . . 8
β’ ((π β§ (π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β (π β (β βm π) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
86 | 85 | ex 414 |
. . . . . . 7
β’ (π β ((π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β (π β (β βm π) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))))) |
87 | 86 | eximdv 1921 |
. . . . . 6
β’ (π β (βπ(π Fn π β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))))) |
88 | 67, 87 | mpd 15 |
. . . . 5
β’ (π β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
89 | | df-rex 3071 |
. . . . 5
β’
(βπ β
(β βm π)βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β βπ(π β (β βm π) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
90 | 88, 89 | sylibr 233 |
. . . 4
β’ (π β βπ β (β βm π)βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
91 | 56, 90 | jca 513 |
. . 3
β’ (π β (βπ β (β βm π)βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β (β βm π)βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
92 | | reeanv 3216 |
. . 3
β’
(βπ β
(β βm π)βπ β (β βm π)(βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β (βπ β (β βm π)βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β (β βm π)βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
93 | 91, 92 | sylibr 233 |
. 2
β’ (π β βπ β (β βm π)βπ β (β βm π)(βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
94 | | nfv 1918 |
. . . . . . . 8
β’
β²π((π β§ π β (β βm π)) β§ π β (β βm π)) |
95 | 34, 69 | nfan 1903 |
. . . . . . . 8
β’
β²π(βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
96 | 94, 95 | nfan 1903 |
. . . . . . 7
β’
β²π(((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
97 | 1 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β Fin) |
98 | 12 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β β
) |
99 | 5 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β (β βm π)) |
100 | | elmapi 8790 |
. . . . . . . . . 10
β’ (π β (β
βm π)
β π:πβΆβ) |
101 | | qssre 12889 |
. . . . . . . . . . 11
β’ β
β β |
102 | 101 | a1i 11 |
. . . . . . . . . 10
β’ (π β (β
βm π)
β β β β) |
103 | 100, 102 | fssd 6687 |
. . . . . . . . 9
β’ (π β (β
βm π)
β π:πβΆβ) |
104 | 103 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (β βm π)) β π:πβΆβ) |
105 | 104 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π:πβΆβ) |
106 | | elmapi 8790 |
. . . . . . . . 9
β’ (π β (β
βm π)
β π:πβΆβ) |
107 | 101 | a1i 11 |
. . . . . . . . 9
β’ (π β (β
βm π)
β β β β) |
108 | 106, 107 | fssd 6687 |
. . . . . . . 8
β’ (π β (β
βm π)
β π:πβΆβ) |
109 | 108 | ad2antlr 726 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π:πβΆβ) |
110 | 9 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β πΈ β
β+) |
111 | 35 | elin2d 4160 |
. . . . . . . . 9
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
112 | 111 | adantlr 714 |
. . . . . . . 8
β’
(((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
113 | 112 | adantll 713 |
. . . . . . 7
β’
(((((π β§ π β (β
βm π))
β§ π β (β
βm π))
β§ (βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
114 | 70 | elin2d 4160 |
. . . . . . . . 9
β’
((βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
115 | 114 | adantll 713 |
. . . . . . . 8
β’
(((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
116 | 115 | adantll 713 |
. . . . . . 7
β’
(((((π β§ π β (β
βm π))
β§ π β (β
βm π))
β§ (βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
117 | 96, 97, 98, 99, 105, 109, 110, 113, 116 | hoiqssbllem1 44949 |
. . . . . 6
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β Xπ β π ((πβπ)[,)(πβπ))) |
118 | | simpl 484 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β ((π β§ π β (β βm π)) β§ π β (β βm π))) |
119 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
120 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβπ) = (πβπ)) |
121 | 120 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ))))) = ((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))) |
122 | 121, 120 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π = π β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)) = (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
123 | 122 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ (π = π β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) = (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
124 | 119, 123 | eleq12d 2828 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))))) |
125 | 124 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
126 | 125 | biimpi 215 |
. . . . . . . . . 10
β’
(βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
127 | 126 | adantr 482 |
. . . . . . . . 9
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ)))) |
128 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
129 | 120 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))) = ((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))) |
130 | 120, 129 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))) = ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
131 | 130 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ (π = π β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) = (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
132 | 128, 131 | eleq12d 2828 |
. . . . . . . . . . . 12
β’ (π = π β ((πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
133 | 132 | cbvralvw 3224 |
. . . . . . . . . . 11
β’
(βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
134 | 133 | biimpi 215 |
. . . . . . . . . 10
β’
(βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
135 | 134 | adantl 483 |
. . . . . . . . 9
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) |
136 | 127, 135 | jca 513 |
. . . . . . . 8
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
137 | 136 | adantl 483 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
138 | | nfv 1918 |
. . . . . . . 8
β’
β²π(((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) |
139 | 1 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β Fin) |
140 | 12 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β β
) |
141 | 5 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π β (β βm π)) |
142 | 104 | ad2antrr 725 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π:πβΆβ) |
143 | 108 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β π:πβΆβ) |
144 | 9 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β πΈ β
β+) |
145 | 125, 111 | sylanbr 583 |
. . . . . . . . . 10
β’
((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
146 | 145 | adantlr 714 |
. . . . . . . . 9
β’
(((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
147 | 146 | adantll 713 |
. . . . . . . 8
β’
(((((π β§ π β (β
βm π))
β§ π β (β
βm π))
β§ (βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β§ π β π) β (πβπ) β (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) |
148 | 133, 114 | sylanbr 583 |
. . . . . . . . . 10
β’
((βπ β
π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
149 | 148 | adantll 713 |
. . . . . . . . 9
β’
(((βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
150 | 149 | adantll 713 |
. . . . . . . 8
β’
(((((π β§ π β (β
βm π))
β§ π β (β
βm π))
β§ (βπ β
π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β§ π β π) β (πβπ) β ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))) |
151 | 138, 139,
140, 141, 142, 143, 144, 147, 150 | hoiqssbllem2 44950 |
. . . . . . 7
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β Xπ β
π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) |
152 | 118, 137,
151 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β Xπ β
π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)) |
153 | 117, 152 | jca 513 |
. . . . 5
β’ ((((π β§ π β (β βm π)) β§ π β (β βm π)) β§ (βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ))))))))) β (π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) |
154 | 153 | ex 414 |
. . . 4
β’ (((π β§ π β (β βm π)) β§ π β (β βm π)) β ((βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β (π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)))) |
155 | 154 | reximdva 3162 |
. . 3
β’ ((π β§ π β (β βm π)) β (βπ β (β
βm π)(βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)))) |
156 | 155 | reximdva 3162 |
. 2
β’ (π β (βπ β (β βm π)βπ β (β βm π)(βπ β π (πβπ) β (β β© (((πβπ) β (πΈ / (2 Β·
(ββ(β―βπ)))))(,)(πβπ))) β§ βπ β π (πβπ) β (β β© ((πβπ)(,)((πβπ) + (πΈ / (2 Β·
(ββ(β―βπ)))))))) β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ)))) |
157 | 93, 156 | mpd 15 |
1
β’ (π β βπ β (β βm π)βπ β (β βm π)(π β Xπ β π ((πβπ)[,)(πβπ)) β§ Xπ β π ((πβπ)[,)(πβπ)) β (π(ballβ(distβ(β^βπ)))πΈ))) |