Step | Hyp | Ref
| Expression |
1 | | ftalem1.6 |
. . . 4
β’ π = (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) / πΈ) |
2 | | fzfid 13934 |
. . . . . 6
β’ (π β (0...(π β 1)) β Fin) |
3 | | ftalem.3 |
. . . . . . . . 9
β’ (π β πΉ β (Polyβπ)) |
4 | | ftalem.1 |
. . . . . . . . . 10
β’ π΄ = (coeffβπΉ) |
5 | 4 | coef3 25737 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β π΄:β0βΆβ) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
β’ (π β π΄:β0βΆβ) |
7 | | elfznn0 13590 |
. . . . . . . 8
β’ (π β (0...(π β 1)) β π β β0) |
8 | | ffvelcdm 7080 |
. . . . . . . 8
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
9 | 6, 7, 8 | syl2an 596 |
. . . . . . 7
β’ ((π β§ π β (0...(π β 1))) β (π΄βπ) β β) |
10 | 9 | abscld 15379 |
. . . . . 6
β’ ((π β§ π β (0...(π β 1))) β (absβ(π΄βπ)) β β) |
11 | 2, 10 | fsumrecl 15676 |
. . . . 5
β’ (π β Ξ£π β (0...(π β 1))(absβ(π΄βπ)) β β) |
12 | | ftalem1.5 |
. . . . 5
β’ (π β πΈ β
β+) |
13 | 11, 12 | rerpdivcld 13043 |
. . . 4
β’ (π β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) / πΈ) β β) |
14 | 1, 13 | eqeltrid 2837 |
. . 3
β’ (π β π β β) |
15 | | 1re 11210 |
. . 3
β’ 1 β
β |
16 | | ifcl 4572 |
. . 3
β’ ((π β β β§ 1 β
β) β if(1 β€ π, π, 1) β β) |
17 | 14, 15, 16 | sylancl 586 |
. 2
β’ (π β if(1 β€ π, π, 1) β β) |
18 | | fzfid 13934 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (0...(π β 1)) β Fin) |
19 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π΄:β0βΆβ) |
20 | 19, 8 | sylan 580 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β β0) β (π΄βπ) β β) |
21 | | simprl 769 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π₯ β β) |
22 | | expcl 14041 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π β β0)
β (π₯βπ) β
β) |
23 | 21, 22 | sylan 580 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β β0) β (π₯βπ) β β) |
24 | 20, 23 | mulcld 11230 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β β0) β ((π΄βπ) Β· (π₯βπ)) β β) |
25 | 7, 24 | sylan2 593 |
. . . . . . . 8
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β ((π΄βπ) Β· (π₯βπ)) β β) |
26 | 18, 25 | fsumcl 15675 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ)) β β) |
27 | | ftalem.4 |
. . . . . . . . . . 11
β’ (π β π β β) |
28 | 27 | nnnn0d 12528 |
. . . . . . . . . 10
β’ (π β π β
β0) |
29 | 28 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π β
β0) |
30 | 19, 29 | ffvelcdmd 7084 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (π΄βπ) β β) |
31 | 21, 29 | expcld 14107 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (π₯βπ) β β) |
32 | 30, 31 | mulcld 11230 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((π΄βπ) Β· (π₯βπ)) β β) |
33 | 3 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β πΉ β (Polyβπ)) |
34 | | ftalem.2 |
. . . . . . . . . 10
β’ π = (degβπΉ) |
35 | 4, 34 | coeid2 25744 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ π₯ β β) β (πΉβπ₯) = Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ))) |
36 | 33, 21, 35 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΉβπ₯) = Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ))) |
37 | | nn0uz 12860 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
38 | 29, 37 | eleqtrdi 2843 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π β
(β€β₯β0)) |
39 | | elfznn0 13590 |
. . . . . . . . . 10
β’ (π β (0...π) β π β β0) |
40 | 39, 24 | sylan2 593 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...π)) β ((π΄βπ) Β· (π₯βπ)) β β) |
41 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = π β (π΄βπ) = (π΄βπ)) |
42 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π = π β (π₯βπ) = (π₯βπ)) |
43 | 41, 42 | oveq12d 7423 |
. . . . . . . . 9
β’ (π = π β ((π΄βπ) Β· (π₯βπ)) = ((π΄βπ) Β· (π₯βπ))) |
44 | 38, 40, 43 | fsumm1 15693 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...π)((π΄βπ) Β· (π₯βπ)) = (Ξ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ)) + ((π΄βπ) Β· (π₯βπ)))) |
45 | 36, 44 | eqtrd 2772 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΉβπ₯) = (Ξ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ)) + ((π΄βπ) Β· (π₯βπ)))) |
46 | 26, 32, 45 | mvrraddd 11622 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ))) = Ξ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ))) |
47 | 46 | fveq2d 6892 |
. . . . 5
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) = (absβΞ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ)))) |
48 | 26 | abscld 15379 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβΞ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ))) β β) |
49 | 25 | abscld 15379 |
. . . . . . 7
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ((π΄βπ) Β· (π₯βπ))) β β) |
50 | 18, 49 | fsumrecl 15676 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ((π΄βπ) Β· (π₯βπ))) β β) |
51 | 12 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β πΈ β
β+) |
52 | 51 | rpred 13012 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β πΈ β β) |
53 | 21 | abscld 15379 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβπ₯) β β) |
54 | 53, 29 | reexpcld 14124 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((absβπ₯)βπ) β β) |
55 | 52, 54 | remulcld 11240 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΈ Β· ((absβπ₯)βπ)) β β) |
56 | 18, 25 | fsumabs 15743 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβΞ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ))) β€ Ξ£π β (0...(π β 1))(absβ((π΄βπ) Β· (π₯βπ)))) |
57 | 11 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ(π΄βπ)) β β) |
58 | 27 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π β β) |
59 | | nnm1nn0 12509 |
. . . . . . . . . 10
β’ (π β β β (π β 1) β
β0) |
60 | 58, 59 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (π β 1) β
β0) |
61 | 53, 60 | reexpcld 14124 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((absβπ₯)β(π β 1)) β
β) |
62 | 57, 61 | remulcld 11240 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) β
β) |
63 | 10 | adantlr 713 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ(π΄βπ)) β β) |
64 | 61 | adantr 481 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β ((absβπ₯)β(π β 1)) β
β) |
65 | 63, 64 | remulcld 11240 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β ((absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) β
β) |
66 | 20, 23 | absmuld 15397 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β β0) β
(absβ((π΄βπ) Β· (π₯βπ))) = ((absβ(π΄βπ)) Β· (absβ(π₯βπ)))) |
67 | 7, 66 | sylan2 593 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ((π΄βπ) Β· (π₯βπ))) = ((absβ(π΄βπ)) Β· (absβ(π₯βπ)))) |
68 | 7, 23 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (π₯βπ) β β) |
69 | 68 | abscld 15379 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ(π₯βπ)) β β) |
70 | 7, 20 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (π΄βπ) β β) |
71 | 70 | absge0d 15387 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β 0 β€
(absβ(π΄βπ))) |
72 | | absexp 15247 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π β β0)
β (absβ(π₯βπ)) = ((absβπ₯)βπ)) |
73 | 21, 7, 72 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ(π₯βπ)) = ((absβπ₯)βπ)) |
74 | 53 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβπ₯) β
β) |
75 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 1 β β) |
76 | 17 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β if(1 β€ π, π, 1) β β) |
77 | | max1 13160 |
. . . . . . . . . . . . . . . . . 18
β’ ((1
β β β§ π
β β) β 1 β€ if(1 β€ π, π, 1)) |
78 | 15, 14, 77 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 β€ if(1 β€ π, π, 1)) |
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 1 β€ if(1 β€ π, π, 1)) |
80 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β if(1 β€ π, π, 1) < (absβπ₯)) |
81 | 75, 76, 53, 79, 80 | lelttrd 11368 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 1 < (absβπ₯)) |
82 | 75, 53, 81 | ltled 11358 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 1 β€ (absβπ₯)) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β 1 β€ (absβπ₯)) |
84 | | elfzuz3 13494 |
. . . . . . . . . . . . . 14
β’ (π β (0...(π β 1)) β (π β 1) β
(β€β₯βπ)) |
85 | 84 | adantl 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (π β 1) β
(β€β₯βπ)) |
86 | 74, 83, 85 | leexp2ad 14213 |
. . . . . . . . . . . 12
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β ((absβπ₯)βπ) β€ ((absβπ₯)β(π β 1))) |
87 | 73, 86 | eqbrtrd 5169 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ(π₯βπ)) β€ ((absβπ₯)β(π β 1))) |
88 | 69, 64, 63, 71, 87 | lemul2ad 12150 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β ((absβ(π΄βπ)) Β· (absβ(π₯βπ))) β€ ((absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1)))) |
89 | 67, 88 | eqbrtrd 5169 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ((π΄βπ) Β· (π₯βπ))) β€ ((absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1)))) |
90 | 18, 49, 65, 89 | fsumle 15741 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ((π΄βπ) Β· (π₯βπ))) β€ Ξ£π β (0...(π β 1))((absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1)))) |
91 | 61 | recnd 11238 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((absβπ₯)β(π β 1)) β
β) |
92 | 63 | recnd 11238 |
. . . . . . . . 9
β’ (((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β§ π β (0...(π β 1))) β (absβ(π΄βπ)) β β) |
93 | 18, 91, 92 | fsummulc1 15727 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) = Ξ£π β (0...(π β 1))((absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1)))) |
94 | 90, 93 | breqtrrd 5175 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ((π΄βπ) Β· (π₯βπ))) β€ (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1)))) |
95 | 14 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π β β) |
96 | | max2 13162 |
. . . . . . . . . . . . . 14
β’ ((1
β β β§ π
β β) β π
β€ if(1 β€ π, π, 1)) |
97 | 15, 14, 96 | sylancr 587 |
. . . . . . . . . . . . 13
β’ (π β π β€ if(1 β€ π, π, 1)) |
98 | 97 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π β€ if(1 β€ π, π, 1)) |
99 | 95, 76, 53, 98, 80 | lelttrd 11368 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β π < (absβπ₯)) |
100 | 1, 99 | eqbrtrrid 5183 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) / πΈ) < (absβπ₯)) |
101 | 57, 53, 51 | ltdivmuld 13063 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((Ξ£π β (0...(π β 1))(absβ(π΄βπ)) / πΈ) < (absβπ₯) β Ξ£π β (0...(π β 1))(absβ(π΄βπ)) < (πΈ Β· (absβπ₯)))) |
102 | 100, 101 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ(π΄βπ)) < (πΈ Β· (absβπ₯))) |
103 | 52, 53 | remulcld 11240 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΈ Β· (absβπ₯)) β β) |
104 | 60 | nn0zd 12580 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (π β 1) β β€) |
105 | | 0red 11213 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 0 β β) |
106 | | 0lt1 11732 |
. . . . . . . . . . . . 13
β’ 0 <
1 |
107 | 106 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 0 < 1) |
108 | 105, 75, 53, 107, 81 | lttrd 11371 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 0 < (absβπ₯)) |
109 | | expgt0 14057 |
. . . . . . . . . . 11
β’
(((absβπ₯)
β β β§ (π
β 1) β β€ β§ 0 < (absβπ₯)) β 0 < ((absβπ₯)β(π β 1))) |
110 | 53, 104, 108, 109 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β 0 < ((absβπ₯)β(π β 1))) |
111 | | ltmul1 12060 |
. . . . . . . . . 10
β’
((Ξ£π β
(0...(π β
1))(absβ(π΄βπ)) β β β§ (πΈ Β· (absβπ₯)) β β β§ (((absβπ₯)β(π β 1)) β β β§ 0 <
((absβπ₯)β(π β 1)))) β
(Ξ£π β
(0...(π β
1))(absβ(π΄βπ)) < (πΈ Β· (absβπ₯)) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) < ((πΈ Β· (absβπ₯)) Β· ((absβπ₯)β(π β 1))))) |
112 | 57, 103, 61, 110, 111 | syl112anc 1374 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) < (πΈ Β· (absβπ₯)) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) < ((πΈ Β· (absβπ₯)) Β· ((absβπ₯)β(π β 1))))) |
113 | 102, 112 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) < ((πΈ Β· (absβπ₯)) Β· ((absβπ₯)β(π β 1)))) |
114 | 53 | recnd 11238 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβπ₯) β β) |
115 | | expm1t 14052 |
. . . . . . . . . . . 12
β’
(((absβπ₯)
β β β§ π
β β) β ((absβπ₯)βπ) = (((absβπ₯)β(π β 1)) Β· (absβπ₯))) |
116 | 114, 58, 115 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((absβπ₯)βπ) = (((absβπ₯)β(π β 1)) Β· (absβπ₯))) |
117 | 91, 114 | mulcomd 11231 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (((absβπ₯)β(π β 1)) Β· (absβπ₯)) = ((absβπ₯) Β· ((absβπ₯)β(π β 1)))) |
118 | 116, 117 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((absβπ₯)βπ) = ((absβπ₯) Β· ((absβπ₯)β(π β 1)))) |
119 | 118 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΈ Β· ((absβπ₯)βπ)) = (πΈ Β· ((absβπ₯) Β· ((absβπ₯)β(π β 1))))) |
120 | 52 | recnd 11238 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β πΈ β β) |
121 | 120, 114,
91 | mulassd 11233 |
. . . . . . . . 9
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β ((πΈ Β· (absβπ₯)) Β· ((absβπ₯)β(π β 1))) = (πΈ Β· ((absβπ₯) Β· ((absβπ₯)β(π β 1))))) |
122 | 119, 121 | eqtr4d 2775 |
. . . . . . . 8
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (πΈ Β· ((absβπ₯)βπ)) = ((πΈ Β· (absβπ₯)) Β· ((absβπ₯)β(π β 1)))) |
123 | 113, 122 | breqtrrd 5175 |
. . . . . . 7
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (Ξ£π β (0...(π β 1))(absβ(π΄βπ)) Β· ((absβπ₯)β(π β 1))) < (πΈ Β· ((absβπ₯)βπ))) |
124 | 50, 62, 55, 94, 123 | lelttrd 11368 |
. . . . . 6
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β Ξ£π β (0...(π β 1))(absβ((π΄βπ) Β· (π₯βπ))) < (πΈ Β· ((absβπ₯)βπ))) |
125 | 48, 50, 55, 56, 124 | lelttrd 11368 |
. . . . 5
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβΞ£π β (0...(π β 1))((π΄βπ) Β· (π₯βπ))) < (πΈ Β· ((absβπ₯)βπ))) |
126 | 47, 125 | eqbrtrd 5169 |
. . . 4
β’ ((π β§ (π₯ β β β§ if(1 β€ π, π, 1) < (absβπ₯))) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ))) |
127 | 126 | expr 457 |
. . 3
β’ ((π β§ π₯ β β) β (if(1 β€ π, π, 1) < (absβπ₯) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ)))) |
128 | 127 | ralrimiva 3146 |
. 2
β’ (π β βπ₯ β β (if(1 β€ π, π, 1) < (absβπ₯) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ)))) |
129 | | breq1 5150 |
. . 3
β’ (π = if(1 β€ π, π, 1) β (π < (absβπ₯) β if(1 β€ π, π, 1) < (absβπ₯))) |
130 | 129 | rspceaimv 3616 |
. 2
β’ ((if(1
β€ π, π, 1) β β β§ βπ₯ β β (if(1 β€ π, π, 1) < (absβπ₯) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ)))) β βπ β β βπ₯ β β (π < (absβπ₯) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ)))) |
131 | 17, 128, 130 | syl2anc 584 |
1
β’ (π β βπ β β βπ₯ β β (π < (absβπ₯) β (absβ((πΉβπ₯) β ((π΄βπ) Β· (π₯βπ)))) < (πΈ Β· ((absβπ₯)βπ)))) |