Proof of Theorem bcsiALT
| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ ((𝐴
·ih 𝐵) = 0 → (abs‘(𝐴 ·ih 𝐵)) =
(abs‘0)) |
| 2 | | abs0 15324 |
. . . 4
⊢
(abs‘0) = 0 |
| 3 | | bcs.1 |
. . . . . 6
⊢ 𝐴 ∈ ℋ |
| 4 | | normge0 31145 |
. . . . . 6
⊢ (𝐴 ∈ ℋ → 0 ≤
(normℎ‘𝐴)) |
| 5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢ 0 ≤
(normℎ‘𝐴) |
| 6 | | bcs.2 |
. . . . . 6
⊢ 𝐵 ∈ ℋ |
| 7 | | normge0 31145 |
. . . . . 6
⊢ (𝐵 ∈ ℋ → 0 ≤
(normℎ‘𝐵)) |
| 8 | 6, 7 | ax-mp 5 |
. . . . 5
⊢ 0 ≤
(normℎ‘𝐵) |
| 9 | 3 | normcli 31150 |
. . . . . 6
⊢
(normℎ‘𝐴) ∈ ℝ |
| 10 | 6 | normcli 31150 |
. . . . . 6
⊢
(normℎ‘𝐵) ∈ ℝ |
| 11 | 9, 10 | mulge0i 11810 |
. . . . 5
⊢ ((0 ≤
(normℎ‘𝐴) ∧ 0 ≤
(normℎ‘𝐵)) → 0 ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵))) |
| 12 | 5, 8, 11 | mp2an 692 |
. . . 4
⊢ 0 ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵)) |
| 13 | 2, 12 | eqbrtri 5164 |
. . 3
⊢
(abs‘0) ≤ ((normℎ‘𝐴) ·
(normℎ‘𝐵)) |
| 14 | 1, 13 | eqbrtrdi 5182 |
. 2
⊢ ((𝐴
·ih 𝐵) = 0 → (abs‘(𝐴 ·ih 𝐵)) ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵))) |
| 15 | | df-ne 2941 |
. . . 4
⊢ ((𝐴
·ih 𝐵) ≠ 0 ↔ ¬ (𝐴 ·ih 𝐵) = 0) |
| 16 | 6, 3 | his1i 31119 |
. . . . . . . 8
⊢ (𝐵
·ih 𝐴) = (∗‘(𝐴 ·ih 𝐵)) |
| 17 | 16 | oveq2i 7442 |
. . . . . . 7
⊢ (((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵))) · (𝐵 ·ih 𝐴)) = (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (∗‘(𝐴
·ih 𝐵))) |
| 18 | 17 | oveq2i 7442 |
. . . . . 6
⊢
(((∗‘((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (𝐵 ·ih 𝐴))) = (((∗‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (∗‘(𝐴
·ih 𝐵)))) |
| 19 | 3, 6 | hicli 31100 |
. . . . . . 7
⊢ (𝐴
·ih 𝐵) ∈ ℂ |
| 20 | | abslem2 15378 |
. . . . . . 7
⊢ (((𝐴
·ih 𝐵) ∈ ℂ ∧ (𝐴 ·ih 𝐵) ≠ 0) →
(((∗‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (∗‘(𝐴
·ih 𝐵)))) = (2 · (abs‘(𝐴
·ih 𝐵)))) |
| 21 | 19, 20 | mpan 690 |
. . . . . 6
⊢ ((𝐴
·ih 𝐵) ≠ 0 → (((∗‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (∗‘(𝐴
·ih 𝐵)))) = (2 · (abs‘(𝐴
·ih 𝐵)))) |
| 22 | 18, 21 | eqtr2id 2790 |
. . . . 5
⊢ ((𝐴
·ih 𝐵) ≠ 0 → (2 ·
(abs‘(𝐴
·ih 𝐵))) = (((∗‘((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (𝐵 ·ih 𝐴)))) |
| 23 | 19 | abs00i 15437 |
. . . . . . . 8
⊢
((abs‘(𝐴
·ih 𝐵)) = 0 ↔ (𝐴 ·ih 𝐵) = 0) |
| 24 | 23 | necon3bii 2993 |
. . . . . . 7
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 ↔ (𝐴 ·ih 𝐵) ≠ 0) |
| 25 | 19 | abscli 15434 |
. . . . . . . . . 10
⊢
(abs‘(𝐴
·ih 𝐵)) ∈ ℝ |
| 26 | 25 | recni 11275 |
. . . . . . . . 9
⊢
(abs‘(𝐴
·ih 𝐵)) ∈ ℂ |
| 27 | 19, 26 | divclzi 12002 |
. . . . . . . 8
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → ((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) ∈ ℂ) |
| 28 | 19, 26 | divreczi 12005 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → ((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) = ((𝐴 ·ih 𝐵) · (1 /
(abs‘(𝐴
·ih 𝐵))))) |
| 29 | 28 | fveq2d 6910 |
. . . . . . . . 9
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (abs‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) = (abs‘((𝐴
·ih 𝐵) · (1 / (abs‘(𝐴
·ih 𝐵)))))) |
| 30 | 26 | recclzi 11992 |
. . . . . . . . . . 11
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (1 / (abs‘(𝐴
·ih 𝐵))) ∈ ℂ) |
| 31 | | absmul 15333 |
. . . . . . . . . . 11
⊢ (((𝐴
·ih 𝐵) ∈ ℂ ∧ (1 /
(abs‘(𝐴
·ih 𝐵))) ∈ ℂ) →
(abs‘((𝐴
·ih 𝐵) · (1 / (abs‘(𝐴
·ih 𝐵))))) = ((abs‘(𝐴 ·ih 𝐵)) · (abs‘(1 /
(abs‘(𝐴
·ih 𝐵)))))) |
| 32 | 19, 30, 31 | sylancr 587 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (abs‘((𝐴
·ih 𝐵) · (1 / (abs‘(𝐴
·ih 𝐵))))) = ((abs‘(𝐴 ·ih 𝐵)) · (abs‘(1 /
(abs‘(𝐴
·ih 𝐵)))))) |
| 33 | 25 | rerecclzi 12031 |
. . . . . . . . . . . 12
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (1 / (abs‘(𝐴
·ih 𝐵))) ∈ ℝ) |
| 34 | | 0re 11263 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
| 35 | 33, 34 | jctil 519 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (0 ∈ ℝ ∧ (1
/ (abs‘(𝐴
·ih 𝐵))) ∈ ℝ)) |
| 36 | 19 | absgt0i 15438 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴
·ih 𝐵) ≠ 0 ↔ 0 < (abs‘(𝐴
·ih 𝐵))) |
| 37 | 24, 36 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 ↔ 0 < (abs‘(𝐴
·ih 𝐵))) |
| 38 | 25 | recgt0i 12173 |
. . . . . . . . . . . . . 14
⊢ (0 <
(abs‘(𝐴
·ih 𝐵)) → 0 < (1 / (abs‘(𝐴
·ih 𝐵)))) |
| 39 | 37, 38 | sylbi 217 |
. . . . . . . . . . . . 13
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → 0 < (1 /
(abs‘(𝐴
·ih 𝐵)))) |
| 40 | | ltle 11349 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ (1 / (abs‘(𝐴 ·ih 𝐵))) ∈ ℝ) → (0
< (1 / (abs‘(𝐴
·ih 𝐵))) → 0 ≤ (1 / (abs‘(𝐴
·ih 𝐵))))) |
| 41 | 35, 39, 40 | sylc 65 |
. . . . . . . . . . . 12
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → 0 ≤ (1 /
(abs‘(𝐴
·ih 𝐵)))) |
| 42 | 33, 41 | absidd 15461 |
. . . . . . . . . . 11
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (abs‘(1 /
(abs‘(𝐴
·ih 𝐵)))) = (1 / (abs‘(𝐴 ·ih 𝐵)))) |
| 43 | 42 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → ((abs‘(𝐴
·ih 𝐵)) · (abs‘(1 /
(abs‘(𝐴
·ih 𝐵))))) = ((abs‘(𝐴 ·ih 𝐵)) · (1 /
(abs‘(𝐴
·ih 𝐵))))) |
| 44 | 32, 43 | eqtrd 2777 |
. . . . . . . . 9
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (abs‘((𝐴
·ih 𝐵) · (1 / (abs‘(𝐴
·ih 𝐵))))) = ((abs‘(𝐴 ·ih 𝐵)) · (1 /
(abs‘(𝐴
·ih 𝐵))))) |
| 45 | 26 | recidzi 11994 |
. . . . . . . . 9
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → ((abs‘(𝐴
·ih 𝐵)) · (1 / (abs‘(𝐴
·ih 𝐵)))) = 1) |
| 46 | 29, 44, 45 | 3eqtrd 2781 |
. . . . . . . 8
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (abs‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) = 1) |
| 47 | 27, 46 | jca 511 |
. . . . . . 7
⊢
((abs‘(𝐴
·ih 𝐵)) ≠ 0 → (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) ∈ ℂ ∧ (abs‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) = 1)) |
| 48 | 24, 47 | sylbir 235 |
. . . . . 6
⊢ ((𝐴
·ih 𝐵) ≠ 0 → (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) ∈ ℂ ∧ (abs‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) = 1)) |
| 49 | 3, 6 | normlem7tALT 31138 |
. . . . . 6
⊢ ((((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵))) ∈ ℂ ∧
(abs‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) = 1) →
(((∗‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (𝐵 ·ih 𝐴))) ≤ (2 ·
((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((𝐴
·ih 𝐵) ≠ 0 → (((∗‘((𝐴
·ih 𝐵) / (abs‘(𝐴 ·ih 𝐵)))) · (𝐴 ·ih 𝐵)) + (((𝐴 ·ih 𝐵) / (abs‘(𝐴
·ih 𝐵))) · (𝐵 ·ih 𝐴))) ≤ (2 ·
((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 51 | 22, 50 | eqbrtrd 5165 |
. . . 4
⊢ ((𝐴
·ih 𝐵) ≠ 0 → (2 ·
(abs‘(𝐴
·ih 𝐵))) ≤ (2 · ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 52 | 15, 51 | sylbir 235 |
. . 3
⊢ (¬
(𝐴
·ih 𝐵) = 0 → (2 · (abs‘(𝐴
·ih 𝐵))) ≤ (2 · ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 53 | 10 | recni 11275 |
. . . . . 6
⊢
(normℎ‘𝐵) ∈ ℂ |
| 54 | 9 | recni 11275 |
. . . . . 6
⊢
(normℎ‘𝐴) ∈ ℂ |
| 55 | | normval 31143 |
. . . . . . . 8
⊢ (𝐵 ∈ ℋ →
(normℎ‘𝐵) = (√‘(𝐵 ·ih 𝐵))) |
| 56 | 6, 55 | ax-mp 5 |
. . . . . . 7
⊢
(normℎ‘𝐵) = (√‘(𝐵 ·ih 𝐵)) |
| 57 | | normval 31143 |
. . . . . . . 8
⊢ (𝐴 ∈ ℋ →
(normℎ‘𝐴) = (√‘(𝐴 ·ih 𝐴))) |
| 58 | 3, 57 | ax-mp 5 |
. . . . . . 7
⊢
(normℎ‘𝐴) = (√‘(𝐴 ·ih 𝐴)) |
| 59 | 56, 58 | oveq12i 7443 |
. . . . . 6
⊢
((normℎ‘𝐵) ·
(normℎ‘𝐴)) = ((√‘(𝐵 ·ih 𝐵)) ·
(√‘(𝐴
·ih 𝐴))) |
| 60 | 53, 54, 59 | mulcomli 11270 |
. . . . 5
⊢
((normℎ‘𝐴) ·
(normℎ‘𝐵)) = ((√‘(𝐵 ·ih 𝐵)) ·
(√‘(𝐴
·ih 𝐴))) |
| 61 | 60 | breq2i 5151 |
. . . 4
⊢
((abs‘(𝐴
·ih 𝐵)) ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵)) ↔ (abs‘(𝐴 ·ih 𝐵)) ≤ ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴)))) |
| 62 | | 2pos 12369 |
. . . . 5
⊢ 0 <
2 |
| 63 | | hiidge0 31117 |
. . . . . . . 8
⊢ (𝐵 ∈ ℋ → 0 ≤
(𝐵
·ih 𝐵)) |
| 64 | | hiidrcl 31114 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℋ → (𝐵
·ih 𝐵) ∈ ℝ) |
| 65 | 6, 64 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐵
·ih 𝐵) ∈ ℝ |
| 66 | 65 | sqrtcli 15410 |
. . . . . . . 8
⊢ (0 ≤
(𝐵
·ih 𝐵) → (√‘(𝐵 ·ih 𝐵)) ∈
ℝ) |
| 67 | 6, 63, 66 | mp2b 10 |
. . . . . . 7
⊢
(√‘(𝐵
·ih 𝐵)) ∈ ℝ |
| 68 | | hiidge0 31117 |
. . . . . . . 8
⊢ (𝐴 ∈ ℋ → 0 ≤
(𝐴
·ih 𝐴)) |
| 69 | | hiidrcl 31114 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℋ → (𝐴
·ih 𝐴) ∈ ℝ) |
| 70 | 3, 69 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐴
·ih 𝐴) ∈ ℝ |
| 71 | 70 | sqrtcli 15410 |
. . . . . . . 8
⊢ (0 ≤
(𝐴
·ih 𝐴) → (√‘(𝐴 ·ih 𝐴)) ∈
ℝ) |
| 72 | 3, 68, 71 | mp2b 10 |
. . . . . . 7
⊢
(√‘(𝐴
·ih 𝐴)) ∈ ℝ |
| 73 | 67, 72 | remulcli 11277 |
. . . . . 6
⊢
((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))) ∈ ℝ |
| 74 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 75 | 25, 73, 74 | lemul2i 12191 |
. . . . 5
⊢ (0 < 2
→ ((abs‘(𝐴
·ih 𝐵)) ≤ ((√‘(𝐵 ·ih 𝐵)) ·
(√‘(𝐴
·ih 𝐴))) ↔ (2 · (abs‘(𝐴
·ih 𝐵))) ≤ (2 · ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴)))))) |
| 76 | 62, 75 | ax-mp 5 |
. . . 4
⊢
((abs‘(𝐴
·ih 𝐵)) ≤ ((√‘(𝐵 ·ih 𝐵)) ·
(√‘(𝐴
·ih 𝐴))) ↔ (2 · (abs‘(𝐴
·ih 𝐵))) ≤ (2 · ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 77 | 61, 76 | bitri 275 |
. . 3
⊢
((abs‘(𝐴
·ih 𝐵)) ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵)) ↔ (2 · (abs‘(𝐴
·ih 𝐵))) ≤ (2 · ((√‘(𝐵
·ih 𝐵)) · (√‘(𝐴
·ih 𝐴))))) |
| 78 | 52, 77 | sylibr 234 |
. 2
⊢ (¬
(𝐴
·ih 𝐵) = 0 → (abs‘(𝐴 ·ih 𝐵)) ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵))) |
| 79 | 14, 78 | pm2.61i 182 |
1
⊢
(abs‘(𝐴
·ih 𝐵)) ≤
((normℎ‘𝐴) ·
(normℎ‘𝐵)) |