Step | Hyp | Ref
| Expression |
1 | | 2rp 12925 |
. . 3
β’ 2 β
β+ |
2 | 1 | a1i 11 |
. 2
β’ ((π β NrmCVec β§ π΄ β π) β 2 β
β+) |
3 | | nvge0.1 |
. . 3
β’ π = (BaseSetβπ) |
4 | | nvge0.6 |
. . 3
β’ π =
(normCVβπ) |
5 | 3, 4 | nvcl 29645 |
. 2
β’ ((π β NrmCVec β§ π΄ β π) β (πβπ΄) β β) |
6 | | eqid 2733 |
. . . . . . 7
β’
(0vecβπ) = (0vecβπ) |
7 | 6, 4 | nvz0 29652 |
. . . . . 6
β’ (π β NrmCVec β (πβ(0vecβπ)) = 0) |
8 | 7 | adantr 482 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (πβ(0vecβπ)) = 0) |
9 | | 1pneg1e0 12277 |
. . . . . . . . 9
β’ (1 + -1)
= 0 |
10 | 9 | oveq1i 7368 |
. . . . . . . 8
β’ ((1 +
-1)( Β·π OLD βπ)π΄) = (0(
Β·π OLD βπ)π΄) |
11 | | eqid 2733 |
. . . . . . . . 9
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
12 | 3, 11, 6 | nv0 29621 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (0(
Β·π OLD βπ)π΄) = (0vecβπ)) |
13 | 10, 12 | eqtr2id 2786 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β (0vecβπ) = ((1 + -1)(
Β·π OLD βπ)π΄)) |
14 | | neg1cn 12272 |
. . . . . . . 8
β’ -1 β
β |
15 | | ax-1cn 11114 |
. . . . . . . . 9
β’ 1 β
β |
16 | | eqid 2733 |
. . . . . . . . . 10
β’ (
+π£ βπ) = ( +π£ βπ) |
17 | 3, 16, 11 | nvdir 29615 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ (1 β
β β§ -1 β β β§ π΄ β π)) β ((1 + -1)(
Β·π OLD βπ)π΄) = ((1(
Β·π OLD βπ)π΄)( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) |
18 | 15, 17 | mp3anr1 1459 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (-1 β
β β§ π΄ β
π)) β ((1 + -1)(
Β·π OLD βπ)π΄) = ((1(
Β·π OLD βπ)π΄)( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) |
19 | 14, 18 | mpanr1 702 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β ((1 + -1)(
Β·π OLD βπ)π΄) = ((1(
Β·π OLD βπ)π΄)( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) |
20 | 3, 11 | nvsid 29611 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (1(
Β·π OLD βπ)π΄) = π΄) |
21 | 20 | oveq1d 7373 |
. . . . . . 7
β’ ((π β NrmCVec β§ π΄ β π) β ((1(
Β·π OLD βπ)π΄)( +π£ βπ)(-1(
Β·π OLD βπ)π΄)) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) |
22 | 13, 19, 21 | 3eqtrd 2777 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π) β (0vecβπ) = (π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) |
23 | 22 | fveq2d 6847 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (πβ(0vecβπ)) = (πβ(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))) |
24 | 8, 23 | eqtr3d 2775 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β 0 = (πβ(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄)))) |
25 | 3, 11 | nvscl 29610 |
. . . . . 6
β’ ((π β NrmCVec β§ -1 β
β β§ π΄ β
π) β (-1(
Β·π OLD βπ)π΄) β π) |
26 | 14, 25 | mp3an2 1450 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (-1(
Β·π OLD βπ)π΄) β π) |
27 | 3, 16, 4 | nvtri 29654 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ (-1(
Β·π OLD βπ)π΄) β π) β (πβ(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) β€ ((πβπ΄) + (πβ(-1(
Β·π OLD βπ)π΄)))) |
28 | 26, 27 | mpd3an3 1463 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β (πβ(π΄( +π£ βπ)(-1(
Β·π OLD βπ)π΄))) β€ ((πβπ΄) + (πβ(-1(
Β·π OLD βπ)π΄)))) |
29 | 24, 28 | eqbrtrd 5128 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π) β 0 β€ ((πβπ΄) + (πβ(-1(
Β·π OLD βπ)π΄)))) |
30 | 3, 11, 4 | nvm1 29649 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (πβ(-1(
Β·π OLD βπ)π΄)) = (πβπ΄)) |
31 | 30 | oveq2d 7374 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β ((πβπ΄) + (πβ(-1(
Β·π OLD βπ)π΄))) = ((πβπ΄) + (πβπ΄))) |
32 | 5 | recnd 11188 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π) β (πβπ΄) β β) |
33 | 32 | 2timesd 12401 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β (2 Β· (πβπ΄)) = ((πβπ΄) + (πβπ΄))) |
34 | 31, 33 | eqtr4d 2776 |
. . 3
β’ ((π β NrmCVec β§ π΄ β π) β ((πβπ΄) + (πβ(-1(
Β·π OLD βπ)π΄))) = (2 Β· (πβπ΄))) |
35 | 29, 34 | breqtrd 5132 |
. 2
β’ ((π β NrmCVec β§ π΄ β π) β 0 β€ (2 Β· (πβπ΄))) |
36 | 2, 5, 35 | prodge0rd 13027 |
1
β’ ((π β NrmCVec β§ π΄ β π) β 0 β€ (πβπ΄)) |