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 26789

Description: If 𝑀 is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 26779 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 26496	. . . . . 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 11142	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
8	7	halfcld 12377	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴 + 𝐵) / 2) ∈ ℂ)
9	4, 8	eqeltrd 2833	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	3, 9	subcld 11483	. . . . . . 7 ⊢ (𝜑 → (𝑄 − 𝑀) ∈ ℂ)
11		chordthmlem.QneM	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ≠ 𝑀)
12	3, 9, 11	subne0d 11492	. . . . . . 7 ⊢ (𝜑 → (𝑄 − 𝑀) ≠ 0)
13	6, 9	subcld 11483	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑀) ∈ ℂ)
14	4	oveq1d 7370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · 2) = (((𝐴 + 𝐵) / 2) · 2))
15	9	times2d 12376	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 · 2) = (𝑀 + 𝑀))
16		2cnd 12214	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
17		2ne0 12240	. . . . . . . . . . . . . . . 16 ⊢ 2 ≠ 0
18	17	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ≠ 0)
19	7, 16, 18	divcan1d 11909	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 + 𝐵) / 2) · 2) = (𝐴 + 𝐵))
20	14, 15, 19	3eqtr3d 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑀 + 𝑀) = (𝐴 + 𝐵))
21		chordthmlem.AneB	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
22	5, 6, 6, 21	addneintr2d 11332	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 𝐵) ≠ (𝐵 + 𝐵))
23	20, 22	eqnetrd 2996	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑀 + 𝑀) ≠ (𝐵 + 𝐵))
24	23	neneqd 2934	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝑀 + 𝑀) = (𝐵 + 𝐵))
25		oveq12 7364	. . . . . . . . . . . 12 ⊢ ((𝑀 = 𝐵 ∧ 𝑀 = 𝐵) → (𝑀 + 𝑀) = (𝐵 + 𝐵))
26	25	anidms 566	. . . . . . . . . . 11 ⊢ (𝑀 = 𝐵 → (𝑀 + 𝑀) = (𝐵 + 𝐵))
27	24, 26	nsyl 140	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝑀 = 𝐵)
28	27	neqned 2936	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≠ 𝐵)
29	28	necomd 2984	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ≠ 𝑀)
30	6, 9, 29	subne0d 11492	. . . . . . 7 ⊢ (𝜑 → (𝐵 − 𝑀) ≠ 0)
31	2, 10, 12, 13, 30	angcld 26762	. . . . . 6 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ (-π(,]π))
32	1, 31	sselid 3928	. . . . 5 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ ℝ)
33	32	recnd 11151	. . . 4 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹(𝐵 − 𝑀)) ∈ ℂ)
34	33	coscld 16047	. . 3 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) ∈ ℂ)
35	6, 9	negsubdi2d 11499	. . . . . . 7 ⊢ (𝜑 → -(𝐵 − 𝑀) = (𝑀 − 𝐵))
36	9, 9, 5, 6	addsubeq4d 11534	. . . . . . . 8 ⊢ (𝜑 → ((𝑀 + 𝑀) = (𝐴 + 𝐵) ↔ (𝐴 − 𝑀) = (𝑀 − 𝐵)))
37	20, 36	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑀) = (𝑀 − 𝐵))
38	35, 37	eqtr4d 2771	. . . . . 6 ⊢ (𝜑 → -(𝐵 − 𝑀) = (𝐴 − 𝑀))
39	38	oveq2d 7371	. . . . 5 ⊢ (𝜑 → ((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀)) = ((𝑄 − 𝑀)𝐹(𝐴 − 𝑀)))
40	39	fveq2d 6835	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀))) = (cos‘((𝑄 − 𝑀)𝐹(𝐴 − 𝑀))))
41	2, 10, 12, 13, 30	cosangneg2d 26764	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹-(𝐵 − 𝑀))) = -(cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
42	5, 5, 6, 21	addneintrd 11331	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 + 𝐴) ≠ (𝐴 + 𝐵))
43	42, 20	neeqtrrd 3003	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 + 𝐴) ≠ (𝑀 + 𝑀))
44	43	necomd 2984	. . . . . . . 8 ⊢ (𝜑 → (𝑀 + 𝑀) ≠ (𝐴 + 𝐴))
45	44	neneqd 2934	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑀 + 𝑀) = (𝐴 + 𝐴))
46		oveq12 7364	. . . . . . . 8 ⊢ ((𝑀 = 𝐴 ∧ 𝑀 = 𝐴) → (𝑀 + 𝑀) = (𝐴 + 𝐴))
47	46	anidms 566	. . . . . . 7 ⊢ (𝑀 = 𝐴 → (𝑀 + 𝑀) = (𝐴 + 𝐴))
48	45, 47	nsyl 140	. . . . . 6 ⊢ (𝜑 → ¬ 𝑀 = 𝐴)
49	48	neqned 2936	. . . . 5 ⊢ (𝜑 → 𝑀 ≠ 𝐴)
50		eqidd 2734	. . . . 5 ⊢ (𝜑 → (abs‘(𝑄 − 𝑀)) = (abs‘(𝑄 − 𝑀)))
51	5, 9	subcld 11483	. . . . . . 7 ⊢ (𝜑 → (𝐴 − 𝑀) ∈ ℂ)
52	51	absnegd 15366	. . . . . 6 ⊢ (𝜑 → (abs‘-(𝐴 − 𝑀)) = (abs‘(𝐴 − 𝑀)))
53	5, 9	negsubdi2d 11499	. . . . . . 7 ⊢ (𝜑 → -(𝐴 − 𝑀) = (𝑀 − 𝐴))
54	53	fveq2d 6835	. . . . . 6 ⊢ (𝜑 → (abs‘-(𝐴 − 𝑀)) = (abs‘(𝑀 − 𝐴)))
55	37	fveq2d 6835	. . . . . 6 ⊢ (𝜑 → (abs‘(𝐴 − 𝑀)) = (abs‘(𝑀 − 𝐵)))
56	52, 54, 55	3eqtr3d 2776	. . . . 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 26779	. . . 4 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐴 − 𝑀))) = (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
59	40, 41, 58	3eqtr3rd 2777	. . 3 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = -(cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))))
60	34, 59	eqnegad 11854	. 2 ⊢ (𝜑 → (cos‘((𝑄 − 𝑀)𝐹(𝐵 − 𝑀))) = 0)
61		coseq0negpitopi 26459	. . 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 2113 ≠ wne 2929 ∖ cdif 3895 {csn 4577 {cpr 4579 ‘cfv 6489 (class class class)co 7355 ∈ cmpo 7357 ℂcc 11015 ℝcr 11016 0cc0 11017 + caddc 11020 · cmul 11022 − cmin 11355 -cneg 11356 / cdiv 11785 2c2 12191 (,]cioc 13253 ℑcim 15012 abscabs 15148 cosccos 15978 πcpi 15980 logclog 26510

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 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-inf2 9542 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095 ax-addf 11096

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 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-iin 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-of 7619 df-om 7806 df-1st 7930 df-2nd 7931 df-supp 8100 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-er 8631 df-map 8761 df-pm 8762 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9257 df-fi 9306 df-sup 9337 df-inf 9338 df-oi 9407 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-6 12203 df-7 12204 df-8 12205 df-9 12206 df-n0 12393 df-z 12480 df-dec 12599 df-uz 12743 df-q 12853 df-rp 12897 df-xneg 13017 df-xadd 13018 df-xmul 13019 df-ioo 13256 df-ioc 13257 df-ico 13258 df-icc 13259 df-fz 13415 df-fzo 13562 df-fl 13703 df-mod 13781 df-seq 13916 df-exp 13976 df-fac 14188 df-bc 14217 df-hash 14245 df-shft 14981 df-cj 15013 df-re 15014 df-im 15015 df-sqrt 15149 df-abs 15150 df-limsup 15385 df-clim 15402 df-rlim 15403 df-sum 15601 df-ef 15981 df-sin 15983 df-cos 15984 df-pi 15986 df-struct 17065 df-sets 17082 df-slot 17100 df-ndx 17112 df-base 17128 df-ress 17149 df-plusg 17181 df-mulr 17182 df-starv 17183 df-sca 17184 df-vsca 17185 df-ip 17186 df-tset 17187 df-ple 17188 df-ds 17190 df-unif 17191 df-hom 17192 df-cco 17193 df-rest 17333 df-topn 17334 df-0g 17352 df-gsum 17353 df-topgen 17354 df-pt 17355 df-prds 17358 df-xrs 17414 df-qtop 17419 df-imas 17420 df-xps 17422 df-mre 17496 df-mrc 17497 df-acs 17499 df-mgm 18556 df-sgrp 18635 df-mnd 18651 df-submnd 18700 df-mulg 18989 df-cntz 19237 df-cmn 19702 df-psmet 21292 df-xmet 21293 df-met 21294 df-bl 21295 df-mopn 21296 df-fbas 21297 df-fg 21298 df-cnfld 21301 df-top 22829 df-topon 22846 df-topsp 22868 df-bases 22881 df-cld 22954 df-ntr 22955 df-cls 22956 df-nei 23033 df-lp 23071 df-perf 23072 df-cn 23162 df-cnp 23163 df-haus 23250 df-tx 23497 df-hmeo 23690 df-fil 23781 df-fm 23873 df-flim 23874 df-flf 23875 df-xms 24255 df-ms 24256 df-tms 24257 df-cncf 24818 df-limc 25814 df-dv 25815 df-log 26512

This theorem is referenced by: chordthmlem2 26790

W3C validator