Step | Hyp | Ref
| Expression |
1 | | pjthlem.1 |
. . . 4
β’ (π β π β βHil) |
2 | | hlcph 24765 |
. . . 4
β’ (π β βHil β π β
βPreHil) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β π β βPreHil) |
4 | | pjthlem.4 |
. . 3
β’ (π β π΄ β π) |
5 | | pjthlem.2 |
. . . . 5
β’ (π β π β πΏ) |
6 | | pjthlem.v |
. . . . . 6
β’ π = (Baseβπ) |
7 | | pjthlem.l |
. . . . . 6
β’ πΏ = (LSubSpβπ) |
8 | 6, 7 | lssss 20454 |
. . . . 5
β’ (π β πΏ β π β π) |
9 | 5, 8 | syl 17 |
. . . 4
β’ (π β π β π) |
10 | | pjthlem.5 |
. . . 4
β’ (π β π΅ β π) |
11 | 9, 10 | sseldd 3948 |
. . 3
β’ (π β π΅ β π) |
12 | | pjthlem.h |
. . . 4
β’ , =
(Β·πβπ) |
13 | 6, 12 | cphipcl 24592 |
. . 3
β’ ((π β βPreHil β§
π΄ β π β§ π΅ β π) β (π΄ , π΅) β β) |
14 | 3, 4, 11, 13 | syl3anc 1371 |
. 2
β’ (π β (π΄ , π΅) β β) |
15 | 14 | abscld 15333 |
. . . 4
β’ (π β (absβ(π΄ , π΅)) β β) |
16 | 15 | recnd 11192 |
. . 3
β’ (π β (absβ(π΄ , π΅)) β β) |
17 | 15 | resqcld 14040 |
. . . . . . 7
β’ (π β ((absβ(π΄ , π΅))β2) β β) |
18 | 17 | renegcld 11591 |
. . . . . 6
β’ (π β -((absβ(π΄ , π΅))β2) β β) |
19 | 6, 12 | reipcl 24598 |
. . . . . . . . 9
β’ ((π β βPreHil β§
π΅ β π) β (π΅ , π΅) β β) |
20 | 3, 11, 19 | syl2anc 584 |
. . . . . . . 8
β’ (π β (π΅ , π΅) β β) |
21 | | 2re 12236 |
. . . . . . . 8
β’ 2 β
β |
22 | | readdcl 11143 |
. . . . . . . 8
β’ (((π΅ , π΅) β β β§ 2 β β)
β ((π΅ , π΅) + 2) β
β) |
23 | 20, 21, 22 | sylancl 586 |
. . . . . . 7
β’ (π β ((π΅ , π΅) + 2) β β) |
24 | | 0red 11167 |
. . . . . . . 8
β’ (π β 0 β
β) |
25 | | peano2re 11337 |
. . . . . . . . 9
β’ ((π΅ , π΅) β β β ((π΅ , π΅) + 1) β β) |
26 | 20, 25 | syl 17 |
. . . . . . . 8
β’ (π β ((π΅ , π΅) + 1) β β) |
27 | 6, 12 | ipge0 24599 |
. . . . . . . . . 10
β’ ((π β βPreHil β§
π΅ β π) β 0 β€ (π΅ , π΅)) |
28 | 3, 11, 27 | syl2anc 584 |
. . . . . . . . 9
β’ (π β 0 β€ (π΅ , π΅)) |
29 | 20 | ltp1d 12094 |
. . . . . . . . 9
β’ (π β (π΅ , π΅) < ((π΅ , π΅) + 1)) |
30 | 24, 20, 26, 28, 29 | lelttrd 11322 |
. . . . . . . 8
β’ (π β 0 < ((π΅ , π΅) + 1)) |
31 | 26 | ltp1d 12094 |
. . . . . . . . 9
β’ (π β ((π΅ , π΅) + 1) < (((π΅ , π΅) + 1) + 1)) |
32 | | df-2 12225 |
. . . . . . . . . . 11
β’ 2 = (1 +
1) |
33 | 32 | oveq2i 7373 |
. . . . . . . . . 10
β’ ((π΅ , π΅) + 2) = ((π΅ , π΅) + (1 + 1)) |
34 | 20 | recnd 11192 |
. . . . . . . . . . 11
β’ (π β (π΅ , π΅) β β) |
35 | | ax-1cn 11118 |
. . . . . . . . . . . 12
β’ 1 β
β |
36 | | addass 11147 |
. . . . . . . . . . . 12
β’ (((π΅ , π΅) β β β§ 1 β β
β§ 1 β β) β (((π΅ , π΅) + 1) + 1) = ((π΅ , π΅) + (1 + 1))) |
37 | 35, 35, 36 | mp3an23 1453 |
. . . . . . . . . . 11
β’ ((π΅ , π΅) β β β (((π΅ , π΅) + 1) + 1) = ((π΅ , π΅) + (1 + 1))) |
38 | 34, 37 | syl 17 |
. . . . . . . . . 10
β’ (π β (((π΅ , π΅) + 1) + 1) = ((π΅ , π΅) + (1 + 1))) |
39 | 33, 38 | eqtr4id 2790 |
. . . . . . . . 9
β’ (π β ((π΅ , π΅) + 2) = (((π΅ , π΅) + 1) + 1)) |
40 | 31, 39 | breqtrrd 5138 |
. . . . . . . 8
β’ (π β ((π΅ , π΅) + 1) < ((π΅ , π΅) + 2)) |
41 | 24, 26, 23, 30, 40 | lttrd 11325 |
. . . . . . 7
β’ (π β 0 < ((π΅ , π΅) + 2)) |
42 | 23, 41 | elrpd 12963 |
. . . . . 6
β’ (π β ((π΅ , π΅) + 2) β
β+) |
43 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π( Β·π
βπ)π΅) β (π΄ β π₯) = (π΄ β (π( Β·π
βπ)π΅))) |
44 | 43 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π₯ = (π( Β·π
βπ)π΅) β (πβ(π΄ β π₯)) = (πβ(π΄ β (π( Β·π
βπ)π΅)))) |
45 | 44 | breq2d 5122 |
. . . . . . . . . . . 12
β’ (π₯ = (π( Β·π
βπ)π΅) β ((πβπ΄) β€ (πβ(π΄ β π₯)) β (πβπ΄) β€ (πβ(π΄ β (π( Β·π
βπ)π΅))))) |
46 | | pjthlem.7 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β π (πβπ΄) β€ (πβ(π΄ β π₯))) |
47 | | cphlmod 24575 |
. . . . . . . . . . . . . 14
β’ (π β βPreHil β
π β
LMod) |
48 | 3, 47 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β LMod) |
49 | | pjthlem.8 |
. . . . . . . . . . . . . 14
β’ π = ((π΄ , π΅) / ((π΅ , π΅) + 1)) |
50 | | hlphl 24766 |
. . . . . . . . . . . . . . . . 17
β’ (π β βHil β π β PreHil) |
51 | 1, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β PreHil) |
52 | | eqid 2731 |
. . . . . . . . . . . . . . . . 17
β’
(Scalarβπ) =
(Scalarβπ) |
53 | | eqid 2731 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
54 | 52, 12, 6, 53 | ipcl 21074 |
. . . . . . . . . . . . . . . 16
β’ ((π β PreHil β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) β (Baseβ(Scalarβπ))) |
55 | 51, 4, 11, 54 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ , π΅) β (Baseβ(Scalarβπ))) |
56 | 52, 53 | hlress 24769 |
. . . . . . . . . . . . . . . . 17
β’ (π β βHil β
β β (Baseβ(Scalarβπ))) |
57 | 1, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(Baseβ(Scalarβπ))) |
58 | 57, 26 | sseldd 3948 |
. . . . . . . . . . . . . . 15
β’ (π β ((π΅ , π΅) + 1) β
(Baseβ(Scalarβπ))) |
59 | 20, 28 | ge0p1rpd 12996 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΅ , π΅) + 1) β
β+) |
60 | 59 | rpne0d 12971 |
. . . . . . . . . . . . . . 15
β’ (π β ((π΅ , π΅) + 1) β 0) |
61 | 52, 53 | cphdivcl 24583 |
. . . . . . . . . . . . . . 15
β’ ((π β βPreHil β§
((π΄ , π΅) β (Baseβ(Scalarβπ)) β§ ((π΅ , π΅) + 1) β
(Baseβ(Scalarβπ)) β§ ((π΅ , π΅) + 1) β 0)) β ((π΄ , π΅) / ((π΅ , π΅) + 1)) β
(Baseβ(Scalarβπ))) |
62 | 3, 55, 58, 60, 61 | syl13anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄ , π΅) / ((π΅ , π΅) + 1)) β
(Baseβ(Scalarβπ))) |
63 | 49, 62 | eqeltrid 2836 |
. . . . . . . . . . . . 13
β’ (π β π β (Baseβ(Scalarβπ))) |
64 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’ (
Β·π βπ) = ( Β·π
βπ) |
65 | 52, 64, 53, 7 | lssvscl 20473 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β πΏ) β§ (π β (Baseβ(Scalarβπ)) β§ π΅ β π)) β (π( Β·π
βπ)π΅) β π) |
66 | 48, 5, 63, 10, 65 | syl22anc 837 |
. . . . . . . . . . . 12
β’ (π β (π( Β·π
βπ)π΅) β π) |
67 | 45, 46, 66 | rspcdva 3583 |
. . . . . . . . . . 11
β’ (π β (πβπ΄) β€ (πβ(π΄ β (π( Β·π
βπ)π΅)))) |
68 | | cphngp 24574 |
. . . . . . . . . . . . . 14
β’ (π β βPreHil β
π β
NrmGrp) |
69 | 3, 68 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β NrmGrp) |
70 | | pjthlem.n |
. . . . . . . . . . . . . 14
β’ π = (normβπ) |
71 | 6, 70 | nmcl 24009 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ π΄ β π) β (πβπ΄) β β) |
72 | 69, 4, 71 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β (πβπ΄) β β) |
73 | 6, 52, 64, 53 | lmodvscl 20396 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ π΅ β π) β (π( Β·π
βπ)π΅) β π) |
74 | 48, 63, 11, 73 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ (π β (π( Β·π
βπ)π΅) β π) |
75 | | pjthlem.m |
. . . . . . . . . . . . . . 15
β’ β =
(-gβπ) |
76 | 6, 75 | lmodvsubcl 20424 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π΄ β π β§ (π( Β·π
βπ)π΅) β π) β (π΄ β (π( Β·π
βπ)π΅)) β π) |
77 | 48, 4, 74, 76 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β (π( Β·π
βπ)π΅)) β π) |
78 | 6, 70 | nmcl 24009 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ (π΄ β (π( Β·π
βπ)π΅)) β π) β (πβ(π΄ β (π( Β·π
βπ)π΅))) β β) |
79 | 69, 77, 78 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β (πβ(π΄ β (π( Β·π
βπ)π΅))) β β) |
80 | 6, 70 | nmge0 24010 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ π΄ β π) β 0 β€ (πβπ΄)) |
81 | 69, 4, 80 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πβπ΄)) |
82 | 6, 70 | nmge0 24010 |
. . . . . . . . . . . . 13
β’ ((π β NrmGrp β§ (π΄ β (π( Β·π
βπ)π΅)) β π) β 0 β€ (πβ(π΄ β (π( Β·π
βπ)π΅)))) |
83 | 69, 77, 82 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (π β 0 β€ (πβ(π΄ β (π( Β·π
βπ)π΅)))) |
84 | 72, 79, 81, 83 | le2sqd 14170 |
. . . . . . . . . . 11
β’ (π β ((πβπ΄) β€ (πβ(π΄ β (π( Β·π
βπ)π΅))) β ((πβπ΄)β2) β€ ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2))) |
85 | 67, 84 | mpbid 231 |
. . . . . . . . . 10
β’ (π β ((πβπ΄)β2) β€ ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2)) |
86 | 79 | resqcld 14040 |
. . . . . . . . . . 11
β’ (π β ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) β β) |
87 | 72 | resqcld 14040 |
. . . . . . . . . . 11
β’ (π β ((πβπ΄)β2) β β) |
88 | 86, 87 | subge0d 11754 |
. . . . . . . . . 10
β’ (π β (0 β€ (((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) β ((πβπ΄)β2)) β ((πβπ΄)β2) β€ ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2))) |
89 | 85, 88 | mpbird 256 |
. . . . . . . . 9
β’ (π β 0 β€ (((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) β ((πβπ΄)β2))) |
90 | | 2z 12544 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β€ |
91 | | rpexpcl 13996 |
. . . . . . . . . . . . . . . 16
β’ ((((π΅ , π΅) + 1) β β+ β§ 2
β β€) β (((π΅
, π΅) + 1)β2) β
β+) |
92 | 59, 90, 91 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ (π β (((π΅ , π΅) + 1)β2) β
β+) |
93 | 17, 92 | rerpdivcld 12997 |
. . . . . . . . . . . . . 14
β’ (π β (((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) β
β) |
94 | 93, 23 | remulcld 11194 |
. . . . . . . . . . . . 13
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) β β) |
95 | 94 | recnd 11192 |
. . . . . . . . . . . 12
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) β β) |
96 | 95 | negcld 11508 |
. . . . . . . . . . 11
β’ (π β -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) β β) |
97 | 6, 12 | cphipcl 24592 |
. . . . . . . . . . . 12
β’ ((π β βPreHil β§
π΄ β π β§ π΄ β π) β (π΄ , π΄) β β) |
98 | 3, 4, 4, 97 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β (π΄ , π΄) β β) |
99 | 96, 98 | pncand 11522 |
. . . . . . . . . 10
β’ (π β ((-((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) + (π΄ , π΄)) β (π΄ , π΄)) = -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) |
100 | 6, 12, 70 | nmsq 24595 |
. . . . . . . . . . . . . 14
β’ ((π β βPreHil β§
(π΄ β (π( Β·π
βπ)π΅)) β π) β ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) = ((π΄ β (π( Β·π
βπ)π΅)) , (π΄ β (π( Β·π
βπ)π΅)))) |
101 | 3, 77, 100 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (π β ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) = ((π΄ β (π( Β·π
βπ)π΅)) , (π΄ β (π( Β·π
βπ)π΅)))) |
102 | 12, 6, 75 | cphsubdir 24609 |
. . . . . . . . . . . . . 14
β’ ((π β βPreHil β§
(π΄ β π β§ (π( Β·π
βπ)π΅) β π β§ (π΄ β (π( Β·π
βπ)π΅)) β π)) β ((π΄ β (π( Β·π
βπ)π΅)) , (π΄ β (π( Β·π
βπ)π΅))) = ((π΄ , (π΄ β (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))))) |
103 | 3, 4, 74, 77, 102 | syl13anc 1372 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ β (π( Β·π
βπ)π΅)) , (π΄ β (π( Β·π
βπ)π΅))) = ((π΄ , (π΄ β (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))))) |
104 | 12, 6, 75 | cphsubdi 24610 |
. . . . . . . . . . . . . . . 16
β’ ((π β βPreHil β§
(π΄ β π β§ π΄ β π β§ (π( Β·π
βπ)π΅) β π)) β (π΄ , (π΄ β (π( Β·π
βπ)π΅))) = ((π΄ , π΄) β (π΄ , (π( Β·π
βπ)π΅)))) |
105 | 3, 4, 4, 74, 104 | syl13anc 1372 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ , (π΄ β (π( Β·π
βπ)π΅))) = ((π΄ , π΄) β (π΄ , (π( Β·π
βπ)π΅)))) |
106 | 105 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄ , (π΄ β (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))) = (((π΄ , π΄) β (π΄ , (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))))) |
107 | 6, 12 | cphipcl 24592 |
. . . . . . . . . . . . . . . 16
β’ ((π β βPreHil β§
π΄ β π β§ (π( Β·π
βπ)π΅) β π) β (π΄ , (π( Β·π
βπ)π΅)) β β) |
108 | 3, 4, 74, 107 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ , (π( Β·π
βπ)π΅)) β β) |
109 | 12, 6, 75 | cphsubdi 24610 |
. . . . . . . . . . . . . . . . 17
β’ ((π β βPreHil β§
((π(
Β·π βπ)π΅) β π β§ π΄ β π β§ (π( Β·π
βπ)π΅) β π)) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))) = (((π( Β·π
βπ)π΅) , π΄) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)))) |
110 | 3, 74, 4, 74, 109 | syl13anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))) = (((π( Β·π
βπ)π΅) , π΄) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)))) |
111 | 6, 12 | cphipcl 24592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β βPreHil β§
(π(
Β·π βπ)π΅) β π β§ π΄ β π) β ((π( Β·π
βπ)π΅) , π΄) β β) |
112 | 3, 74, 4, 111 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π( Β·π
βπ)π΅) , π΄) β β) |
113 | 6, 12 | cphipcl 24592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β βPreHil β§
(π(
Β·π βπ)π΅) β π β§ (π( Β·π
βπ)π΅) β π) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)) β β) |
114 | 3, 74, 74, 113 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)) β β) |
115 | 112, 114 | subcld 11521 |
. . . . . . . . . . . . . . . 16
β’ (π β (((π( Β·π
βπ)π΅) , π΄) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅))) β β) |
116 | 110, 115 | eqeltrd 2832 |
. . . . . . . . . . . . . . 15
β’ (π β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))) β β) |
117 | 98, 108, 116 | subsub4d 11552 |
. . . . . . . . . . . . . 14
β’ (π β (((π΄ , π΄) β (π΄ , (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))) = ((π΄ , π΄) β ((π΄ , (π( Β·π
βπ)π΅)) + ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))))) |
118 | 93 | recnd 11192 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) β
β) |
119 | 26 | recnd 11192 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π΅ , π΅) + 1) β β) |
120 | | 1cnd 11159 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β
β) |
121 | 118, 119,
120 | adddid 11188 |
. . . . . . . . . . . . . . . 16
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (((π΅ , π΅) + 1) + 1)) = (((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) + ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β·
1))) |
122 | 39 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (((π΅ , π΅) + 1) + 1))) |
123 | 12, 6, 52, 53, 64 | cphassr 24613 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β βPreHil β§
(π β
(Baseβ(Scalarβπ)) β§ π΄ β π β§ π΅ β π)) β (π΄ , (π( Β·π
βπ)π΅)) = ((ββπ) Β· (π΄ , π΅))) |
124 | 3, 63, 4, 11, 123 | syl13anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π΄ , (π( Β·π
βπ)π΅)) = ((ββπ) Β· (π΄ , π΅))) |
125 | 14, 119, 60 | divcld 11940 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((π΄ , π΅) / ((π΅ , π΅) + 1)) β β) |
126 | 49, 125 | eqeltrid 2836 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
127 | 126 | cjcld 15093 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ββπ) β
β) |
128 | 127, 14 | mulcomd 11185 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((ββπ) Β· (π΄ , π΅)) = ((π΄ , π΅) Β· (ββπ))) |
129 | 14 | cjcld 15093 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (ββ(π΄ , π΅)) β β) |
130 | 14, 129, 119, 60 | divassd 11975 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π΄ , π΅) Β· (ββ(π΄ , π΅))) / ((π΅ , π΅) + 1)) = ((π΄ , π΅) Β· ((ββ(π΄ , π΅)) / ((π΅ , π΅) + 1)))) |
131 | 14 | absvalsqd 15339 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((absβ(π΄ , π΅))β2) = ((π΄ , π΅) Β· (ββ(π΄ , π΅)))) |
132 | 131 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((absβ(π΄ , π΅))β2) / ((π΅ , π΅) + 1)) = (((π΄ , π΅) Β· (ββ(π΄ , π΅))) / ((π΅ , π΅) + 1))) |
133 | 49 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(ββπ) =
(ββ((π΄ , π΅) / ((π΅ , π΅) + 1))) |
134 | 14, 119, 60 | cjdivd 15120 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (ββ((π΄ , π΅) / ((π΅ , π΅) + 1))) = ((ββ(π΄ , π΅)) / (ββ((π΅ , π΅) + 1)))) |
135 | 26 | cjred 15123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (ββ((π΅ , π΅) + 1)) = ((π΅ , π΅) + 1)) |
136 | 135 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((ββ(π΄ , π΅)) / (ββ((π΅ , π΅) + 1))) = ((ββ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
137 | 134, 136 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (ββ((π΄ , π΅) / ((π΅ , π΅) + 1))) = ((ββ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
138 | 133, 137 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (ββπ) = ((ββ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
139 | 138 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π΄ , π΅) Β· (ββπ)) = ((π΄ , π΅) Β· ((ββ(π΄ , π΅)) / ((π΅ , π΅) + 1)))) |
140 | 130, 132,
139 | 3eqtr4rd 2782 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π΄ , π΅) Β· (ββπ)) = (((absβ(π΄ , π΅))β2) / ((π΅ , π΅) + 1))) |
141 | 124, 128,
140 | 3eqtrd 2775 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ , (π( Β·π
βπ)π΅)) = (((absβ(π΄ , π΅))β2) / ((π΅ , π΅) + 1))) |
142 | 17 | recnd 11192 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β ((absβ(π΄ , π΅))β2) β β) |
143 | 142, 119 | mulcomd 11185 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 1)) = (((π΅ , π΅) + 1) Β· ((absβ(π΄ , π΅))β2))) |
144 | 119 | sqvald 14058 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π΅ , π΅) + 1)β2) = (((π΅ , π΅) + 1) Β· ((π΅ , π΅) + 1))) |
145 | 143, 144 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 1)) / (((π΅ , π΅) + 1)β2)) = ((((π΅ , π΅) + 1) Β· ((absβ(π΄ , π΅))β2)) / (((π΅ , π΅) + 1) Β· ((π΅ , π΅) + 1)))) |
146 | 142, 119,
119, 60, 60 | divcan5d 11966 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((π΅ , π΅) + 1) Β· ((absβ(π΄ , π΅))β2)) / (((π΅ , π΅) + 1) Β· ((π΅ , π΅) + 1))) = (((absβ(π΄ , π΅))β2) / ((π΅ , π΅) + 1))) |
147 | 145, 146 | eqtr2d 2772 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((absβ(π΄ , π΅))β2) / ((π΅ , π΅) + 1)) = ((((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 1)) / (((π΅ , π΅) + 1)β2))) |
148 | 92 | rpcnd 12968 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((π΅ , π΅) + 1)β2) β
β) |
149 | 92 | rpne0d 12971 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (((π΅ , π΅) + 1)β2) β 0) |
150 | 142, 119,
148, 149 | div23d 11977 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 1)) / (((π΅ , π΅) + 1)β2)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1))) |
151 | 141, 147,
150 | 3eqtrd 2775 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ , (π( Β·π
βπ)π΅)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1))) |
152 | 93, 26 | remulcld 11194 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) β β) |
153 | 151, 152 | eqeltrd 2832 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄ , (π( Β·π
βπ)π΅)) β β) |
154 | 153 | cjred 15123 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ββ(π΄ , (π( Β·π
βπ)π΅))) = (π΄ , (π( Β·π
βπ)π΅))) |
155 | 12, 6 | cphipcj 24600 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β βPreHil β§
π΄ β π β§ (π( Β·π
βπ)π΅) β π) β (ββ(π΄ , (π( Β·π
βπ)π΅))) = ((π( Β·π
βπ)π΅) , π΄)) |
156 | 3, 4, 74, 155 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (ββ(π΄ , (π( Β·π
βπ)π΅))) = ((π( Β·π
βπ)π΅) , π΄)) |
157 | 154, 156,
151 | 3eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π( Β·π
βπ)π΅) , π΄) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1))) |
158 | 12, 6, 52, 53, 64 | cph2ass 24614 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β βPreHil β§
(π β
(Baseβ(Scalarβπ)) β§ π β (Baseβ(Scalarβπ))) β§ (π΅ β π β§ π΅ β π)) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)) = ((π Β· (ββπ)) Β· (π΅ , π΅))) |
159 | 3, 63, 63, 11, 11, 158 | syl122anc 1379 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)) = ((π Β· (ββπ)) Β· (π΅ , π΅))) |
160 | 49 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(absβπ) =
(absβ((π΄ , π΅) / ((π΅ , π΅) + 1))) |
161 | 14, 119, 60 | absdivd 15352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (absβ((π΄ , π΅) / ((π΅ , π΅) + 1))) = ((absβ(π΄ , π΅)) / (absβ((π΅ , π΅) + 1)))) |
162 | 59 | rpge0d 12970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β 0 β€ ((π΅ , π΅) + 1)) |
163 | 26, 162 | absidd 15319 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (absβ((π΅ , π΅) + 1)) = ((π΅ , π΅) + 1)) |
164 | 163 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β ((absβ(π΄ , π΅)) / (absβ((π΅ , π΅) + 1))) = ((absβ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
165 | 161, 164 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (absβ((π΄ , π΅) / ((π΅ , π΅) + 1))) = ((absβ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
166 | 160, 165 | eqtrid 2783 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (absβπ) = ((absβ(π΄ , π΅)) / ((π΅ , π΅) + 1))) |
167 | 166 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((absβπ)β2) = (((absβ(π΄ , π΅)) / ((π΅ , π΅) + 1))β2)) |
168 | 126 | absvalsqd 15339 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((absβπ)β2) = (π Β· (ββπ))) |
169 | 16, 119, 60 | sqdivd 14074 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (((absβ(π΄ , π΅)) / ((π΅ , π΅) + 1))β2) = (((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2))) |
170 | 167, 168,
169 | 3eqtr3d 2779 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π Β· (ββπ)) = (((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2))) |
171 | 170 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((π Β· (ββπ)) Β· (π΅ , π΅)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (π΅ , π΅))) |
172 | 159, 171 | eqtrd 2771 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (π΅ , π΅))) |
173 | 157, 172 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (((π( Β·π
βπ)π΅) , π΄) β ((π( Β·π
βπ)π΅) , (π( Β·π
βπ)π΅))) = (((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (π΅ , π΅)))) |
174 | | pncan2 11417 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π΅ , π΅) β β β§ 1 β β)
β (((π΅ , π΅) + 1) β (π΅ , π΅)) = 1) |
175 | 34, 35, 174 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (((π΅ , π΅) + 1) β (π΅ , π΅)) = 1) |
176 | 175 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (((π΅ , π΅) + 1) β (π΅ , π΅))) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β·
1)) |
177 | 118, 119,
34 | subdid 11620 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (((π΅ , π΅) + 1) β (π΅ , π΅))) = (((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (π΅ , π΅)))) |
178 | 176, 177 | eqtr3d 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· 1) =
(((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· (π΅ , π΅)))) |
179 | 173, 110,
178 | 3eqtr4d 2781 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β·
1)) |
180 | 151, 179 | oveq12d 7380 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΄ , (π( Β·π
βπ)π΅)) + ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))) = (((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 1)) + ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β·
1))) |
181 | 121, 122,
180 | 3eqtr4rd 2782 |
. . . . . . . . . . . . . . 15
β’ (π β ((π΄ , (π( Β·π
βπ)π΅)) + ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) |
182 | 181 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄ , π΄) β ((π΄ , (π( Β·π
βπ)π΅)) + ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅))))) = ((π΄ , π΄) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)))) |
183 | 106, 117,
182 | 3eqtrd 2775 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ , (π΄ β (π( Β·π
βπ)π΅))) β ((π( Β·π
βπ)π΅) , (π΄ β (π( Β·π
βπ)π΅)))) = ((π΄ , π΄) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)))) |
184 | 101, 103,
183 | 3eqtrd 2775 |
. . . . . . . . . . . 12
β’ (π β ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) = ((π΄ , π΄) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)))) |
185 | 98, 95 | negsubd 11527 |
. . . . . . . . . . . 12
β’ (π β ((π΄ , π΄) + -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) = ((π΄ , π΄) β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)))) |
186 | 98, 96 | addcomd 11366 |
. . . . . . . . . . . 12
β’ (π β ((π΄ , π΄) + -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) = (-((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) + (π΄ , π΄))) |
187 | 184, 185,
186 | 3eqtr2d 2777 |
. . . . . . . . . . 11
β’ (π β ((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) = (-((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) + (π΄ , π΄))) |
188 | 6, 12, 70 | nmsq 24595 |
. . . . . . . . . . . 12
β’ ((π β βPreHil β§
π΄ β π) β ((πβπ΄)β2) = (π΄ , π΄)) |
189 | 3, 4, 188 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β ((πβπ΄)β2) = (π΄ , π΄)) |
190 | 187, 189 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π β (((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) β ((πβπ΄)β2)) = ((-((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2)) + (π΄ , π΄)) β (π΄ , π΄))) |
191 | 23 | renegcld 11591 |
. . . . . . . . . . . . 13
β’ (π β -((π΅ , π΅) + 2) β β) |
192 | 191 | recnd 11192 |
. . . . . . . . . . . 12
β’ (π β -((π΅ , π΅) + 2) β β) |
193 | 142, 192,
148, 149 | div23d 11977 |
. . . . . . . . . . 11
β’ (π β ((((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) / (((π΅ , π΅) + 1)β2)) = ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· -((π΅ , π΅) + 2))) |
194 | 23 | recnd 11192 |
. . . . . . . . . . . 12
β’ (π β ((π΅ , π΅) + 2) β β) |
195 | 118, 194 | mulneg2d 11618 |
. . . . . . . . . . 11
β’ (π β ((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· -((π΅ , π΅) + 2)) = -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) |
196 | 193, 195 | eqtrd 2771 |
. . . . . . . . . 10
β’ (π β ((((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) / (((π΅ , π΅) + 1)β2)) = -((((absβ(π΄ , π΅))β2) / (((π΅ , π΅) + 1)β2)) Β· ((π΅ , π΅) + 2))) |
197 | 99, 190, 196 | 3eqtr4rd 2782 |
. . . . . . . . 9
β’ (π β ((((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) / (((π΅ , π΅) + 1)β2)) = (((πβ(π΄ β (π( Β·π
βπ)π΅)))β2) β ((πβπ΄)β2))) |
198 | 89, 197 | breqtrrd 5138 |
. . . . . . . 8
β’ (π β 0 β€
((((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) / (((π΅ , π΅) + 1)β2))) |
199 | 17, 191 | remulcld 11194 |
. . . . . . . . 9
β’ (π β (((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) β β) |
200 | 199, 92 | ge0divd 13004 |
. . . . . . . 8
β’ (π β (0 β€
(((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) β 0 β€ ((((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2)) / (((π΅ , π΅) + 1)β2)))) |
201 | 198, 200 | mpbird 256 |
. . . . . . 7
β’ (π β 0 β€ (((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2))) |
202 | | mulneg12 11602 |
. . . . . . . 8
β’
((((absβ(π΄
, π΅))β2) β β β§
((π΅ , π΅) + 2) β β) β
(-((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 2)) = (((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2))) |
203 | 142, 194,
202 | syl2anc 584 |
. . . . . . 7
β’ (π β (-((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 2)) = (((absβ(π΄ , π΅))β2) Β· -((π΅ , π΅) + 2))) |
204 | 201, 203 | breqtrrd 5138 |
. . . . . 6
β’ (π β 0 β€
(-((absβ(π΄ , π΅))β2) Β· ((π΅ , π΅) + 2))) |
205 | 18, 42, 204 | prodge0ld 13032 |
. . . . 5
β’ (π β 0 β€ -((absβ(π΄ , π΅))β2)) |
206 | 17 | le0neg1d 11735 |
. . . . 5
β’ (π β (((absβ(π΄ , π΅))β2) β€ 0 β 0 β€
-((absβ(π΄ , π΅))β2))) |
207 | 205, 206 | mpbird 256 |
. . . 4
β’ (π β ((absβ(π΄ , π΅))β2) β€ 0) |
208 | 15 | sqge0d 14052 |
. . . 4
β’ (π β 0 β€ ((absβ(π΄ , π΅))β2)) |
209 | | 0re 11166 |
. . . . 5
β’ 0 β
β |
210 | | letri3 11249 |
. . . . 5
β’
((((absβ(π΄
, π΅))β2) β β β§
0 β β) β (((absβ(π΄ , π΅))β2) = 0 β (((absβ(π΄ , π΅))β2) β€ 0 β§ 0 β€
((absβ(π΄ , π΅))β2)))) |
211 | 17, 209, 210 | sylancl 586 |
. . . 4
β’ (π β (((absβ(π΄ , π΅))β2) = 0 β (((absβ(π΄ , π΅))β2) β€ 0 β§ 0 β€
((absβ(π΄ , π΅))β2)))) |
212 | 207, 208,
211 | mpbir2and 711 |
. . 3
β’ (π β ((absβ(π΄ , π΅))β2) = 0) |
213 | 16, 212 | sqeq0d 14060 |
. 2
β’ (π β (absβ(π΄ , π΅)) = 0) |
214 | 14, 213 | abs00d 15343 |
1
β’ (π β (π΄ , π΅) = 0) |