Step | Hyp | Ref
| Expression |
1 | | oveq2 7359 |
. . . . 5
β’ (π΅ = (0vecβπ) β (π΄ππ΅) = (π΄π(0vecβπ))) |
2 | | siii.9 |
. . . . . . 7
β’ π β
CPreHilOLD |
3 | 2 | phnvi 29587 |
. . . . . 6
β’ π β NrmCVec |
4 | | siii.a |
. . . . . 6
β’ π΄ β π |
5 | | siii.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
6 | | eqid 2737 |
. . . . . . 7
β’
(0vecβπ) = (0vecβπ) |
7 | | siii.7 |
. . . . . . 7
β’ π =
(Β·πOLDβπ) |
8 | 5, 6, 7 | dip0r 29488 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π) β (π΄π(0vecβπ)) = 0) |
9 | 3, 4, 8 | mp2an 690 |
. . . . 5
β’ (π΄π(0vecβπ)) = 0 |
10 | 1, 9 | eqtrdi 2793 |
. . . 4
β’ (π΅ = (0vecβπ) β (π΄ππ΅) = 0) |
11 | 10 | abs00bd 15136 |
. . 3
β’ (π΅ = (0vecβπ) β (absβ(π΄ππ΅)) = 0) |
12 | | siii.6 |
. . . . . 6
β’ π =
(normCVβπ) |
13 | 5, 12 | nvge0 29444 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β 0 β€ (πβπ΄)) |
14 | 3, 4, 13 | mp2an 690 |
. . . 4
β’ 0 β€
(πβπ΄) |
15 | | siii.b |
. . . . 5
β’ π΅ β π |
16 | 5, 12 | nvge0 29444 |
. . . . 5
β’ ((π β NrmCVec β§ π΅ β π) β 0 β€ (πβπ΅)) |
17 | 3, 15, 16 | mp2an 690 |
. . . 4
β’ 0 β€
(πβπ΅) |
18 | 5, 12, 3, 4 | nvcli 29433 |
. . . . 5
β’ (πβπ΄) β β |
19 | 5, 12, 3, 15 | nvcli 29433 |
. . . . 5
β’ (πβπ΅) β β |
20 | 18, 19 | mulge0i 11660 |
. . . 4
β’ ((0 β€
(πβπ΄) β§ 0 β€ (πβπ΅)) β 0 β€ ((πβπ΄) Β· (πβπ΅))) |
21 | 14, 17, 20 | mp2an 690 |
. . 3
β’ 0 β€
((πβπ΄) Β· (πβπ΅)) |
22 | 11, 21 | eqbrtrdi 5142 |
. 2
β’ (π΅ = (0vecβπ) β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) |
23 | 5, 7 | dipcl 29483 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) β β) |
24 | 3, 4, 15, 23 | mp3an 1461 |
. . . . 5
β’ (π΄ππ΅) β β |
25 | | absval 15083 |
. . . . 5
β’ ((π΄ππ΅) β β β (absβ(π΄ππ΅)) = (ββ((π΄ππ΅) Β· (ββ(π΄ππ΅))))) |
26 | 24, 25 | ax-mp 5 |
. . . 4
β’
(absβ(π΄ππ΅)) = (ββ((π΄ππ΅) Β· (ββ(π΄ππ΅)))) |
27 | 19 | recni 11127 |
. . . . . . . . . . 11
β’ (πβπ΅) β β |
28 | 27 | sqeq0i 14040 |
. . . . . . . . . 10
β’ (((πβπ΅)β2) = 0 β (πβπ΅) = 0) |
29 | 5, 6, 12 | nvz 29440 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β ((πβπ΅) = 0 β π΅ = (0vecβπ))) |
30 | 3, 15, 29 | mp2an 690 |
. . . . . . . . . 10
β’ ((πβπ΅) = 0 β π΅ = (0vecβπ)) |
31 | 28, 30 | bitri 274 |
. . . . . . . . 9
β’ (((πβπ΅)β2) = 0 β π΅ = (0vecβπ)) |
32 | 31 | necon3bii 2994 |
. . . . . . . 8
β’ (((πβπ΅)β2) β 0 β π΅ β (0vecβπ)) |
33 | 5, 7 | dipcl 29483 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΅ β π β§ π΄ β π) β (π΅ππ΄) β β) |
34 | 3, 15, 4, 33 | mp3an 1461 |
. . . . . . . . 9
β’ (π΅ππ΄) β β |
35 | 19 | resqcli 14044 |
. . . . . . . . . 10
β’ ((πβπ΅)β2) β β |
36 | 35 | recni 11127 |
. . . . . . . . 9
β’ ((πβπ΅)β2) β β |
37 | 34, 36 | divcan1zi 11849 |
. . . . . . . 8
β’ (((πβπ΅)β2) β 0 β (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)) = (π΅ππ΄)) |
38 | 32, 37 | sylbir 234 |
. . . . . . 7
β’ (π΅ β
(0vecβπ)
β (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)) = (π΅ππ΄)) |
39 | 5, 7 | dipcj 29485 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (ββ(π΄ππ΅)) = (π΅ππ΄)) |
40 | 3, 4, 15, 39 | mp3an 1461 |
. . . . . . 7
β’
(ββ(π΄ππ΅)) = (π΅ππ΄) |
41 | 38, 40 | eqtr4di 2795 |
. . . . . 6
β’ (π΅ β
(0vecβπ)
β (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)) = (ββ(π΄ππ΅))) |
42 | 41 | oveq2d 7367 |
. . . . 5
β’ (π΅ β
(0vecβπ)
β ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2))) = ((π΄ππ΅) Β· (ββ(π΄ππ΅)))) |
43 | 42 | fveq2d 6843 |
. . . 4
β’ (π΅ β
(0vecβπ)
β (ββ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)))) = (ββ((π΄ππ΅) Β· (ββ(π΄ππ΅))))) |
44 | 26, 43 | eqtr4id 2796 |
. . 3
β’ (π΅ β
(0vecβπ)
β (absβ(π΄ππ΅)) = (ββ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2))))) |
45 | 38 | eqcomd 2743 |
. . . 4
β’ (π΅ β
(0vecβπ)
β (π΅ππ΄) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2))) |
46 | 34, 36 | divclzi 11848 |
. . . . . 6
β’ (((πβπ΅)β2) β 0 β ((π΅ππ΄) / ((πβπ΅)β2)) β β) |
47 | 32, 46 | sylbir 234 |
. . . . 5
β’ (π΅ β
(0vecβπ)
β ((π΅ππ΄) / ((πβπ΅)β2)) β β) |
48 | | div23 11790 |
. . . . . . . . . 10
β’ (((π΅ππ΄) β β β§ (π΄ππ΅) β β β§ (((πβπ΅)β2) β β β§ ((πβπ΅)β2) β 0)) β (((π΅ππ΄) Β· (π΄ππ΅)) / ((πβπ΅)β2)) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) |
49 | 34, 24, 48 | mp3an12 1451 |
. . . . . . . . 9
β’ ((((πβπ΅)β2) β β β§ ((πβπ΅)β2) β 0) β (((π΅ππ΄) Β· (π΄ππ΅)) / ((πβπ΅)β2)) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) |
50 | 36, 49 | mpan 688 |
. . . . . . . 8
β’ (((πβπ΅)β2) β 0 β (((π΅ππ΄) Β· (π΄ππ΅)) / ((πβπ΅)β2)) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) |
51 | 32, 50 | sylbir 234 |
. . . . . . 7
β’ (π΅ β
(0vecβπ)
β (((π΅ππ΄) Β· (π΄ππ΅)) / ((πβπ΅)β2)) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) |
52 | 5, 7 | ipipcj 29486 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄ππ΅) Β· (π΅ππ΄)) = ((absβ(π΄ππ΅))β2)) |
53 | 3, 4, 15, 52 | mp3an 1461 |
. . . . . . . . 9
β’ ((π΄ππ΅) Β· (π΅ππ΄)) = ((absβ(π΄ππ΅))β2) |
54 | 24, 34, 53 | mulcomli 11122 |
. . . . . . . 8
β’ ((π΅ππ΄) Β· (π΄ππ΅)) = ((absβ(π΄ππ΅))β2) |
55 | 54 | oveq1i 7361 |
. . . . . . 7
β’ (((π΅ππ΄) Β· (π΄ππ΅)) / ((πβπ΅)β2)) = (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2)) |
56 | 51, 55 | eqtr3di 2792 |
. . . . . 6
β’ (π΅ β
(0vecβπ)
β (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅)) = (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2))) |
57 | 24 | abscli 15240 |
. . . . . . . . 9
β’
(absβ(π΄ππ΅)) β β |
58 | 57 | resqcli 14044 |
. . . . . . . 8
β’
((absβ(π΄ππ΅))β2) β β |
59 | 58, 35 | redivclzi 11879 |
. . . . . . 7
β’ (((πβπ΅)β2) β 0 β (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2)) β β) |
60 | 32, 59 | sylbir 234 |
. . . . . 6
β’ (π΅ β
(0vecβπ)
β (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2)) β β) |
61 | 56, 60 | eqeltrd 2838 |
. . . . 5
β’ (π΅ β
(0vecβπ)
β (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅)) β β) |
62 | 30 | necon3bii 2994 |
. . . . . . . 8
β’ ((πβπ΅) β 0 β π΅ β (0vecβπ)) |
63 | 19 | sqgt0i 14045 |
. . . . . . . 8
β’ ((πβπ΅) β 0 β 0 < ((πβπ΅)β2)) |
64 | 62, 63 | sylbir 234 |
. . . . . . 7
β’ (π΅ β
(0vecβπ)
β 0 < ((πβπ΅)β2)) |
65 | 57 | sqge0i 14046 |
. . . . . . . 8
β’ 0 β€
((absβ(π΄ππ΅))β2) |
66 | | divge0 11982 |
. . . . . . . 8
β’
(((((absβ(π΄ππ΅))β2) β β β§ 0 β€
((absβ(π΄ππ΅))β2)) β§ (((πβπ΅)β2) β β β§ 0 <
((πβπ΅)β2))) β 0 β€
(((absβ(π΄ππ΅))β2) / ((πβπ΅)β2))) |
67 | 58, 65, 66 | mpanl12 700 |
. . . . . . 7
β’ ((((πβπ΅)β2) β β β§ 0 <
((πβπ΅)β2)) β 0 β€ (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2))) |
68 | 35, 64, 67 | sylancr 587 |
. . . . . 6
β’ (π΅ β
(0vecβπ)
β 0 β€ (((absβ(π΄ππ΅))β2) / ((πβπ΅)β2))) |
69 | 68, 56 | breqtrrd 5131 |
. . . . 5
β’ (π΅ β
(0vecβπ)
β 0 β€ (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) |
70 | | eqid 2737 |
. . . . . 6
β’ (
βπ£ βπ) = ( βπ£
βπ) |
71 | | eqid 2737 |
. . . . . 6
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
72 | 5, 12, 7, 2, 4, 15,
70, 71 | siilem2 29623 |
. . . . 5
β’ ((((π΅ππ΄) / ((πβπ΅)β2)) β β β§ (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅)) β β β§ 0 β€ (((π΅ππ΄) / ((πβπ΅)β2)) Β· (π΄ππ΅))) β ((π΅ππ΄) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) |
73 | 47, 61, 69, 72 | syl3anc 1371 |
. . . 4
β’ (π΅ β
(0vecβπ)
β ((π΅ππ΄) = (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) |
74 | 45, 73 | mpd 15 |
. . 3
β’ (π΅ β
(0vecβπ)
β (ββ((π΄ππ΅) Β· (((π΅ππ΄) / ((πβπ΅)β2)) Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅))) |
75 | 44, 74 | eqbrtrd 5125 |
. 2
β’ (π΅ β
(0vecβπ)
β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) |
76 | 22, 75 | pm2.61ine 3026 |
1
β’
(absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅)) |