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