Step |
Hyp |
Ref |
Expression |
1 |
|
chordthmlem3.A |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
2 |
|
chordthmlem3.B |
⊢ ( 𝜑 → 𝐵 ∈ ℂ ) |
3 |
|
chordthmlem3.Q |
⊢ ( 𝜑 → 𝑄 ∈ ℂ ) |
4 |
|
chordthmlem3.X |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
5 |
|
chordthmlem3.M |
⊢ ( 𝜑 → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) ) |
6 |
|
chordthmlem3.P |
⊢ ( 𝜑 → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ) |
7 |
|
chordthmlem3.ABequidistQ |
⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) ) |
8 |
1 2
|
addcld |
⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ ) |
9 |
8
|
halfcld |
⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ) |
10 |
5 9
|
eqeltrd |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
11 |
3 10
|
subcld |
⊢ ( 𝜑 → ( 𝑄 − 𝑀 ) ∈ ℂ ) |
12 |
11
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − 𝑀 ) ) ∈ ℝ ) |
13 |
12
|
recnd |
⊢ ( 𝜑 → ( abs ‘ ( 𝑄 − 𝑀 ) ) ∈ ℂ ) |
14 |
13
|
sqcld |
⊢ ( 𝜑 → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ∈ ℂ ) |
15 |
14
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ∈ ℂ ) |
16 |
15
|
addid1d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + 0 ) = ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ) |
17 |
4
|
recnd |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
18 |
17 1
|
mulcld |
⊢ ( 𝜑 → ( 𝑋 · 𝐴 ) ∈ ℂ ) |
19 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
20 |
19 17
|
subcld |
⊢ ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ ) |
21 |
20 2
|
mulcld |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · 𝐵 ) ∈ ℂ ) |
22 |
18 21
|
addcld |
⊢ ( 𝜑 → ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ∈ ℂ ) |
23 |
6 22
|
eqeltrd |
⊢ ( 𝜑 → 𝑃 ∈ ℂ ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑃 ∈ ℂ ) |
25 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑃 = 𝑀 ) |
26 |
24 25
|
subeq0bd |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( 𝑃 − 𝑀 ) = 0 ) |
27 |
26
|
abs00bd |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑀 ) ) = 0 ) |
28 |
27
|
sq0id |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) = 0 ) |
29 |
28
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + 0 ) ) |
30 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → 𝑄 ∈ ℂ ) |
31 |
30 24
|
abssubd |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑃 ) ) = ( abs ‘ ( 𝑃 − 𝑄 ) ) ) |
32 |
25
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( 𝑄 − 𝑃 ) = ( 𝑄 − 𝑀 ) ) |
33 |
32
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑃 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) ) ) |
34 |
31 33
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) ) ) |
35 |
34
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) ) |
36 |
16 29 35
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ 𝑃 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |
37 |
23 10
|
subcld |
⊢ ( 𝜑 → ( 𝑃 − 𝑀 ) ∈ ℂ ) |
38 |
37
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − 𝑀 ) ) ∈ ℝ ) |
39 |
38
|
recnd |
⊢ ( 𝜑 → ( abs ‘ ( 𝑃 − 𝑀 ) ) ∈ ℂ ) |
40 |
39
|
sqcld |
⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ∈ ℂ ) |
41 |
40
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ∈ ℂ ) |
42 |
41
|
addid2d |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 0 + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) |
43 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → 𝑄 ∈ ℂ ) |
44 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → 𝑄 = 𝑀 ) |
45 |
43 44
|
subeq0bd |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 𝑄 − 𝑀 ) = 0 ) |
46 |
45
|
abs00bd |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( abs ‘ ( 𝑄 − 𝑀 ) ) = 0 ) |
47 |
46
|
sq0id |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) = 0 ) |
48 |
47
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) = ( 0 + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |
49 |
44
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( 𝑃 − 𝑄 ) = ( 𝑃 − 𝑀 ) ) |
50 |
49
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑃 − 𝑀 ) ) ) |
51 |
50
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) |
52 |
42 48 51
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ 𝑄 = 𝑀 ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |
53 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 ∈ ℂ ) |
54 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑄 ∈ ℂ ) |
55 |
10
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑀 ∈ ℂ ) |
56 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 ≠ 𝑀 ) |
57 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑄 ≠ 𝑀 ) |
58 |
|
eqid |
⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) |
59 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝐴 ∈ ℂ ) |
60 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝐵 ∈ ℂ ) |
61 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑋 ∈ ℝ ) |
62 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑀 = ( ( 𝐴 + 𝐵 ) / 2 ) ) |
63 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → 𝑃 = ( ( 𝑋 · 𝐴 ) + ( ( 1 − 𝑋 ) · 𝐵 ) ) ) |
64 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( abs ‘ ( 𝐴 − 𝑄 ) ) = ( abs ‘ ( 𝐵 − 𝑄 ) ) ) |
65 |
58 59 60 54 61 62 63 64 56 57
|
chordthmlem2 |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) |
66 |
|
eqid |
⊢ ( abs ‘ ( 𝑄 − 𝑀 ) ) = ( abs ‘ ( 𝑄 − 𝑀 ) ) |
67 |
|
eqid |
⊢ ( abs ‘ ( 𝑃 − 𝑀 ) ) = ( abs ‘ ( 𝑃 − 𝑀 ) ) |
68 |
|
eqid |
⊢ ( abs ‘ ( 𝑃 − 𝑄 ) ) = ( abs ‘ ( 𝑃 − 𝑄 ) ) |
69 |
|
eqid |
⊢ ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) = ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) |
70 |
58 66 67 68 69
|
pythag |
⊢ ( ( ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ∧ ( ( 𝑄 − 𝑀 ) ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℑ ‘ ( log ‘ ( 𝑦 / 𝑥 ) ) ) ) ( 𝑃 − 𝑀 ) ) ∈ { ( π / 2 ) , - ( π / 2 ) } ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |
71 |
53 54 55 56 57 65 70
|
syl321anc |
⊢ ( ( 𝜑 ∧ ( 𝑃 ≠ 𝑀 ∧ 𝑄 ≠ 𝑀 ) ) → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |
72 |
36 52 71
|
pm2.61da2ne |
⊢ ( 𝜑 → ( ( abs ‘ ( 𝑃 − 𝑄 ) ) ↑ 2 ) = ( ( ( abs ‘ ( 𝑄 − 𝑀 ) ) ↑ 2 ) + ( ( abs ‘ ( 𝑃 − 𝑀 ) ) ↑ 2 ) ) ) |