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