![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > chordthmlem2 | Unicode version |
Description: If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem 20634, where P = B, and using angrtmuld 20611 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.) |
Ref | Expression |
---|---|
chordthmlem2.angdef |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.A |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.B |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.Q |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.X |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.M |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.P |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.ABequidistQ |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.PneM |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
chordthmlem2.QneM |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
chordthmlem2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chordthmlem2.angdef |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | chordthmlem2.A |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | chordthmlem2.B |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | chordthmlem2.Q |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | chordthmlem2.M |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | chordthmlem2.ABequidistQ |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 2re 10033 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() | |
8 | 7 | a1i 11 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 2ne0 10047 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() | |
10 | 9 | a1i 11 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 8, 10 | rereccld 9805 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | chordthmlem2.X |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 11, 12 | resubcld 9429 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | recnd 9078 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 3, 2 | subcld 9375 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 11 | recnd 9078 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 12 | recnd 9078 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 16, 17, 15 | subdird 9454 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 2cn 10034 |
. . . . . . . . . . . . . . 15
![]() ![]() ![]() ![]() | |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 3, 20, 10 | divcan4d 9760 |
. . . . . . . . . . . . 13
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 3 | times2d 10175 |
. . . . . . . . . . . . . 14
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | 22 | oveq1d 6063 |
. . . . . . . . . . . . 13
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 21, 23 | eqtr3d 2446 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24, 5 | oveq12d 6066 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | 3, 3 | addcld 9071 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | 2, 3 | addcld 9071 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 26, 27, 20, 10 | divsubdird 9793 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 3, 2, 3 | pnpcan2d 9413 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | 29 | oveq1d 6063 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 25, 28, 30 | 3eqtr2d 2450 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 15, 20, 10 | divrec2d 9758 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 31, 32 | eqtrd 2444 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | chordthmlem2.P |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
35 | 17, 2 | mulcld 9072 |
. . . . . . . . . . . . 13
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | ax-1cn 9012 |
. . . . . . . . . . . . . . . 16
![]() ![]() ![]() ![]() | |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . 15
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 37, 17 | subcld 9375 |
. . . . . . . . . . . . . 14
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 38, 3 | mulcld 9072 |
. . . . . . . . . . . . 13
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 35, 39 | addcld 9071 |
. . . . . . . . . . . 12
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 34, 40 | eqeltrd 2486 |
. . . . . . . . . . 11
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 2, 41, 3, 17 | affineequiv 20628 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 34, 42 | mpbid 202 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | 33, 43 | oveq12d 6066 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 27 | halfcld 10176 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | 5, 45 | eqeltrd 2486 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
47 | 3, 46, 41 | nnncan1d 9409 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
48 | 18, 44, 47 | 3eqtr2rd 2451 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | chordthmlem2.PneM |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
50 | 41, 46, 49 | subne0d 9384 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
51 | 48, 50 | eqnetrrd 2595 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 14, 15, 51 | mulne0bbd 9640 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
53 | 3, 2, 52 | subne0ad 9386 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
54 | 53 | necomd 2658 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
55 | chordthmlem2.QneM |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
56 | 1, 2, 3, 4, 5, 6, 54, 55 | chordthmlem 20634 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
57 | 4, 46 | subcld 9375 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
58 | 41, 46 | subcld 9375 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
59 | 3, 46 | subcld 9375 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
60 | 4, 46, 55 | subne0d 9384 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
61 | 20, 10 | recne0d 9748 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
62 | 16, 15, 61, 52 | mulne0d 9638 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
63 | 33, 62 | eqnetrd 2593 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
64 | 33, 48 | oveq12d 6066 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
65 | 14, 15, 51 | mulne0bad 9639 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
66 | 16, 14, 15, 65, 52 | divcan5rd 9781 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
67 | 64, 66 | eqtrd 2444 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
68 | 11, 13, 65 | redivcld 9806 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
69 | 67, 68 | eqeltrd 2486 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
70 | 1, 57, 58, 59, 60, 50, 63, 69 | angrtmuld 20611 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
71 | 56, 70 | mpbird 224 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: chordthmlem3 20636 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-rep 4288 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668 ax-inf2 7560 ax-cnex 9010 ax-resscn 9011 ax-1cn 9012 ax-icn 9013 ax-addcl 9014 ax-addrcl 9015 ax-mulcl 9016 ax-mulrcl 9017 ax-mulcom 9018 ax-addass 9019 ax-mulass 9020 ax-distr 9021 ax-i2m1 9022 ax-1ne0 9023 ax-1rid 9024 ax-rnegex 9025 ax-rrecex 9026 ax-cnre 9027 ax-pre-lttri 9028 ax-pre-lttrn 9029 ax-pre-ltadd 9030 ax-pre-mulgt0 9031 ax-pre-sup 9032 ax-addf 9033 ax-mulf 9034 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-nel 2578 df-ral 2679 df-rex 2680 df-reu 2681 df-rmo 2682 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-pss 3304 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-tp 3790 df-op 3791 df-uni 3984 df-int 4019 df-iun 4063 df-iin 4064 df-br 4181 df-opab 4235 df-mpt 4236 df-tr 4271 df-eprel 4462 df-id 4466 df-po 4471 df-so 4472 df-fr 4509 df-se 4510 df-we 4511 df-ord 4552 df-on 4553 df-lim 4554 df-suc 4555 df-om 4813 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-isom 5430 df-ov 6051 df-oprab 6052 df-mpt2 6053 df-of 6272 df-1st 6316 df-2nd 6317 df-riota 6516 df-recs 6600 df-rdg 6635 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6872 df-map 6987 df-pm 6988 df-ixp 7031 df-en 7077 df-dom 7078 df-sdom 7079 df-fin 7080 df-fi 7382 df-sup 7412 df-oi 7443 df-card 7790 df-cda 8012 df-pnf 9086 df-mnf 9087 df-xr 9088 df-ltxr 9089 df-le 9090 df-sub 9257 df-neg 9258 df-div 9642 df-nn 9965 df-2 10022 df-3 10023 df-4 10024 df-5 10025 df-6 10026 df-7 10027 df-8 10028 df-9 10029 df-10 10030 df-n0 10186 df-z 10247 df-dec 10347 df-uz 10453 df-q 10539 df-rp 10577 df-xneg 10674 df-xadd 10675 df-xmul 10676 df-ioo 10884 df-ioc 10885 df-ico 10886 df-icc 10887 df-fz 11008 df-fzo 11099 df-fl 11165 df-mod 11214 df-seq 11287 df-exp 11346 df-fac 11530 df-bc 11557 df-hash 11582 df-shft 11845 df-cj 11867 df-re 11868 df-im 11869 df-sqr 12003 df-abs 12004 df-limsup 12228 df-clim 12245 df-rlim 12246 df-sum 12443 df-ef 12633 df-sin 12635 df-cos 12636 df-pi 12638 df-struct 13434 df-ndx 13435 df-slot 13436 df-base 13437 df-sets 13438 df-ress 13439 df-plusg 13505 df-mulr 13506 df-starv 13507 df-sca 13508 df-vsca 13509 df-tset 13511 df-ple 13512 df-ds 13514 df-unif 13515 df-hom 13516 df-cco 13517 df-rest 13613 df-topn 13614 df-topgen 13630 df-pt 13631 df-prds 13634 df-xrs 13689 df-0g 13690 df-gsum 13691 df-qtop 13696 df-imas 13697 df-xps 13699 df-mre 13774 df-mrc 13775 df-acs 13777 df-mnd 14653 df-submnd 14702 df-mulg 14778 df-cntz 15079 df-cmn 15377 df-psmet 16657 df-xmet 16658 df-met 16659 df-bl 16660 df-mopn 16661 df-fbas 16662 df-fg 16663 df-cnfld 16667 df-top 16926 df-bases 16928 df-topon 16929 df-topsp 16930 df-cld 17046 df-ntr 17047 df-cls 17048 df-nei 17125 df-lp 17163 df-perf 17164 df-cn 17253 df-cnp 17254 df-haus 17341 df-tx 17555 df-hmeo 17748 df-fil 17839 df-fm 17931 df-flim 17932 df-flf 17933 df-xms 18311 df-ms 18312 df-tms 18313 df-cncf 18869 df-limc 19714 df-dv 19715 df-log 20415 |
Copyright terms: Public domain | W3C validator |