| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pjhth.1 |
⊢ 𝐻 ∈ Cℋ |
| 2 |
|
pjhth.2 |
⊢ ( 𝜑 → 𝐴 ∈ ℋ ) |
| 3 |
|
pjhth.3 |
⊢ ( 𝜑 → 𝐵 ∈ 𝐻 ) |
| 4 |
|
pjhth.4 |
⊢ ( 𝜑 → 𝐶 ∈ 𝐻 ) |
| 5 |
|
pjhth.5 |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ) |
| 6 |
|
pjhth.6 |
⊢ 𝑇 = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 7 |
1
|
cheli |
⊢ ( 𝐵 ∈ 𝐻 → 𝐵 ∈ ℋ ) |
| 8 |
3 7
|
syl |
⊢ ( 𝜑 → 𝐵 ∈ ℋ ) |
| 9 |
|
hvsubcl |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) |
| 10 |
2 8 9
|
syl2anc |
⊢ ( 𝜑 → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) |
| 11 |
1
|
cheli |
⊢ ( 𝐶 ∈ 𝐻 → 𝐶 ∈ ℋ ) |
| 12 |
4 11
|
syl |
⊢ ( 𝜑 → 𝐶 ∈ ℋ ) |
| 13 |
|
hicl |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ∈ ℂ ) |
| 14 |
10 12 13
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ∈ ℂ ) |
| 15 |
14
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ∈ ℝ ) |
| 16 |
15
|
recnd |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ∈ ℂ ) |
| 17 |
15
|
resqcld |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ∈ ℝ ) |
| 18 |
17
|
renegcld |
⊢ ( 𝜑 → - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ∈ ℝ ) |
| 19 |
|
hiidrcl |
⊢ ( 𝐶 ∈ ℋ → ( 𝐶 ·ih 𝐶 ) ∈ ℝ ) |
| 20 |
12 19
|
syl |
⊢ ( 𝜑 → ( 𝐶 ·ih 𝐶 ) ∈ ℝ ) |
| 21 |
|
2re |
⊢ 2 ∈ ℝ |
| 22 |
|
readdcl |
⊢ ( ( ( 𝐶 ·ih 𝐶 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℝ ) |
| 23 |
20 21 22
|
sylancl |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℝ ) |
| 24 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
| 25 |
|
peano2re |
⊢ ( ( 𝐶 ·ih 𝐶 ) ∈ ℝ → ( ( 𝐶 ·ih 𝐶 ) + 1 ) ∈ ℝ ) |
| 26 |
20 25
|
syl |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) ∈ ℝ ) |
| 27 |
|
hiidge0 |
⊢ ( 𝐶 ∈ ℋ → 0 ≤ ( 𝐶 ·ih 𝐶 ) ) |
| 28 |
12 27
|
syl |
⊢ ( 𝜑 → 0 ≤ ( 𝐶 ·ih 𝐶 ) ) |
| 29 |
20
|
ltp1d |
⊢ ( 𝜑 → ( 𝐶 ·ih 𝐶 ) < ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 30 |
24 20 26 28 29
|
lelttrd |
⊢ ( 𝜑 → 0 < ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 31 |
26
|
ltp1d |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) < ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) ) |
| 32 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 33 |
32
|
oveq2i |
⊢ ( ( 𝐶 ·ih 𝐶 ) + 2 ) = ( ( 𝐶 ·ih 𝐶 ) + ( 1 + 1 ) ) |
| 34 |
20
|
recnd |
⊢ ( 𝜑 → ( 𝐶 ·ih 𝐶 ) ∈ ℂ ) |
| 35 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 36 |
|
addass |
⊢ ( ( ( 𝐶 ·ih 𝐶 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) = ( ( 𝐶 ·ih 𝐶 ) + ( 1 + 1 ) ) ) |
| 37 |
35 35 36
|
mp3an23 |
⊢ ( ( 𝐶 ·ih 𝐶 ) ∈ ℂ → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) = ( ( 𝐶 ·ih 𝐶 ) + ( 1 + 1 ) ) ) |
| 38 |
34 37
|
syl |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) = ( ( 𝐶 ·ih 𝐶 ) + ( 1 + 1 ) ) ) |
| 39 |
33 38
|
eqtr4id |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 2 ) = ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) ) |
| 40 |
31 39
|
breqtrrd |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) < ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) |
| 41 |
24 26 23 30 40
|
lttrd |
⊢ ( 𝜑 → 0 < ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) |
| 42 |
23 41
|
elrpd |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℝ+ ) |
| 43 |
|
oveq2 |
⊢ ( 𝑥 = ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) → ( 𝐴 −ℎ 𝑥 ) = ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 44 |
43
|
fveq2d |
⊢ ( 𝑥 = ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) → ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) = ( normℎ ‘ ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 45 |
44
|
breq2d |
⊢ ( 𝑥 = ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) ↔ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) ) |
| 46 |
1
|
chshii |
⊢ 𝐻 ∈ Sℋ |
| 47 |
46
|
a1i |
⊢ ( 𝜑 → 𝐻 ∈ Sℋ ) |
| 48 |
26
|
recnd |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) ∈ ℂ ) |
| 49 |
20 28
|
ge0p1rpd |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) ∈ ℝ+ ) |
| 50 |
49
|
rpne0d |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 1 ) ≠ 0 ) |
| 51 |
14 48 50
|
divcld |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ∈ ℂ ) |
| 52 |
6 51
|
eqeltrid |
⊢ ( 𝜑 → 𝑇 ∈ ℂ ) |
| 53 |
|
shmulcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝑇 ∈ ℂ ∧ 𝐶 ∈ 𝐻 ) → ( 𝑇 ·ℎ 𝐶 ) ∈ 𝐻 ) |
| 54 |
47 52 4 53
|
syl3anc |
⊢ ( 𝜑 → ( 𝑇 ·ℎ 𝐶 ) ∈ 𝐻 ) |
| 55 |
|
shaddcl |
⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐵 ∈ 𝐻 ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ 𝐻 ) → ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ 𝐻 ) |
| 56 |
47 3 54 55
|
syl3anc |
⊢ ( 𝜑 → ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ 𝐻 ) |
| 57 |
45 5 56
|
rspcdva |
⊢ ( 𝜑 → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 58 |
1
|
cheli |
⊢ ( ( 𝑇 ·ℎ 𝐶 ) ∈ 𝐻 → ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) |
| 59 |
54 58
|
syl |
⊢ ( 𝜑 → ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) |
| 60 |
|
hvsubass |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) = ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 61 |
2 8 59 60
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) = ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 62 |
61
|
fveq2d |
⊢ ( 𝜑 → ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( normℎ ‘ ( 𝐴 −ℎ ( 𝐵 +ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 63 |
57 62
|
breqtrrd |
⊢ ( 𝜑 → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 64 |
|
normcl |
⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ∈ ℝ ) |
| 65 |
10 64
|
syl |
⊢ ( 𝜑 → ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ∈ ℝ ) |
| 66 |
|
hvsubcl |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℋ ) |
| 67 |
10 59 66
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℋ ) |
| 68 |
|
normcl |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℋ → ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ∈ ℝ ) |
| 69 |
67 68
|
syl |
⊢ ( 𝜑 → ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ∈ ℝ ) |
| 70 |
|
normge0 |
⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ → 0 ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ) |
| 71 |
10 70
|
syl |
⊢ ( 𝜑 → 0 ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ) |
| 72 |
24 65 69 71 63
|
letrd |
⊢ ( 𝜑 → 0 ≤ ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 73 |
65 69 71 72
|
le2sqd |
⊢ ( 𝜑 → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↔ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) ) ) |
| 74 |
63 73
|
mpbid |
⊢ ( 𝜑 → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) ) |
| 75 |
69
|
resqcld |
⊢ ( 𝜑 → ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) ∈ ℝ ) |
| 76 |
65
|
resqcld |
⊢ ( 𝜑 → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ∈ ℝ ) |
| 77 |
75 76
|
subge0d |
⊢ ( 𝜑 → ( 0 ≤ ( ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) ↔ ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ≤ ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) ) ) |
| 78 |
74 77
|
mpbird |
⊢ ( 𝜑 → 0 ≤ ( ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) ) |
| 79 |
|
2z |
⊢ 2 ∈ ℤ |
| 80 |
|
rpexpcl |
⊢ ( ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ∈ ℝ+ ) |
| 81 |
49 79 80
|
sylancl |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ∈ ℝ+ ) |
| 82 |
17 81
|
rerpdivcld |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ∈ ℝ ) |
| 83 |
82 23
|
remulcld |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ∈ ℝ ) |
| 84 |
83
|
recnd |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ∈ ℂ ) |
| 85 |
84
|
negcld |
⊢ ( 𝜑 → - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ∈ ℂ ) |
| 86 |
|
hicl |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
| 87 |
10 10 86
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
| 88 |
85 87
|
pncand |
⊢ ( 𝜑 → ( ( - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) + ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) = - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 89 |
|
normsq |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℋ → ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) = ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 90 |
67 89
|
syl |
⊢ ( 𝜑 → ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) = ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 91 |
|
his2sub |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ∧ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℋ ) → ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 92 |
10 59 67 91
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 93 |
|
his2sub2 |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 94 |
10 10 59 93
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 95 |
94
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) = ( ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) |
| 96 |
|
hicl |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℂ ) |
| 97 |
10 59 96
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℂ ) |
| 98 |
|
his2sub2 |
⊢ ( ( ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 99 |
59 10 59 98
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) ) |
| 100 |
|
hicl |
⊢ ( ( ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
| 101 |
59 10 100
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
| 102 |
|
hicl |
⊢ ( ( ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℂ ) |
| 103 |
59 59 102
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℂ ) |
| 104 |
101 103
|
subcld |
⊢ ( 𝜑 → ( ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) ∈ ℂ ) |
| 105 |
99 104
|
eqeltrd |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ∈ ℂ ) |
| 106 |
87 97 105
|
subsub4d |
⊢ ( 𝜑 → ( ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) + ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) ) |
| 107 |
82
|
recnd |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ∈ ℂ ) |
| 108 |
35
|
a1i |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
| 109 |
107 48 108
|
adddid |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) ) = ( ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) + ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · 1 ) ) ) |
| 110 |
39
|
oveq2d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) + 1 ) ) ) |
| 111 |
|
his5 |
⊢ ( ( 𝑇 ∈ ℂ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( ∗ ‘ 𝑇 ) · ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ) |
| 112 |
52 10 12 111
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( ∗ ‘ 𝑇 ) · ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ) |
| 113 |
52
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) ∈ ℂ ) |
| 114 |
113 14
|
mulcomd |
⊢ ( 𝜑 → ( ( ∗ ‘ 𝑇 ) · ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ 𝑇 ) ) ) |
| 115 |
14
|
cjcld |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ∈ ℂ ) |
| 116 |
14 115 48 50
|
divassd |
⊢ ( 𝜑 → ( ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) ) |
| 117 |
14
|
absvalsqd |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ) ) |
| 118 |
117
|
oveq1d |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 119 |
6
|
fveq2i |
⊢ ( ∗ ‘ 𝑇 ) = ( ∗ ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 120 |
14 48 50
|
cjdivd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ∗ ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) ) |
| 121 |
26
|
cjred |
⊢ ( 𝜑 → ( ∗ ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 122 |
121
|
oveq2d |
⊢ ( 𝜑 → ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ∗ ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 123 |
120 122
|
eqtrd |
⊢ ( 𝜑 → ( ∗ ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 124 |
119 123
|
eqtrid |
⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 125 |
124
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ 𝑇 ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) ) |
| 126 |
116 118 125
|
3eqtr4rd |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) · ( ∗ ‘ 𝑇 ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 127 |
112 114 126
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 128 |
17
|
recnd |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ∈ ℂ ) |
| 129 |
128 48
|
mulcomd |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) ) |
| 130 |
48
|
sqvald |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) = ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 131 |
129 130
|
oveq12d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) = ( ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) ) |
| 132 |
128 48 48 50 50
|
divcan5d |
⊢ ( 𝜑 → ( ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 133 |
131 132
|
eqtr2d |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ) |
| 134 |
26
|
resqcld |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ∈ ℝ ) |
| 135 |
134
|
recnd |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ∈ ℂ ) |
| 136 |
81
|
rpne0d |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ≠ 0 ) |
| 137 |
128 48 135 136
|
div23d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 138 |
127 133 137
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 139 |
82 26
|
remulcld |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ∈ ℝ ) |
| 140 |
138 139
|
eqeltrd |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℝ ) |
| 141 |
|
hire |
⊢ ( ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ∧ ( 𝑇 ·ℎ 𝐶 ) ∈ ℋ ) → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℝ ↔ ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
| 142 |
10 59 141
|
syl2anc |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ∈ ℝ ↔ ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
| 143 |
140 142
|
mpbid |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) |
| 144 |
143 138
|
eqtr3d |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 145 |
|
his35 |
⊢ ( ( ( 𝑇 ∈ ℂ ∧ 𝑇 ∈ ℂ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) |
| 146 |
52 52 12 12 145
|
syl22anc |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) |
| 147 |
6
|
fveq2i |
⊢ ( abs ‘ 𝑇 ) = ( abs ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 148 |
14 48 50
|
absdivd |
⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( abs ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) ) |
| 149 |
49
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 150 |
26 149
|
absidd |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) = ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) |
| 151 |
150
|
oveq2d |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( abs ‘ ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 152 |
148 151
|
eqtrd |
⊢ ( 𝜑 → ( abs ‘ ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) = ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 153 |
147 152
|
eqtrid |
⊢ ( 𝜑 → ( abs ‘ 𝑇 ) = ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ) |
| 154 |
153
|
oveq1d |
⊢ ( 𝜑 → ( ( abs ‘ 𝑇 ) ↑ 2 ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ↑ 2 ) ) |
| 155 |
52
|
absvalsqd |
⊢ ( 𝜑 → ( ( abs ‘ 𝑇 ) ↑ 2 ) = ( 𝑇 · ( ∗ ‘ 𝑇 ) ) ) |
| 156 |
16 48 50
|
sqdivd |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) ↑ 2 ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ) |
| 157 |
154 155 156
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝑇 · ( ∗ ‘ 𝑇 ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ) |
| 158 |
157
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑇 · ( ∗ ‘ 𝑇 ) ) · ( 𝐶 ·ih 𝐶 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) |
| 159 |
146 158
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) |
| 160 |
144 159
|
oveq12d |
⊢ ( 𝜑 → ( ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) ) |
| 161 |
|
pncan2 |
⊢ ( ( ( 𝐶 ·ih 𝐶 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) − ( 𝐶 ·ih 𝐶 ) ) = 1 ) |
| 162 |
34 35 161
|
sylancl |
⊢ ( 𝜑 → ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) − ( 𝐶 ·ih 𝐶 ) ) = 1 ) |
| 163 |
162
|
oveq2d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) − ( 𝐶 ·ih 𝐶 ) ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · 1 ) ) |
| 164 |
107 48 34
|
subdid |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) − ( 𝐶 ·ih 𝐶 ) ) ) = ( ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) ) |
| 165 |
163 164
|
eqtr3d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · 1 ) = ( ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( 𝐶 ·ih 𝐶 ) ) ) ) |
| 166 |
160 99 165
|
3eqtr4d |
⊢ ( 𝜑 → ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · 1 ) ) |
| 167 |
138 166
|
oveq12d |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) + ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) = ( ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 1 ) ) + ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · 1 ) ) ) |
| 168 |
109 110 167
|
3eqtr4rd |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) + ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 169 |
168
|
oveq2d |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝑇 ·ℎ 𝐶 ) ) + ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) ) |
| 170 |
95 106 169
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) − ( ( 𝑇 ·ℎ 𝐶 ) ·ih ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) ) |
| 171 |
90 92 170
|
3eqtrd |
⊢ ( 𝜑 → ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) ) |
| 172 |
87 84
|
negsubd |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) + - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) ) |
| 173 |
87 85
|
addcomd |
⊢ ( 𝜑 → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) + - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) = ( - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) + ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
| 174 |
171 172 173
|
3eqtr2d |
⊢ ( 𝜑 → ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) = ( - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) + ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
| 175 |
|
normsq |
⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) |
| 176 |
10 175
|
syl |
⊢ ( 𝜑 → ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) |
| 177 |
174 176
|
oveq12d |
⊢ ( 𝜑 → ( ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) = ( ( - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) + ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) − ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
| 178 |
23
|
renegcld |
⊢ ( 𝜑 → - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℝ ) |
| 179 |
178
|
recnd |
⊢ ( 𝜑 → - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℂ ) |
| 180 |
128 179 135 136
|
div23d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) = ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 181 |
23
|
recnd |
⊢ ( 𝜑 → ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℂ ) |
| 182 |
107 181
|
mulneg2d |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) = - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 183 |
180 182
|
eqtrd |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) = - ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 184 |
88 177 183
|
3eqtr4rd |
⊢ ( 𝜑 → ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) = ( ( ( normℎ ‘ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝑇 ·ℎ 𝐶 ) ) ) ↑ 2 ) − ( ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ↑ 2 ) ) ) |
| 185 |
78 184
|
breqtrrd |
⊢ ( 𝜑 → 0 ≤ ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ) |
| 186 |
17 178
|
remulcld |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ∈ ℝ ) |
| 187 |
186 81
|
ge0divd |
⊢ ( 𝜑 → ( 0 ≤ ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ↔ 0 ≤ ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) / ( ( ( 𝐶 ·ih 𝐶 ) + 1 ) ↑ 2 ) ) ) ) |
| 188 |
185 187
|
mpbird |
⊢ ( 𝜑 → 0 ≤ ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 189 |
|
mulneg12 |
⊢ ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ∈ ℂ ∧ ( ( 𝐶 ·ih 𝐶 ) + 2 ) ∈ ℂ ) → ( - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 190 |
128 181 189
|
syl2anc |
⊢ ( 𝜑 → ( - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) = ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · - ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 191 |
188 190
|
breqtrrd |
⊢ ( 𝜑 → 0 ≤ ( - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) · ( ( 𝐶 ·ih 𝐶 ) + 2 ) ) ) |
| 192 |
18 42 191
|
prodge0ld |
⊢ ( 𝜑 → 0 ≤ - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) |
| 193 |
17
|
le0neg1d |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ≤ 0 ↔ 0 ≤ - ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) ) |
| 194 |
192 193
|
mpbird |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ≤ 0 ) |
| 195 |
15
|
sqge0d |
⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) |
| 196 |
|
0re |
⊢ 0 ∈ ℝ |
| 197 |
|
letri3 |
⊢ ( ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) = 0 ↔ ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) ) ) |
| 198 |
17 196 197
|
sylancl |
⊢ ( 𝜑 → ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) = 0 ↔ ( ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ≤ 0 ∧ 0 ≤ ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) ) ) ) |
| 199 |
194 195 198
|
mpbir2and |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) ↑ 2 ) = 0 ) |
| 200 |
16 199
|
sqeq0d |
⊢ ( 𝜑 → ( abs ‘ ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) ) = 0 ) |
| 201 |
14 200
|
abs00d |
⊢ ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = 0 ) |