chordthmlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chordthmlem		Structured version Visualization version GIF version

Theorem chordthmlem 26764

Description: If 𝑀 is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 26754 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right angles. (Contributed by David Moews, 28-Feb-2017.)

**Hypotheses**
Ref	Expression
chordthmlem.angdef	⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
chordthmlem.A	⊢ (𝜑 → 𝐴 ∈ ℂ)
chordthmlem.B	⊢ (𝜑 → 𝐵 ∈ ℂ)
chordthmlem.Q	⊢ (𝜑 → 𝑄 ∈ ℂ)
chordthmlem.M	⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))
chordthmlem.ABequidistQ	⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))
chordthmlem.AneB	⊢ (𝜑 → 𝐴 ≠ 𝐵)
chordthmlem.QneM	⊢ (𝜑 → 𝑄 ≠ 𝑀)

**Assertion**
Ref	Expression
chordthmlem	⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)})

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝐵,𝑦 𝑥,𝑀,𝑦 𝑥,𝑄,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦) 𝐹(𝑥,𝑦)

**Proof of Theorem chordthmlem**
Step	Hyp	Ref	Expression
1		negpitopissre 26471	. . . . . 6 ⊢ (-π(,]π) ⊆ ℝ
2		chordthmlem.angdef	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))
3		chordthmlem.Q	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ ℂ)
4		chordthmlem.M	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 = ((𝐴 + 𝐵) / 2))
5		chordthmlem.A	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℂ)
6		chordthmlem.B	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
7	5, 6	addcld 11126	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
8	7	halfcld 12361	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℂ)
9	4, 8	eqeltrd 2831	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	3, 9	subcld 11467	. . . . . . 7 ⊢ (𝜑 → (𝑄 − 𝑀) ∈ ℂ)
11		chordthmlem.QneM	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ≠ 𝑀)
12	3, 9, 11	subne0d 11476	. . . . . . 7 ⊢ (𝜑 → (𝑄 − 𝑀) ≠ 0)
13	6, 9	subcld 11467	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑀) ∈ ℂ)
14	4	oveq1d 7356	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · 2) = (((𝐴 + 𝐵) / 2) · 2))
15	9	times2d 12360	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · 2) = (𝑀 + 𝑀))
16		2cnd 12198	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
17		2ne0 12224	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ≠ 0)
19	7, 16, 18	divcan1d 11893	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + 𝐵) / 2) · 2) = (𝐴 + 𝐵))
20	14, 15, 19	3eqtr3d 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 + 𝑀) = (𝐴 + 𝐵))
21		chordthmlem.AneB	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
22	5, 6, 6, 21	addneintr2d 11316	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐵 + 𝐵))
23	20, 22	eqnetrd 2995	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 + 𝑀) ≠ (𝐵 + 𝐵))
24	23	neneqd 2933	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑀 + 𝑀) = (𝐵 + 𝐵))
25		oveq12 7350	. . . . . . . . . . . 12 ⊢ ((𝑀 = 𝐵 ∧ 𝑀 = 𝐵) → (𝑀 + 𝑀) = (𝐵 + 𝐵))
26	25	anidms 566	. . . . . . . . . . 11 ⊢ (𝑀 = 𝐵 → (𝑀 + 𝑀) = (𝐵 + 𝐵))
27	24, 26	nsyl 140	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝑀 = 𝐵)
28	27	neqned 2935	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≠ 𝐵)
29	28	necomd 2983	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝑀)
30	6, 9, 29	subne0d 11476	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑀) ≠ 0)
31	2, 10, 12, 13, 30	angcld 26737	. . . . . 6 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ (-π(,]π))
32	1, 31	sselid 3927	. . . . 5 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ ℝ)
33	32	recnd 11135	. . . 4 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ ℂ)
34	33	coscld 16035	. . 3 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) ∈ ℂ)
35	6, 9	negsubdi2d 11483	. . . . . . 7 ⊢ (𝜑 → -(𝐵 − 𝑀) = (𝑀 − 𝐵))
36	9, 9, 5, 6	addsubeq4d 11518	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 + 𝑀) = (𝐴 + 𝐵) ↔ (𝐴 − 𝑀) = (𝑀 − 𝐵)))
37	20, 36	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑀) = (𝑀 − 𝐵))
38	35, 37	eqtr4d 2769	. . . . . 6 ⊢ (𝜑 → -(𝐵 − 𝑀) = (𝐴 − 𝑀))
39	38	oveq2d 7357	. . . . 5 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀)) = ((𝑄 − 𝑀)𝐹(𝐴 − 𝑀)))
40	39	fveq2d 6821	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀))) = (cos‘((𝑄 − 𝑀)𝐹(𝐴 − 𝑀))))
41	2, 10, 12, 13, 30	cosangneg2d 26739	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀))) = -(cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
42	5, 5, 6, 21	addneintrd 11315	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 𝐴) ≠ (𝐴 + 𝐵))
43	42, 20	neeqtrrd 3002	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + 𝐴) ≠ (𝑀 + 𝑀))
44	43	necomd 2983	. . . . . . . 8 ⊢ (𝜑 → (𝑀 + 𝑀) ≠ (𝐴 + 𝐴))
45	44	neneqd 2933	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑀 + 𝑀) = (𝐴 + 𝐴))
46		oveq12 7350	. . . . . . . 8 ⊢ ((𝑀 = 𝐴 ∧ 𝑀 = 𝐴) → (𝑀 + 𝑀) = (𝐴 + 𝐴))
47	46	anidms 566	. . . . . . 7 ⊢ (𝑀 = 𝐴 → (𝑀 + 𝑀) = (𝐴 + 𝐴))
48	45, 47	nsyl 140	. . . . . 6 ⊢ (𝜑 → ¬ 𝑀 = 𝐴)
49	48	neqned 2935	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝐴)
50		eqidd 2732	. . . . 5 ⊢ (𝜑 → (abs‘(𝑄 − 𝑀)) = (abs‘(𝑄 − 𝑀)))
51	5, 9	subcld 11467	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑀) ∈ ℂ)
52	51	absnegd 15354	. . . . . 6 ⊢ (𝜑 → (abs‘-(𝐴 − 𝑀)) = (abs‘(𝐴 − 𝑀)))
53	5, 9	negsubdi2d 11483	. . . . . . 7 ⊢ (𝜑 → -(𝐴 − 𝑀) = (𝑀 − 𝐴))
54	53	fveq2d 6821	. . . . . 6 ⊢ (𝜑 → (abs‘-(𝐴 − 𝑀)) = (abs‘(𝑀 − 𝐴)))
55	37	fveq2d 6821	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴 − 𝑀)) = (abs‘(𝑀 − 𝐵)))
56	52, 54, 55	3eqtr3d 2774	. . . . 5 ⊢ (𝜑 → (abs‘(𝑀 − 𝐴)) = (abs‘(𝑀 − 𝐵)))
57		chordthmlem.ABequidistQ	. . . . 5 ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))
58	2, 3, 9, 5, 3, 9, 6, 11, 49, 11, 28, 50, 56, 57	ssscongptld 26754	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐴 − 𝑀))) = (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
59	40, 41, 58	3eqtr3rd 2775	. . 3 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = -(cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
60	34, 59	eqnegad 11838	. 2 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = 0)
61		coseq0negpitopi 26434	. . 3 ⊢ (((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ (-π(,]π) → ((cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = 0 ↔ ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)}))
62	31, 61	syl 17	. 2 ⊢ (𝜑 → ((cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = 0 ↔ ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)}))
63	60, 62	mpbid 232	1 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ {(π / 2), -(π / 2)})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∖ cdif 3894 {csn 4571 {cpr 4573 ‘cfv 6476 (class class class)co 7341 ∈ cmpo 7343 ℂcc 10999 ℝcr 11000 0cc0 11001 + caddc 11004 · cmul 11006 − cmin 11339 -cneg 11340 / cdiv 11769 2c2 12175 (,]cioc 13241 ℑcim 15000 abscabs 15136 cosccos 15966 πcpi 15968 logclog 26485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-inf2 9526 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-pre-sup 11079 ax-addf 11080

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-se 5565 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-isom 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-er 8617 df-map 8747 df-pm 8748 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-fi 9290 df-sup 9321 df-inf 9322 df-oi 9391 df-card 9827 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-div 11770 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-7 12188 df-8 12189 df-9 12190 df-n0 12377 df-z 12464 df-dec 12584 df-uz 12728 df-q 12842 df-rp 12886 df-xneg 13006 df-xadd 13007 df-xmul 13008 df-ioo 13244 df-ioc 13245 df-ico 13246 df-icc 13247 df-fz 13403 df-fzo 13550 df-fl 13691 df-mod 13769 df-seq 13904 df-exp 13964 df-fac 14176 df-bc 14205 df-hash 14233 df-shft 14969 df-cj 15001 df-re 15002 df-im 15003 df-sqrt 15137 df-abs 15138 df-limsup 15373 df-clim 15390 df-rlim 15391 df-sum 15589 df-ef 15969 df-sin 15971 df-cos 15972 df-pi 15974 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-starv 17171 df-sca 17172 df-vsca 17173 df-ip 17174 df-tset 17175 df-ple 17176 df-ds 17178 df-unif 17179 df-hom 17180 df-cco 17181 df-rest 17321 df-topn 17322 df-0g 17340 df-gsum 17341 df-topgen 17342 df-pt 17343 df-prds 17346 df-xrs 17401 df-qtop 17406 df-imas 17407 df-xps 17409 df-mre 17483 df-mrc 17484 df-acs 17486 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-mulg 18976 df-cntz 19224 df-cmn 19689 df-psmet 21278 df-xmet 21279 df-met 21280 df-bl 21281 df-mopn 21282 df-fbas 21283 df-fg 21284 df-cnfld 21287 df-top 22804 df-topon 22821 df-topsp 22843 df-bases 22856 df-cld 22929 df-ntr 22930 df-cls 22931 df-nei 23008 df-lp 23046 df-perf 23047 df-cn 23137 df-cnp 23138 df-haus 23225 df-tx 23472 df-hmeo 23665 df-fil 23756 df-fm 23848 df-flim 23849 df-flf 23850 df-xms 24230 df-ms 24231 df-tms 24232 df-cncf 24793 df-limc 25789 df-dv 25790 df-log 26487

This theorem is referenced by: chordthmlem2 26765

W3C validator