This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjhthlem1

Description: Lemma for pjhth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (Proof shortened by AV, 10-Jul-2022) (New usage is discouraged.)

Ref Expression
Hypotheses pjhth.1 ⊢ 𝐻 ∈ Cℋ
pjhth.2 ⊢ ( 𝜑 → 𝐴 ∈ ℋ )
pjhth.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝐻 )
pjhth.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝐻 )
pjhth.5 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐻 ( normℎ ‘ ( 𝐴 −ℎ 𝐵 ) ) ≤ ( normℎ ‘ ( 𝐴 −ℎ 𝑥 ) ) )
pjhth.6 ⊢ 𝑇 = ( ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) / ( ( 𝐶 ·ih 𝐶 ) + 1 ) )
Assertion pjhthlem1 ( 𝜑 → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = 0 )

Proof

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 )