Step | Hyp | Ref
| Expression |
1 | | simpl1 1188 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΌ β (Fin β
{β
})) |
2 | 1 | eldifad 3955 |
. . 3
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΌ β Fin) |
3 | | simpl2 1189 |
. . 3
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΉ β π) |
4 | | simpl3 1190 |
. . 3
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΊ β π) |
5 | | rrnval.1 |
. . . 4
β’ π = (β βm
πΌ) |
6 | 5 | rrnmval 37209 |
. . 3
β’ ((πΌ β Fin β§ πΉ β π β§ πΊ β π) β (πΉ(βnβπΌ)πΊ) = (ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))) |
7 | 2, 3, 4, 6 | syl3anc 1368 |
. 2
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (πΉ(βnβπΌ)πΊ) = (ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))) |
8 | | eldifsni 4788 |
. . . . . 6
β’ (πΌ β (Fin β {β
})
β πΌ β
β
) |
9 | 1, 8 | syl 17 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΌ β β
) |
10 | 3, 5 | eleqtrdi 2837 |
. . . . . . . . 9
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΉ β (β βm πΌ)) |
11 | | elmapi 8845 |
. . . . . . . . 9
β’ (πΉ β (β
βm πΌ)
β πΉ:πΌβΆβ) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΉ:πΌβΆβ) |
13 | 12 | ffvelcdmda 7080 |
. . . . . . 7
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (πΉβπ) β β) |
14 | 4, 5 | eleqtrdi 2837 |
. . . . . . . . 9
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΊ β (β βm πΌ)) |
15 | | elmapi 8845 |
. . . . . . . . 9
β’ (πΊ β (β
βm πΌ)
β πΊ:πΌβΆβ) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β πΊ:πΌβΆβ) |
17 | 16 | ffvelcdmda 7080 |
. . . . . . 7
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (πΊβπ) β β) |
18 | 13, 17 | resubcld 11646 |
. . . . . 6
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((πΉβπ) β (πΊβπ)) β β) |
19 | 18 | resqcld 14095 |
. . . . 5
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) β β) |
20 | | simprl 768 |
. . . . . . . 8
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β π
β
β+) |
21 | 20 | rpred 13022 |
. . . . . . 7
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β π
β β) |
22 | 21 | resqcld 14095 |
. . . . . 6
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (π
β2) β β) |
23 | 22 | adantr 480 |
. . . . 5
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (π
β2) β β) |
24 | | absresq 15255 |
. . . . . . 7
β’ (((πΉβπ) β (πΊβπ)) β β β ((absβ((πΉβπ) β (πΊβπ)))β2) = (((πΉβπ) β (πΊβπ))β2)) |
25 | 18, 24 | syl 17 |
. . . . . 6
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((absβ((πΉβπ) β (πΊβπ)))β2) = (((πΉβπ) β (πΊβπ))β2)) |
26 | | rrndstprj1.1 |
. . . . . . . . . 10
β’ π = ((abs β β )
βΎ (β Γ β)) |
27 | 26 | remetdval 24660 |
. . . . . . . . 9
β’ (((πΉβπ) β β β§ (πΊβπ) β β) β ((πΉβπ)π(πΊβπ)) = (absβ((πΉβπ) β (πΊβπ)))) |
28 | 13, 17, 27 | syl2anc 583 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((πΉβπ)π(πΊβπ)) = (absβ((πΉβπ) β (πΊβπ)))) |
29 | | simprr 770 |
. . . . . . . . 9
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
) |
30 | | fveq2 6885 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
31 | | fveq2 6885 |
. . . . . . . . . . . 12
β’ (π = π β (πΊβπ) = (πΊβπ)) |
32 | 30, 31 | oveq12d 7423 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ)π(πΊβπ)) = ((πΉβπ)π(πΊβπ))) |
33 | 32 | breq1d 5151 |
. . . . . . . . . 10
β’ (π = π β (((πΉβπ)π(πΊβπ)) < π
β ((πΉβπ)π(πΊβπ)) < π
)) |
34 | 33 | rspccva 3605 |
. . . . . . . . 9
β’
((βπ β
πΌ ((πΉβπ)π(πΊβπ)) < π
β§ π β πΌ) β ((πΉβπ)π(πΊβπ)) < π
) |
35 | 29, 34 | sylan 579 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((πΉβπ)π(πΊβπ)) < π
) |
36 | 28, 35 | eqbrtrrd 5165 |
. . . . . . 7
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (absβ((πΉβπ) β (πΊβπ))) < π
) |
37 | 18 | recnd 11246 |
. . . . . . . . 9
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((πΉβπ) β (πΊβπ)) β β) |
38 | 37 | abscld 15389 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (absβ((πΉβπ) β (πΊβπ))) β β) |
39 | 21 | adantr 480 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β π
β β) |
40 | 37 | absge0d 15397 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β 0 β€ (absβ((πΉβπ) β (πΊβπ)))) |
41 | 20 | rpge0d 13026 |
. . . . . . . . 9
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β 0 β€ π
) |
42 | 41 | adantr 480 |
. . . . . . . 8
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β 0 β€ π
) |
43 | 38, 39, 40, 42 | lt2sqd 14224 |
. . . . . . 7
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((absβ((πΉβπ) β (πΊβπ))) < π
β ((absβ((πΉβπ) β (πΊβπ)))β2) < (π
β2))) |
44 | 36, 43 | mpbid 231 |
. . . . . 6
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β ((absβ((πΉβπ) β (πΊβπ)))β2) < (π
β2)) |
45 | 25, 44 | eqbrtrrd 5165 |
. . . . 5
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) < (π
β2)) |
46 | 2, 9, 19, 23, 45 | fsumlt 15752 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2) < Ξ£π β πΌ (π
β2)) |
47 | 2, 19 | fsumrecl 15686 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2) β β) |
48 | 18 | sqge0d 14107 |
. . . . . 6
β’ ((((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β§ π β πΌ) β 0 β€ (((πΉβπ) β (πΊβπ))β2)) |
49 | 2, 19, 48 | fsumge0 15747 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β 0 β€ Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) |
50 | | resqrtth 15208 |
. . . . 5
β’
((Ξ£π β
πΌ (((πΉβπ) β (πΊβπ))β2) β β β§ 0 β€
Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) β
((ββΞ£π
β πΌ (((πΉβπ) β (πΊβπ))β2))β2) = Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) |
51 | 47, 49, 50 | syl2anc 583 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))β2) = Ξ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) |
52 | | hashnncl 14331 |
. . . . . . . . . . . 12
β’ (πΌ β Fin β
((β―βπΌ) β
β β πΌ β
β
)) |
53 | 2, 52 | syl 17 |
. . . . . . . . . . 11
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((β―βπΌ) β β β πΌ β β
)) |
54 | 9, 53 | mpbird 257 |
. . . . . . . . . 10
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (β―βπΌ) β β) |
55 | 54 | nnrpd 13020 |
. . . . . . . . 9
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (β―βπΌ) β
β+) |
56 | 55 | rpred 13022 |
. . . . . . . 8
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (β―βπΌ) β β) |
57 | 55 | rpge0d 13026 |
. . . . . . . 8
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β 0 β€ (β―βπΌ)) |
58 | | resqrtth 15208 |
. . . . . . . 8
β’
(((β―βπΌ)
β β β§ 0 β€ (β―βπΌ)) β
((ββ(β―βπΌ))β2) = (β―βπΌ)) |
59 | 56, 57, 58 | syl2anc 583 |
. . . . . . 7
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β
((ββ(β―βπΌ))β2) = (β―βπΌ)) |
60 | 59 | oveq2d 7421 |
. . . . . 6
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((π
β2) Β·
((ββ(β―βπΌ))β2)) = ((π
β2) Β· (β―βπΌ))) |
61 | 22 | recnd 11246 |
. . . . . . 7
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (π
β2) β β) |
62 | 55 | rpcnd 13024 |
. . . . . . 7
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (β―βπΌ) β β) |
63 | 61, 62 | mulcomd 11239 |
. . . . . 6
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((π
β2) Β· (β―βπΌ)) = ((β―βπΌ) Β· (π
β2))) |
64 | 60, 63 | eqtrd 2766 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((π
β2) Β·
((ββ(β―βπΌ))β2)) = ((β―βπΌ) Β· (π
β2))) |
65 | 20 | rpcnd 13024 |
. . . . . 6
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β π
β β) |
66 | 55 | rpsqrtcld 15364 |
. . . . . . 7
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β
(ββ(β―βπΌ)) β
β+) |
67 | 66 | rpcnd 13024 |
. . . . . 6
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β
(ββ(β―βπΌ)) β β) |
68 | 65, 67 | sqmuld 14128 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((π
Β·
(ββ(β―βπΌ)))β2) = ((π
β2) Β·
((ββ(β―βπΌ))β2))) |
69 | | fsumconst 15742 |
. . . . . 6
β’ ((πΌ β Fin β§ (π
β2) β β) β
Ξ£π β πΌ (π
β2) = ((β―βπΌ) Β· (π
β2))) |
70 | 2, 61, 69 | syl2anc 583 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β Ξ£π β πΌ (π
β2) = ((β―βπΌ) Β· (π
β2))) |
71 | 64, 68, 70 | 3eqtr4d 2776 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((π
Β·
(ββ(β―βπΌ)))β2) = Ξ£π β πΌ (π
β2)) |
72 | 46, 51, 71 | 3brtr4d 5173 |
. . 3
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))β2) < ((π
Β·
(ββ(β―βπΌ)))β2)) |
73 | 47, 49 | resqrtcld 15370 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) β β) |
74 | 20, 66 | rpmulcld 13038 |
. . . . 5
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (π
Β·
(ββ(β―βπΌ))) β
β+) |
75 | 74 | rpred 13022 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (π
Β·
(ββ(β―βπΌ))) β β) |
76 | 47, 49 | sqrtge0d 15373 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β 0 β€ (ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))) |
77 | 74 | rpge0d 13026 |
. . . 4
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β 0 β€ (π
Β·
(ββ(β―βπΌ)))) |
78 | 73, 75, 76, 77 | lt2sqd 14224 |
. . 3
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β ((ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) < (π
Β·
(ββ(β―βπΌ))) β ((ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2))β2) < ((π
Β·
(ββ(β―βπΌ)))β2))) |
79 | 72, 78 | mpbird 257 |
. 2
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (ββΞ£π β πΌ (((πΉβπ) β (πΊβπ))β2)) < (π
Β·
(ββ(β―βπΌ)))) |
80 | 7, 79 | eqbrtrd 5163 |
1
β’ (((πΌ β (Fin β {β
})
β§ πΉ β π β§ πΊ β π) β§ (π
β β+ β§
βπ β πΌ ((πΉβπ)π(πΊβπ)) < π
)) β (πΉ(βnβπΌ)πΊ) < (π
Β·
(ββ(β―βπΌ)))) |