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	syl5eq	⊢ ( 𝜑 → ( ∗ ‘ 𝑇 ) = ( ( ∗ ‘ ( ( 𝐴 −ℎ 𝐵 ) ·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	syl5eq	⊢ ( 𝜑 → ( 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 )