Step | Hyp | Ref
| Expression |
1 | | nnuz 12813 |
. . . 4
β’ β =
(β€β₯β1) |
2 | | 1zzd 12541 |
. . . . . 6
β’ (π β 1 β
β€) |
3 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ π β β) β π β β) |
4 | | rpvmasum.g |
. . . . . . . . . 10
β’ πΊ = (DChrβπ) |
5 | | rpvmasum.z |
. . . . . . . . . 10
β’ π =
(β€/nβ€βπ) |
6 | | rpvmasum.d |
. . . . . . . . . 10
β’ π· = (BaseβπΊ) |
7 | | rpvmasum.l |
. . . . . . . . . 10
β’ πΏ = (β€RHomβπ) |
8 | | dchrisum.b |
. . . . . . . . . . 11
β’ (π β π β π·) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β π·) |
10 | 3 | nnzd 12533 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β€) |
11 | 4, 5, 6, 7, 9, 10 | dchrzrhcl 26609 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβ(πΏβπ)) β β) |
12 | | dchrisum.4 |
. . . . . . . . . . . 12
β’ ((π β§ π β β+) β π΄ β
β) |
13 | 12 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ β β+ π΄ β β) |
14 | | nnrp 12933 |
. . . . . . . . . . 11
β’ (π β β β π β
β+) |
15 | | nfcsb1v 3885 |
. . . . . . . . . . . . . 14
β’
β²πβ¦π / πβ¦π΄ |
16 | 15 | nfel1 2924 |
. . . . . . . . . . . . 13
β’
β²πβ¦π / πβ¦π΄ β β |
17 | | csbeq1a 3874 |
. . . . . . . . . . . . . 14
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
19 | 16, 18 | rspc 3572 |
. . . . . . . . . . . 12
β’ (π β β+
β (βπ β
β+ π΄
β β β β¦π / πβ¦π΄ β β)) |
20 | 19 | impcom 409 |
. . . . . . . . . . 11
β’
((βπ β
β+ π΄
β β β§ π
β β+) β β¦π / πβ¦π΄ β β) |
21 | 13, 14, 20 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β β) |
22 | 21 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β β) β β¦π / πβ¦π΄ β β) |
23 | 11, 22 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) |
24 | | nfcv 2908 |
. . . . . . . . 9
β’
β²ππ |
25 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π(πβ(πΏβπ)) |
26 | | nfcv 2908 |
. . . . . . . . . 10
β’
β²π
Β· |
27 | 25, 26, 15 | nfov 7392 |
. . . . . . . . 9
β’
β²π((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) |
28 | | 2fveq3 6852 |
. . . . . . . . . 10
β’ (π = π β (πβ(πΏβπ)) = (πβ(πΏβπ))) |
29 | 28, 17 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = π β ((πβ(πΏβπ)) Β· π΄) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
30 | | dchrisum.7 |
. . . . . . . . 9
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) Β· π΄)) |
31 | 24, 27, 29, 30 | fvmptf 6974 |
. . . . . . . 8
β’ ((π β β β§ ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄) β β) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
32 | 3, 23, 31 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β) β (πΉβπ) = ((πβ(πΏβπ)) Β· β¦π / πβ¦π΄)) |
33 | 32, 23 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π β β) β (πΉβπ) β β) |
34 | 1, 2, 33 | serf 13943 |
. . . . 5
β’ (π β seq1( + , πΉ):ββΆβ) |
35 | 34 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π β β) β (seq1( + , πΉ)βπ) β β) |
36 | 12 | recnd 11190 |
. . . . . . . . 9
β’ ((π β§ π β β+) β π΄ β
β) |
37 | 36 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β β+ π΄ β β) |
38 | 37 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β
βπ β
β+ π΄
β β) |
39 | | id 22 |
. . . . . . . 8
β’ (π β β+
β π β
β+) |
40 | | 2re 12234 |
. . . . . . . . . 10
β’ 2 β
β |
41 | | dchrisum.9 |
. . . . . . . . . 10
β’ (π β π
β β) |
42 | | remulcl 11143 |
. . . . . . . . . 10
β’ ((2
β β β§ π
β β) β (2 Β· π
) β β) |
43 | 40, 41, 42 | sylancr 588 |
. . . . . . . . 9
β’ (π β (2 Β· π
) β
β) |
44 | | rpvmasum.a |
. . . . . . . . . . . 12
β’ (π β π β β) |
45 | | lbfzo0 13619 |
. . . . . . . . . . . 12
β’ (0 β
(0..^π) β π β
β) |
46 | 44, 45 | sylibr 233 |
. . . . . . . . . . 11
β’ (π β 0 β (0..^π)) |
47 | | dchrisum.10 |
. . . . . . . . . . 11
β’ (π β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π
) |
48 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = 0 β (0..^π’) = (0..^0)) |
49 | | fzo0 13603 |
. . . . . . . . . . . . . . . . 17
β’ (0..^0) =
β
|
50 | 48, 49 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
β’ (π’ = 0 β (0..^π’) = β
) |
51 | 50 | sumeq1d 15593 |
. . . . . . . . . . . . . . 15
β’ (π’ = 0 β Ξ£π β (0..^π’)(πβ(πΏβπ)) = Ξ£π β β
(πβ(πΏβπ))) |
52 | | sum0 15613 |
. . . . . . . . . . . . . . 15
β’
Ξ£π β
β
(πβ(πΏβπ)) = 0 |
53 | 51, 52 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
β’ (π’ = 0 β Ξ£π β (0..^π’)(πβ(πΏβπ)) = 0) |
54 | 53 | abs00bd 15183 |
. . . . . . . . . . . . 13
β’ (π’ = 0 β
(absβΞ£π β
(0..^π’)(πβ(πΏβπ))) = 0) |
55 | 54 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π’ = 0 β
((absβΞ£π β
(0..^π’)(πβ(πΏβπ))) β€ π
β 0 β€ π
)) |
56 | 55 | rspcv 3580 |
. . . . . . . . . . 11
β’ (0 β
(0..^π) β
(βπ’ β
(0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π
β 0 β€ π
)) |
57 | 46, 47, 56 | sylc 65 |
. . . . . . . . . 10
β’ (π β 0 β€ π
) |
58 | | 0le2 12262 |
. . . . . . . . . . 11
β’ 0 β€
2 |
59 | | mulge0 11680 |
. . . . . . . . . . 11
β’ (((2
β β β§ 0 β€ 2) β§ (π
β β β§ 0 β€ π
)) β 0 β€ (2 Β·
π
)) |
60 | 40, 58, 59 | mpanl12 701 |
. . . . . . . . . 10
β’ ((π
β β β§ 0 β€
π
) β 0 β€ (2
Β· π
)) |
61 | 41, 57, 60 | syl2anc 585 |
. . . . . . . . 9
β’ (π β 0 β€ (2 Β· π
)) |
62 | 43, 61 | ge0p1rpd 12994 |
. . . . . . . 8
β’ (π β ((2 Β· π
) + 1) β
β+) |
63 | | rpdivcl 12947 |
. . . . . . . 8
β’ ((π β β+
β§ ((2 Β· π
) + 1)
β β+) β (π / ((2 Β· π
) + 1)) β
β+) |
64 | 39, 62, 63 | syl2anr 598 |
. . . . . . 7
β’ ((π β§ π β β+) β (π / ((2 Β· π
) + 1)) β
β+) |
65 | | dchrisum.6 |
. . . . . . . 8
β’ (π β (π β β+ β¦ π΄) βπ
0) |
66 | 65 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β+) β (π β β+
β¦ π΄)
βπ 0) |
67 | 38, 64, 66 | rlimi 15402 |
. . . . . 6
β’ ((π β§ π β β+) β
βπ β β
βπ β
β+ (π β€
π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1)))) |
68 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
69 | | dchrisum.3 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
70 | 69 | nnred 12175 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
71 | 70 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β β) |
72 | 68, 71 | ifcld 4537 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β if(π β€ π, π, π) β β) |
73 | | 0red 11165 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 β
β) |
74 | 69 | nngt0d 12209 |
. . . . . . . . . . . . 13
β’ (π β 0 < π) |
75 | 74 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β 0 < π) |
76 | | max1 13111 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
77 | 70, 76 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π β€ if(π β€ π, π, π)) |
78 | 73, 71, 72, 75, 77 | ltletrd 11322 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β 0 < if(π β€ π, π, π)) |
79 | 72, 78 | elrpd 12961 |
. . . . . . . . . 10
β’ ((π β§ π β β) β if(π β€ π, π, π) β
β+) |
80 | 79 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β β) β if(π β€ π, π, π) β
β+) |
81 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β€ if(π β€ π, π, π) |
82 | | nfcv 2908 |
. . . . . . . . . . . . 13
β’
β²πabs |
83 | | nfcsb1v 3885 |
. . . . . . . . . . . . . 14
β’
β²πβ¦if(π β€ π, π, π) / πβ¦π΄ |
84 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π
β |
85 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π0 |
86 | 83, 84, 85 | nfov 7392 |
. . . . . . . . . . . . 13
β’
β²π(β¦if(π β€ π, π, π) / πβ¦π΄ β 0) |
87 | 82, 86 | nffv 6857 |
. . . . . . . . . . . 12
β’
β²π(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) |
88 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π
< |
89 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π(π / ((2 Β· π
) + 1)) |
90 | 87, 88, 89 | nfbr 5157 |
. . . . . . . . . . 11
β’
β²π(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)) |
91 | 81, 90 | nfim 1900 |
. . . . . . . . . 10
β’
β²π(π β€ if(π β€ π, π, π) β (absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1))) |
92 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = if(π β€ π, π, π) β (π β€ π β π β€ if(π β€ π, π, π))) |
93 | | csbeq1a 3874 |
. . . . . . . . . . . . 13
β’ (π = if(π β€ π, π, π) β π΄ = β¦if(π β€ π, π, π) / πβ¦π΄) |
94 | 93 | fvoveq1d 7384 |
. . . . . . . . . . . 12
β’ (π = if(π β€ π, π, π) β (absβ(π΄ β 0)) =
(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0))) |
95 | 94 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π = if(π β€ π, π, π) β ((absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1)) β
(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)))) |
96 | 92, 95 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = if(π β€ π, π, π) β ((π β€ π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1))) β (π β€ if(π β€ π, π, π) β (absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1))))) |
97 | 91, 96 | rspc 3572 |
. . . . . . . . 9
β’ (if(π β€ π, π, π) β β+ β
(βπ β
β+ (π β€
π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1))) β (π β€ if(π β€ π, π, π) β (absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1))))) |
98 | 80, 97 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β β) β
(βπ β
β+ (π β€
π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1))) β (π β€ if(π β€ π, π, π) β (absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1))))) |
99 | 70 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β β) β π β
β) |
100 | | max2 13113 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
101 | 99, 100 | sylancom 589 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β β) β π β€ if(π β€ π, π, π)) |
102 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β
βπ β
β+ π΄
β β) |
103 | 83 | nfel1 2924 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβ¦if(π β€ π, π, π) / πβ¦π΄ β β |
104 | 93 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = if(π β€ π, π, π) β (π΄ β β β
β¦if(π β€
π, π, π) / πβ¦π΄ β β)) |
105 | 103, 104 | rspc 3572 |
. . . . . . . . . . . . . . . . . 18
β’ (if(π β€ π, π, π) β β+ β
(βπ β
β+ π΄
β β β β¦if(π β€ π, π, π) / πβ¦π΄ β β)) |
106 | 80, 102, 105 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β β) β
β¦if(π β€
π, π, π) / πβ¦π΄ β β) |
107 | 106 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β β) β
β¦if(π β€
π, π, π) / πβ¦π΄ β β) |
108 | 107 | subid1d 11508 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π β β) β
(β¦if(π β€
π, π, π) / πβ¦π΄ β 0) = β¦if(π β€ π, π, π) / πβ¦π΄) |
109 | 108 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β β) β
(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) =
(absββ¦if(π β€ π, π, π) / πβ¦π΄)) |
110 | 72 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β β) β if(π β€ π, π, π) β β) |
111 | 99, 76 | sylancom 589 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β β) β π β€ if(π β€ π, π, π)) |
112 | | elicopnf 13369 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (if(π β€ π, π, π) β (π[,)+β) β (if(π β€ π, π, π) β β β§ π β€ if(π β€ π, π, π)))) |
113 | 99, 112 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β β) β
(if(π β€ π, π, π) β (π[,)+β) β (if(π β€ π, π, π) β β β§ π β€ if(π β€ π, π, π)))) |
114 | 110, 111,
113 | mpbir2and 712 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β β) β if(π β€ π, π, π) β (π[,)+β)) |
115 | 44 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β π β
β) |
116 | | rpvmasum.1 |
. . . . . . . . . . . . . . . . . 18
β’ 1 =
(0gβπΊ) |
117 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β π β π·) |
118 | | dchrisum.n1 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β 1 ) |
119 | 118 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β π β 1 ) |
120 | | dchrisum.2 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π₯ β π΄ = π΅) |
121 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β π β
β) |
122 | 12 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β+) β§ π β β) β§ π β β+)
β π΄ β
β) |
123 | | simpll 766 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β+) β§ π β β) β π) |
124 | | dchrisum.5 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
125 | 123, 124 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β+) β§ π β β) β§ (π β β+
β§ π₯ β
β+) β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
126 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β+) β§ π β β) β (π β β+
β¦ π΄)
βπ 0) |
127 | 5, 7, 115, 4, 6, 116, 117, 119, 120, 121, 122, 125, 126, 30 | dchrisumlema 26852 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β+) β§ π β β) β
((if(π β€ π, π, π) β β+ β
β¦if(π β€
π, π, π) / πβ¦π΄ β β) β§ (if(π β€ π, π, π) β (π[,)+β) β 0 β€
β¦if(π β€
π, π, π) / πβ¦π΄))) |
128 | 127 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β+) β§ π β β) β
(if(π β€ π, π, π) β (π[,)+β) β 0 β€
β¦if(π β€
π, π, π) / πβ¦π΄)) |
129 | 114, 128 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β+) β§ π β β) β 0 β€
β¦if(π β€
π, π, π) / πβ¦π΄) |
130 | 106, 129 | absidd 15314 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ π β β) β
(absββ¦if(π β€ π, π, π) / πβ¦π΄) = β¦if(π β€ π, π, π) / πβ¦π΄) |
131 | 109, 130 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β
(absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) = β¦if(π β€ π, π, π) / πβ¦π΄) |
132 | 131 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β β) β
((absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)) β β¦if(π β€ π, π, π) / πβ¦π΄ < (π / ((2 Β· π
) + 1)))) |
133 | | rpre 12930 |
. . . . . . . . . . . . . 14
β’ (π β β+
β π β
β) |
134 | 133 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β π β
β) |
135 | 62 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β ((2
Β· π
) + 1) β
β+) |
136 | 106, 134,
135 | ltmuldiv2d 13012 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β β) β ((((2
Β· π
) + 1) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π β β¦if(π β€ π, π, π) / πβ¦π΄ < (π / ((2 Β· π
) + 1)))) |
137 | 132, 136 | bitr4d 282 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β
((absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)) β (((2 Β· π
) + 1) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π)) |
138 | 43 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β (2
Β· π
) β
β) |
139 | 135 | rpred 12964 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β ((2
Β· π
) + 1) β
β) |
140 | 138 | lep1d 12093 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β (2
Β· π
) β€ ((2
Β· π
) +
1)) |
141 | 138, 139,
106, 129, 140 | lemul1ad 12101 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β β) β ((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β€ (((2 Β· π
) + 1) Β· β¦if(π β€ π, π, π) / πβ¦π΄)) |
142 | 138, 106 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β ((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β β) |
143 | 139, 106 | remulcld 11192 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ π β β) β (((2
Β· π
) + 1) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β β) |
144 | | lelttr 11252 |
. . . . . . . . . . . . 13
β’ ((((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β β β§ (((2 Β· π
) + 1) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β β β§ π β β) β ((((2 Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β€ (((2 Β· π
) + 1) Β· β¦if(π β€ π, π, π) / πβ¦π΄) β§ (((2 Β· π
) + 1) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π) β ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π)) |
145 | 142, 143,
134, 144 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ π β β) β ((((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β€ (((2 Β· π
) + 1) Β· β¦if(π β€ π, π, π) / πβ¦π΄) β§ (((2 Β· π
) + 1) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π) β ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π)) |
146 | 141, 145 | mpand 694 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β ((((2
Β· π
) + 1) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π β ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π)) |
147 | 137, 146 | sylbid 239 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β β) β
((absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)) β ((2 Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π)) |
148 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β 1 β
β) |
149 | 69 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π β β) |
150 | 149 | nnge1d 12208 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β 1 β€ π) |
151 | 148, 71, 72, 150, 77 | letrd 11319 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β 1 β€ if(π β€ π, π, π)) |
152 | | flge1nn 13733 |
. . . . . . . . . . . . 13
β’
((if(π β€ π, π, π) β β β§ 1 β€ if(π β€ π, π, π)) β (ββif(π β€ π, π, π)) β β) |
153 | 72, 151, 152 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β
(ββif(π β€
π, π, π)) β β) |
154 | 153 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β
(ββif(π β€
π, π, π)) β β) |
155 | 44 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β β) |
156 | 8 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β π·) |
157 | 118 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β 1 ) |
158 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β β) |
159 | 12 | ad4ant14 751 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β§ π β β+) β π΄ β
β) |
160 | 124 | 3adant1r 1178 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
161 | 160 | 3adant1r 1178 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
162 | 65 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (π β β+ β¦ π΄) βπ
0) |
163 | 41 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π
β β) |
164 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π
) |
165 | 79 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β if(π β€ π, π, π) β
β+) |
166 | 77 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β€ if(π β€ π, π, π)) |
167 | 72 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β if(π β€ π, π, π) β β) |
168 | | fllep1 13713 |
. . . . . . . . . . . . . . . 16
β’ (if(π β€ π, π, π) β β β if(π β€ π, π, π) β€ ((ββif(π β€ π, π, π)) + 1)) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β if(π β€ π, π, π) β€ ((ββif(π β€ π, π, π)) + 1)) |
170 | 153 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (ββif(π β€ π, π, π)) β β) |
171 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β
(β€β₯β(ββif(π β€ π, π, π)))) |
172 | 5, 7, 155, 4, 6, 116, 156, 157, 120, 158, 159, 161, 162, 30, 163, 164, 165, 166, 169, 170, 171 | dchrisumlem2 26854 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β€ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄)) |
173 | 172 | adantllr 718 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β€ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄)) |
174 | 34 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β seq1( + , πΉ):ββΆβ) |
175 | | eluznn 12850 |
. . . . . . . . . . . . . . . . . 18
β’
(((ββif(π β€ π, π, π)) β β β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β β) |
176 | 154, 175 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β β) |
177 | 174, 176 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (seq1( + , πΉ)βπ) β β) |
178 | 154 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (ββif(π β€ π, π, π)) β β) |
179 | 174, 178 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))) β β) |
180 | 177, 179 | subcld 11519 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π)))) β β) |
181 | 180 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β β) |
182 | 142 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) β β) |
183 | 134 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β π β β) |
184 | | lelttr 11252 |
. . . . . . . . . . . . . 14
β’
(((absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β β β§ ((2 Β·
π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) β β β§ π β β) β (((absβ((seq1(
+ , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β€ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) β§ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
185 | 181, 182,
183, 184 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (((absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) β€ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) β§ ((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
186 | 173, 185 | mpand 694 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ π β β) β§ π β
(β€β₯β(ββif(π β€ π, π, π)))) β (((2 Β· π
) Β· β¦if(π β€ π, π, π) / πβ¦π΄) < π β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
187 | 186 | ralrimdva 3152 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β (((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π β βπ β
(β€β₯β(ββif(π β€ π, π, π)))(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
188 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = (ββif(π β€ π, π, π)) β
(β€β₯βπ) =
(β€β₯β(ββif(π β€ π, π, π)))) |
189 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = (ββif(π β€ π, π, π)) β (seq1( + , πΉ)βπ) = (seq1( + , πΉ)β(ββif(π β€ π, π, π)))) |
190 | 189 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = (ββif(π β€ π, π, π)) β ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ)) = ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) |
191 | 190 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = (ββif(π β€ π, π, π)) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) = (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π)))))) |
192 | 191 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = (ββif(π β€ π, π, π)) β ((absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
193 | 188, 192 | raleqbidv 3322 |
. . . . . . . . . . . 12
β’ (π = (ββif(π β€ π, π, π)) β (βπ β (β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π β βπ β
(β€β₯β(ββif(π β€ π, π, π)))(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π)) |
194 | 193 | rspcev 3584 |
. . . . . . . . . . 11
β’
(((ββif(π β€ π, π, π)) β β β§ βπ β
(β€β₯β(ββif(π β€ π, π, π)))(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββif(π β€ π, π, π))))) < π) β βπ β β βπ β (β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π) |
195 | 154, 187,
194 | syl6an 683 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β β) β (((2
Β· π
) Β·
β¦if(π β€
π, π, π) / πβ¦π΄) < π β βπ β β βπ β (β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π)) |
196 | 147, 195 | syld 47 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β β) β
((absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1)) β βπ β β βπ β (β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π)) |
197 | 101, 196 | embantd 59 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β β) β ((π β€ if(π β€ π, π, π) β (absβ(β¦if(π β€ π, π, π) / πβ¦π΄ β 0)) < (π / ((2 Β· π
) + 1))) β βπ β β βπ β (β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π)) |
198 | 98, 197 | syld 47 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π β β) β
(βπ β
β+ (π β€
π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1))) β βπ β β βπ β
(β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π)) |
199 | 198 | rexlimdva 3153 |
. . . . . 6
β’ ((π β§ π β β+) β
(βπ β β
βπ β
β+ (π β€
π β (absβ(π΄ β 0)) < (π / ((2 Β· π
) + 1))) β βπ β β βπ β
(β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π)) |
200 | 67, 199 | mpd 15 |
. . . . 5
β’ ((π β§ π β β+) β
βπ β β
βπ β
(β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π) |
201 | 200 | ralrimiva 3144 |
. . . 4
β’ (π β βπ β β+ βπ β β βπ β
(β€β₯βπ)(absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)βπ))) < π) |
202 | | seqex 13915 |
. . . . 5
β’ seq1( + ,
πΉ) β
V |
203 | 202 | a1i 11 |
. . . 4
β’ (π β seq1( + , πΉ) β V) |
204 | 1, 35, 201, 203 | caucvg 15570 |
. . 3
β’ (π β seq1( + , πΉ) β dom β
) |
205 | 202 | eldm 5861 |
. . 3
β’ (seq1( +
, πΉ) β dom β
β βπ‘seq1( + ,
πΉ) β π‘) |
206 | 204, 205 | sylib 217 |
. 2
β’ (π β βπ‘seq1( + , πΉ) β π‘) |
207 | | simpr 486 |
. . . . 5
β’ ((π β§ seq1( + , πΉ) β π‘) β seq1( + , πΉ) β π‘) |
208 | | elrege0 13378 |
. . . . . . . 8
β’ ((2
Β· π
) β
(0[,)+β) β ((2 Β· π
) β β β§ 0 β€ (2 Β·
π
))) |
209 | 43, 61, 208 | sylanbrc 584 |
. . . . . . 7
β’ (π β (2 Β· π
) β
(0[,)+β)) |
210 | 209 | adantr 482 |
. . . . . 6
β’ ((π β§ seq1( + , πΉ) β π‘) β (2 Β· π
) β (0[,)+β)) |
211 | | eqid 2737 |
. . . . . . . 8
β’
(β€β₯β(ββπ)) =
(β€β₯β(ββπ)) |
212 | | pnfxr 11216 |
. . . . . . . . . . . 12
β’ +β
β β* |
213 | | icossre 13352 |
. . . . . . . . . . . 12
β’ ((π β β β§ +β
β β*) β (π[,)+β) β
β) |
214 | 70, 212, 213 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (π[,)+β) β
β) |
215 | 214 | sselda 3949 |
. . . . . . . . . 10
β’ ((π β§ π β (π[,)+β)) β π β β) |
216 | 215 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β π β β) |
217 | 216 | flcld 13710 |
. . . . . . . 8
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (ββπ) β
β€) |
218 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β seq1( + , πΉ) β π‘) |
219 | 34 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β seq1( + , πΉ):ββΆβ) |
220 | | 1red 11163 |
. . . . . . . . . . . . 13
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β 1 β
β) |
221 | 70 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β π β β) |
222 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β π β β) |
223 | 222 | nnge1d 12208 |
. . . . . . . . . . . . 13
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β 1 β€ π) |
224 | | elicopnf 13369 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β (π[,)+β) β (π β β β§ π β€ π))) |
225 | 70, 224 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β (π β (π[,)+β) β (π β β β§ π β€ π))) |
226 | 225 | simplbda 501 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π[,)+β)) β π β€ π) |
227 | 226 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β π β€ π) |
228 | 220, 221,
216, 223, 227 | letrd 11319 |
. . . . . . . . . . . 12
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β 1 β€ π) |
229 | | flge1nn 13733 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β€
π) β
(ββπ) β
β) |
230 | 216, 228,
229 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (ββπ) β
β) |
231 | 219, 230 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (seq1( + , πΉ)β(ββπ)) β
β) |
232 | | nnex 12166 |
. . . . . . . . . . . 12
β’ β
β V |
233 | 232 | mptex 7178 |
. . . . . . . . . . 11
β’ (π β β β¦ ((seq1(
+ , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) β V |
234 | 233 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) β V) |
235 | 219 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β seq1( + , πΉ):ββΆβ) |
236 | | eluznn 12850 |
. . . . . . . . . . . 12
β’
(((ββπ)
β β β§ π
β (β€β₯β(ββπ))) β π β β) |
237 | 230, 236 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β β) |
238 | 235, 237 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (seq1( + , πΉ)βπ) β β) |
239 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (seq1( + , πΉ)βπ) = (seq1( + , πΉ)βπ)) |
240 | 239 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π = π β ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)) = ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) |
241 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦ ((seq1(
+ , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) = (π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) |
242 | | ovex 7395 |
. . . . . . . . . . . 12
β’ ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)) β V |
243 | 240, 241,
242 | fvmpt3i 6958 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((seq1(
+ , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ) = ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) |
244 | 237, 243 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ) = ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) |
245 | 211, 217,
218, 231, 234, 238, 244 | climsubc2 15528 |
. . . . . . . . 9
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) β ((seq1( + , πΉ)β(ββπ)) β π‘)) |
246 | 232 | mptex 7178 |
. . . . . . . . . 10
β’ (π β β β¦
(absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) β V |
247 | 246 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) β V) |
248 | | fvex 6860 |
. . . . . . . . . . . . . 14
β’ (seq1( +
, πΉ)β(ββπ)) β V |
249 | 248 | fvconst2 7158 |
. . . . . . . . . . . . 13
β’ (π β β β ((β
Γ {(seq1( + , πΉ)β(ββπ))})βπ) = (seq1( + , πΉ)β(ββπ))) |
250 | 237, 249 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((β Γ {(seq1( + ,
πΉ)β(ββπ))})βπ) = (seq1( + , πΉ)β(ββπ))) |
251 | 250 | oveq1d 7377 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (((β Γ {(seq1( + ,
πΉ)β(ββπ))})βπ) β (seq1( + , πΉ)βπ)) = ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) |
252 | 244, 251 | eqtr4d 2780 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ) = (((β Γ {(seq1( + , πΉ)β(ββπ))})βπ) β (seq1( + , πΉ)βπ))) |
253 | 231 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (seq1( + , πΉ)β(ββπ)) β β) |
254 | 250, 253 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((β Γ {(seq1( + ,
πΉ)β(ββπ))})βπ) β β) |
255 | 254, 238 | subcld 11519 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (((β Γ {(seq1( + ,
πΉ)β(ββπ))})βπ) β (seq1( + , πΉ)βπ)) β β) |
256 | 252, 255 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ) β β) |
257 | 240 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) = (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) |
258 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β β β¦
(absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) = (π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) |
259 | | fvex 6860 |
. . . . . . . . . . . 12
β’
(absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) β V |
260 | 257, 258,
259 | fvmpt3i 6958 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦
(absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) = (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) |
261 | 237, 260 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) = (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) |
262 | 244 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (absβ((π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ)) = (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) |
263 | 261, 262 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) = (absβ((π β β β¦ ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))βπ))) |
264 | 211, 245,
247, 217, 256, 263 | climabs 15493 |
. . . . . . . 8
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)))) β (absβ((seq1( + , πΉ)β(ββπ)) β π‘))) |
265 | 43 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (2 Β· π
) β
β) |
266 | | 0red 11165 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π[,)+β)) β 0 β
β) |
267 | 70 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π[,)+β)) β π β β) |
268 | 74 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π[,)+β)) β 0 < π) |
269 | 266, 267,
215, 268, 226 | ltletrd 11322 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π[,)+β)) β 0 < π) |
270 | 215, 269 | elrpd 12961 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π[,)+β)) β π β β+) |
271 | | nfcsb1v 3885 |
. . . . . . . . . . . . . . . 16
β’
β²πβ¦π / πβ¦π΄ |
272 | 271 | nfel1 2924 |
. . . . . . . . . . . . . . 15
β’
β²πβ¦π / πβ¦π΄ β β |
273 | | csbeq1a 3874 |
. . . . . . . . . . . . . . . 16
β’ (π = π β π΄ = β¦π / πβ¦π΄) |
274 | 273 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π΄ β β β β¦π / πβ¦π΄ β β)) |
275 | 272, 274 | rspc 3572 |
. . . . . . . . . . . . . 14
β’ (π β β+
β (βπ β
β+ π΄
β β β β¦π / πβ¦π΄ β β)) |
276 | 13, 275 | mpan9 508 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β+) β
β¦π / πβ¦π΄ β β) |
277 | 270, 276 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π[,)+β)) β β¦π / πβ¦π΄ β β) |
278 | 277 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β β¦π / πβ¦π΄ β β) |
279 | 265, 278 | remulcld 11192 |
. . . . . . . . . 10
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β ((2 Β· π
) Β· β¦π / πβ¦π΄) β β) |
280 | 279 | recnd 11190 |
. . . . . . . . 9
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β ((2 Β· π
) Β· β¦π / πβ¦π΄) β β) |
281 | | 1z 12540 |
. . . . . . . . 9
β’ 1 β
β€ |
282 | 1 | eqimss2i 4008 |
. . . . . . . . . 10
β’
(β€β₯β1) β β |
283 | 282, 232 | climconst2 15437 |
. . . . . . . . 9
β’ ((((2
Β· π
) Β·
β¦π / πβ¦π΄) β β β§ 1 β β€)
β (β Γ {((2 Β· π
) Β· β¦π / πβ¦π΄)}) β ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
284 | 280, 281,
283 | sylancl 587 |
. . . . . . . 8
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (β Γ {((2
Β· π
) Β·
β¦π / πβ¦π΄)}) β ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
285 | 253, 238 | subcld 11519 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ)) β β) |
286 | 285 | abscld 15328 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) β β) |
287 | 261, 286 | eqeltrd 2838 |
. . . . . . . 8
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) β β) |
288 | | ovex 7395 |
. . . . . . . . . . 11
β’ ((2
Β· π
) Β·
β¦π / πβ¦π΄) β V |
289 | 288 | fvconst2 7158 |
. . . . . . . . . 10
β’ (π β β β ((β
Γ {((2 Β· π
)
Β· β¦π /
πβ¦π΄)})βπ) = ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
290 | 237, 289 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((β Γ {((2 Β·
π
) Β·
β¦π / πβ¦π΄)})βπ) = ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
291 | 279 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((2 Β· π
) Β· β¦π / πβ¦π΄) β β) |
292 | 290, 291 | eqeltrd 2838 |
. . . . . . . 8
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((β Γ {((2 Β·
π
) Β·
β¦π / πβ¦π΄)})βπ) β β) |
293 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π) |
294 | 293, 44 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β β) |
295 | 293, 8 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β π·) |
296 | 293, 118 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β 1 ) |
297 | 222 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β β) |
298 | 293, 12 | sylan 581 |
. . . . . . . . . 10
β’
(((((π β§ seq1( + ,
πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β§ π β β+) β π΄ β
β) |
299 | 293, 124 | syl3an1 1164 |
. . . . . . . . . 10
β’
(((((π β§ seq1( + ,
πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β§ (π β β+ β§ π₯ β β+)
β§ (π β€ π β§ π β€ π₯)) β π΅ β€ π΄) |
300 | 293, 65 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (π β β+ β¦ π΄) βπ
0) |
301 | 293, 41 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π
β β) |
302 | 293, 47 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β βπ’ β (0..^π)(absβΞ£π β (0..^π’)(πβ(πΏβπ))) β€ π
) |
303 | 270 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β π β β+) |
304 | 303 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β β+) |
305 | 227 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β€ π) |
306 | 216 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β β) |
307 | | reflcl 13708 |
. . . . . . . . . . . 12
β’ (π β β β
(ββπ) β
β) |
308 | | peano2re 11335 |
. . . . . . . . . . . 12
β’
((ββπ)
β β β ((ββπ) + 1) β β) |
309 | 306, 307,
308 | 3syl 18 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((ββπ) + 1) β β) |
310 | | flltp1 13712 |
. . . . . . . . . . . 12
β’ (π β β β π < ((ββπ) + 1)) |
311 | 306, 310 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π < ((ββπ) + 1)) |
312 | 306, 309,
311 | ltled 11310 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β€ ((ββπ) + 1)) |
313 | 230 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (ββπ) β β) |
314 | | simpr 486 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β π β
(β€β₯β(ββπ))) |
315 | 5, 7, 294, 4, 6, 116, 295, 296, 120, 297, 298, 299, 300, 30, 301, 302, 304, 305, 312, 313, 314 | dchrisumlem2 26854 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββπ)))) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
316 | 253, 238 | abssubd 15345 |
. . . . . . . . . 10
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β (absβ((seq1( + , πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))) = (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββπ))))) |
317 | 261, 316 | eqtrd 2777 |
. . . . . . . . 9
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) = (absβ((seq1( + , πΉ)βπ) β (seq1( + , πΉ)β(ββπ))))) |
318 | 315, 317,
290 | 3brtr4d 5142 |
. . . . . . . 8
β’ ((((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β§ π β
(β€β₯β(ββπ))) β ((π β β β¦ (absβ((seq1( +
, πΉ)β(ββπ)) β (seq1( + , πΉ)βπ))))βπ) β€ ((β Γ {((2 Β· π
) Β· β¦π / πβ¦π΄)})βπ)) |
319 | 211, 217,
264, 284, 287, 292, 318 | climle 15529 |
. . . . . . 7
β’ (((π β§ seq1( + , πΉ) β π‘) β§ π β (π[,)+β)) β (absβ((seq1( + ,
πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
320 | 319 | ralrimiva 3144 |
. . . . . 6
β’ ((π β§ seq1( + , πΉ) β π‘) β βπ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) |
321 | | oveq1 7369 |
. . . . . . . . . 10
β’ (π = (2 Β· π
) β (π Β· π΅) = ((2 Β· π
) Β· π΅)) |
322 | 321 | breq2d 5122 |
. . . . . . . . 9
β’ (π = (2 Β· π
) β ((absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅) β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ ((2 Β· π
) Β· π΅))) |
323 | 322 | ralbidv 3175 |
. . . . . . . 8
β’ (π = (2 Β· π
) β (βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅) β βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ ((2 Β· π
) Β· π΅))) |
324 | | 2fveq3 6852 |
. . . . . . . . . . 11
β’ (π = π₯ β (seq1( + , πΉ)β(ββπ)) = (seq1( + , πΉ)β(ββπ₯))) |
325 | 324 | fvoveq1d 7384 |
. . . . . . . . . 10
β’ (π = π₯ β (absβ((seq1( + , πΉ)β(ββπ)) β π‘)) = (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘))) |
326 | | vex 3452 |
. . . . . . . . . . . . 13
β’ π β V |
327 | 326 | a1i 11 |
. . . . . . . . . . . 12
β’ (π = π₯ β π β V) |
328 | | equequ2 2030 |
. . . . . . . . . . . . . 14
β’ (π = π₯ β (π = π β π = π₯)) |
329 | 328 | biimpa 478 |
. . . . . . . . . . . . 13
β’ ((π = π₯ β§ π = π) β π = π₯) |
330 | 329, 120 | syl 17 |
. . . . . . . . . . . 12
β’ ((π = π₯ β§ π = π) β π΄ = π΅) |
331 | 327, 330 | csbied 3898 |
. . . . . . . . . . 11
β’ (π = π₯ β β¦π / πβ¦π΄ = π΅) |
332 | 331 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π₯ β ((2 Β· π
) Β· β¦π / πβ¦π΄) = ((2 Β· π
) Β· π΅)) |
333 | 325, 332 | breq12d 5123 |
. . . . . . . . 9
β’ (π = π₯ β ((absβ((seq1( + , πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄) β (absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ ((2 Β· π
) Β· π΅))) |
334 | 333 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ β
(π[,)+β)(absβ((seq1( + , πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄) β βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ ((2 Β· π
) Β· π΅)) |
335 | 323, 334 | bitr4di 289 |
. . . . . . 7
β’ (π = (2 Β· π
) β (βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅) β βπ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄))) |
336 | 335 | rspcev 3584 |
. . . . . 6
β’ (((2
Β· π
) β
(0[,)+β) β§ βπ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ)) β π‘)) β€ ((2 Β· π
) Β· β¦π / πβ¦π΄)) β βπ β (0[,)+β)βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅)) |
337 | 210, 320,
336 | syl2anc 585 |
. . . . 5
β’ ((π β§ seq1( + , πΉ) β π‘) β βπ β (0[,)+β)βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅)) |
338 | | r19.42v 3188 |
. . . . 5
β’
(βπ β
(0[,)+β)(seq1( + , πΉ)
β π‘ β§
βπ₯ β (π[,)+β)(absβ((seq1( +
, πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅)) β (seq1( + , πΉ) β π‘ β§ βπ β (0[,)+β)βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅))) |
339 | 207, 337,
338 | sylanbrc 584 |
. . . 4
β’ ((π β§ seq1( + , πΉ) β π‘) β βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅))) |
340 | 339 | ex 414 |
. . 3
β’ (π β (seq1( + , πΉ) β π‘ β βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅)))) |
341 | 340 | eximdv 1921 |
. 2
β’ (π β (βπ‘seq1( + , πΉ) β π‘ β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅)))) |
342 | 206, 341 | mpd 15 |
1
β’ (π β βπ‘βπ β (0[,)+β)(seq1( + , πΉ) β π‘ β§ βπ₯ β (π[,)+β)(absβ((seq1( + , πΉ)β(ββπ₯)) β π‘)) β€ (π Β· π΅))) |