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 ⊢H∈Cℋ
pjhth.2 ⊢φ→A∈ℋ
pjhth.3 ⊢φ→B∈H
pjhth.4 ⊢φ→C∈H
pjhth.5 ⊢φ→∀x∈Hnormℎ⁡A-ℎB≤normℎ⁡A-ℎx
pjhth.6 ⊢T=A-ℎB⋅ihCC⋅ihC+1
Assertion pjhthlem1 ⊢φ→A-ℎB⋅ihC=0

Proof

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