Description: Property of the midpoint. (Contributed by Thierry Arnoux, 1-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismid.p | |
|
ismid.d | |
||
ismid.i | |
||
ismid.g | |
||
ismid.1 | |
||
midcl.1 | |
||
midcl.2 | |
||
ismidb.s | |
||
ismidb.m | |
||
Assertion | ismidb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismid.p | |
|
2 | ismid.d | |
|
3 | ismid.i | |
|
4 | ismid.g | |
|
5 | ismid.1 | |
|
6 | midcl.1 | |
|
7 | midcl.2 | |
|
8 | ismidb.s | |
|
9 | ismidb.m | |
|
10 | eqid | |
|
11 | 1 2 3 10 4 8 6 7 5 | mideu | |
12 | fveq2 | |
|
13 | 12 | fveq1d | |
14 | 13 | eqeq2d | |
15 | 14 | riota2 | |
16 | 9 11 15 | syl2anc | |
17 | df-mid | |
|
18 | fveq2 | |
|
19 | 18 1 | eqtr4di | |
20 | fveq2 | |
|
21 | 20 8 | eqtr4di | |
22 | 21 | fveq1d | |
23 | 22 | fveq1d | |
24 | 23 | eqeq2d | |
25 | 19 24 | riotaeqbidv | |
26 | 19 19 25 | mpoeq123dv | |
27 | 4 | elexd | |
28 | 1 | fvexi | |
29 | 28 28 | mpoex | |
30 | 29 | a1i | |
31 | 17 26 27 30 | fvmptd3 | |
32 | simprr | |
|
33 | simprl | |
|
34 | 33 | fveq2d | |
35 | 32 34 | eqeq12d | |
36 | 35 | riotabidv | |
37 | riotacl | |
|
38 | 11 37 | syl | |
39 | 31 36 6 7 38 | ovmpod | |
40 | 39 | eqeq1d | |
41 | 16 40 | bitr4d | |