Step | Hyp | Ref
| Expression |
1 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
2 | | 1zzd 12541 |
. . . . . 6
β’ (π β 1 β
β€) |
3 | | fzfid 13885 |
. . . . . 6
β’ (π β (0...π) β Fin) |
4 | | 1zzd 12541 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π < π) β 1 β β€) |
5 | | plyeq0.3 |
. . . . . . . . . . . . . . . . 17
β’ (π β π΄ β ((π βͺ {0}) βm
β0)) |
6 | | plyeq0.1 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
7 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β |
8 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 0 β
β) |
9 | 8 | snssd 4774 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β {0} β
β) |
10 | 6, 9 | unssd 4151 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π βͺ {0}) β
β) |
11 | | cnex 11139 |
. . . . . . . . . . . . . . . . . . 19
β’ β
β V |
12 | | ssexg 5285 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π βͺ {0}) β β
β§ β β V) β (π βͺ {0}) β V) |
13 | 10, 11, 12 | sylancl 587 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π βͺ {0}) β V) |
14 | | nn0ex 12426 |
. . . . . . . . . . . . . . . . . 18
β’
β0 β V |
15 | | elmapg 8785 |
. . . . . . . . . . . . . . . . . 18
β’ (((π βͺ {0}) β V β§
β0 β V) β (π΄ β ((π βͺ {0}) βm
β0) β π΄:β0βΆ(π βͺ {0}))) |
16 | 13, 14, 15 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΄ β ((π βͺ {0}) βm
β0) β π΄:β0βΆ(π βͺ {0}))) |
17 | 5, 16 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄:β0βΆ(π βͺ {0})) |
18 | 17, 10 | fssd 6691 |
. . . . . . . . . . . . . . 15
β’ (π β π΄:β0βΆβ) |
19 | | elfznn0 13541 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β π β β0) |
20 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . 15
β’ ((π΄:β0βΆβ β§
π β
β0) β (π΄βπ) β β) |
21 | 18, 19, 20 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (π΄βπ) β β) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π < π) β (π΄βπ) β β) |
23 | 22 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ π < π) β (absβ(π΄βπ)) β β) |
24 | 23 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π < π) β (absβ(π΄βπ)) β β) |
25 | | divcnv 15745 |
. . . . . . . . . . 11
β’
((absβ(π΄βπ)) β β β (π β β β¦ ((absβ(π΄βπ)) / π)) β 0) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((absβ(π΄βπ)) / π)) β 0) |
27 | | nnex 12166 |
. . . . . . . . . . . 12
β’ β
β V |
28 | 27 | mptex 7178 |
. . . . . . . . . . 11
β’ (π β β β¦
((absβ(π΄βπ)) Β· (πβ(π β π)))) β V |
29 | 28 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π)))) β V) |
30 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π = π β ((absβ(π΄βπ)) / π) = ((absβ(π΄βπ)) / π)) |
31 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦
((absβ(π΄βπ)) / π)) = (π β β β¦ ((absβ(π΄βπ)) / π)) |
32 | | ovex 7395 |
. . . . . . . . . . . . 13
β’
((absβ(π΄βπ)) / π) β V |
33 | 30, 31, 32 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ (π β β β ((π β β β¦
((absβ(π΄βπ)) / π))βπ) = ((absβ(π΄βπ)) / π)) |
34 | 33 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) / π))βπ) = ((absβ(π΄βπ)) / π)) |
35 | | nndivre 12201 |
. . . . . . . . . . . 12
β’
(((absβ(π΄βπ)) β β β§ π β β) β ((absβ(π΄βπ)) / π) β β) |
36 | 23, 35 | sylan 581 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((absβ(π΄βπ)) / π) β β) |
37 | 34, 36 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) / π))βπ) β β) |
38 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβ(π β π)) = (πβ(π β π))) |
39 | 38 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = π β ((absβ(π΄βπ)) Β· (πβ(π β π))) = ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
40 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦
((absβ(π΄βπ)) Β· (πβ(π β π)))) = (π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
41 | | ovex 7395 |
. . . . . . . . . . . . 13
β’
((absβ(π΄βπ)) Β· (πβ(π β π))) β V |
42 | 39, 40, 41 | fvmpt 6953 |
. . . . . . . . . . . 12
β’ (π β β β ((π β β β¦
((absβ(π΄βπ)) Β· (πβ(π β π))))βπ) = ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
43 | 42 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π))))βπ) = ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
44 | 21 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π΄βπ) β β) |
45 | 44 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ(π΄βπ)) β β) |
46 | | nnrp 12933 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β+) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β+) |
48 | | elfzelz 13448 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β π β β€) |
49 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . . 19
β’ (β‘π΄ β (π β {0})) β dom π΄ |
50 | 49, 17 | fssdm 6693 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β‘π΄ β (π β {0})) β
β0) |
51 | | plyeq0.6 |
. . . . . . . . . . . . . . . . . . 19
β’ π = sup((β‘π΄ β (π β {0})), β, <
) |
52 | | nn0ssz 12529 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β0 β β€ |
53 | 50, 52 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘π΄ β (π β {0})) β
β€) |
54 | | plyeq0.7 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘π΄ β (π β {0})) β
β
) |
55 | | plyeq0.2 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β
β0) |
56 | 55 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β β) |
57 | 17 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π΄ Fn β0) |
58 | | elpreima 7013 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π΄ Fn β0 β
(π§ β (β‘π΄ β (π β {0})) β (π§ β β0 β§ (π΄βπ§) β (π β {0})))) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π§ β (β‘π΄ β (π β {0})) β (π§ β β0 β§ (π΄βπ§) β (π β {0})))) |
60 | 59 | simplbda 501 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β (π΄βπ§) β (π β {0})) |
61 | | eldifsni 4755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄βπ§) β (π β {0}) β (π΄βπ§) β 0) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β (π΄βπ§) β 0) |
63 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π§ β (π΄βπ) = (π΄βπ§)) |
64 | 63 | neeq1d 3004 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π§ β ((π΄βπ) β 0 β (π΄βπ§) β 0)) |
65 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π§ β (π β€ π β π§ β€ π)) |
66 | 64, 65 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π§ β (((π΄βπ) β 0 β π β€ π) β ((π΄βπ§) β 0 β π§ β€ π))) |
67 | | plyeq0.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (π΄ β
(β€β₯β(π + 1))) = {0}) |
68 | | plyco0 25569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β0
β§ π΄:β0βΆβ) β
((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |
69 | 55, 18, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ((π΄ β
(β€β₯β(π + 1))) = {0} β βπ β β0
((π΄βπ) β 0 β π β€ π))) |
70 | 67, 69 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β βπ β β0 ((π΄βπ) β 0 β π β€ π)) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β βπ β β0
((π΄βπ) β 0 β π β€ π)) |
72 | 50 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β π§ β β0) |
73 | 66, 71, 72 | rspcdva 3585 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β ((π΄βπ§) β 0 β π§ β€ π)) |
74 | 62, 73 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π§ β (β‘π΄ β (π β {0}))) β π§ β€ π) |
75 | 74 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π) |
76 | | brralrspcev 5170 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
βπ§ β (β‘π΄ β (π β {0}))π§ β€ π) β βπ₯ β β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π₯) |
77 | 56, 75, 76 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β βπ₯ β β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π₯) |
78 | | suprzcl 12590 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((β‘π΄ β (π β {0})) β β€ β§ (β‘π΄ β (π β {0})) β β
β§
βπ₯ β β
βπ§ β (β‘π΄ β (π β {0}))π§ β€ π₯) β sup((β‘π΄ β (π β {0})), β, < ) β
(β‘π΄ β (π β {0}))) |
79 | 53, 54, 77, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β sup((β‘π΄ β (π β {0})), β, < ) β
(β‘π΄ β (π β {0}))) |
80 | 51, 79 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β (β‘π΄ β (π β {0}))) |
81 | 50, 80 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β0) |
82 | 81 | nn0zd 12532 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β€) |
83 | | zsubcl 12552 |
. . . . . . . . . . . . . . . 16
β’ ((π β β€ β§ π β β€) β (π β π) β β€) |
84 | 48, 82, 83 | syl2anr 598 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0...π)) β (π β π) β β€) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π β π) β β€) |
86 | 47, 85 | rpexpcld 14157 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ(π β π)) β
β+) |
87 | 86 | rpred 12964 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ(π β π)) β β) |
88 | 45, 87 | remulcld 11192 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((absβ(π΄βπ)) Β· (πβ(π β π))) β β) |
89 | 43, 88 | eqeltrd 2838 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π))))βπ) β β) |
90 | | nnrecre 12202 |
. . . . . . . . . . . . 13
β’ (π β β β (1 /
π) β
β) |
91 | 90 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (1 / π) β
β) |
92 | 22 | absge0d 15336 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ π < π) β 0 β€ (absβ(π΄βπ))) |
93 | 92 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 0 β€
(absβ(π΄βπ))) |
94 | | nnre 12167 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
96 | | nnge1 12188 |
. . . . . . . . . . . . . . 15
β’ (π β β β 1 β€
π) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 1 β€ π) |
98 | | 1red 11163 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 1 β
β) |
99 | 85 | zred 12614 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π β π) β β) |
100 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π < π) |
101 | 48 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π)) β π β β€) |
102 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β€) |
103 | 82 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β€) |
104 | | zltp1le 12560 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β€) β (π < π β (π + 1) β€ π)) |
105 | 102, 103,
104 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π < π β (π + 1) β€ π)) |
106 | 100, 105 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π + 1) β€ π) |
107 | 19 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π)) β π β β0) |
108 | 107 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β π β β) |
109 | 108 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
110 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (0...π)) β π β
β0) |
111 | 110 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (0...π)) β π β β) |
112 | 111 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
113 | 109, 98, 112 | leaddsub2d 11764 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π + 1) β€ π β 1 β€ (π β π))) |
114 | 106, 113 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 1 β€ (π β π)) |
115 | 108 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β π β β) |
116 | 115 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
117 | 111 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0...π)) β π β β) |
118 | 117 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
119 | 116, 118 | negsubdi2d 11535 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β -(π β π) = (π β π)) |
120 | 114, 119 | breqtrrd 5138 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 1 β€ -(π β π)) |
121 | 98, 99, 120 | lenegcon2d 11745 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (π β π) β€ -1) |
122 | | neg1z 12546 |
. . . . . . . . . . . . . . . 16
β’ -1 β
β€ |
123 | | eluz 12784 |
. . . . . . . . . . . . . . . 16
β’ (((π β π) β β€ β§ -1 β β€)
β (-1 β (β€β₯β(π β π)) β (π β π) β€ -1)) |
124 | 85, 122, 123 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (-1 β
(β€β₯β(π β π)) β (π β π) β€ -1)) |
125 | 121, 124 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β -1 β
(β€β₯β(π β π))) |
126 | 95, 97, 125 | leexp2ad 14164 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ(π β π)) β€ (πβ-1)) |
127 | | nncn 12168 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
128 | 127 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β β) |
129 | | expn1 13984 |
. . . . . . . . . . . . . 14
β’ (π β β β (πβ-1) = (1 / π)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ-1) = (1 / π)) |
131 | 126, 130 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ(π β π)) β€ (1 / π)) |
132 | 87, 91, 45, 93, 131 | lemul2ad 12102 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((absβ(π΄βπ)) Β· (πβ(π β π))) β€ ((absβ(π΄βπ)) Β· (1 / π))) |
133 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ(π΄βπ)) β β) |
134 | | nnne0 12194 |
. . . . . . . . . . . . . 14
β’ (π β β β π β 0) |
135 | 134 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β π β 0) |
136 | 133, 128,
135 | divrecd 11941 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((absβ(π΄βπ)) / π) = ((absβ(π΄βπ)) Β· (1 / π))) |
137 | 34, 136 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) / π))βπ) = ((absβ(π΄βπ)) Β· (1 / π))) |
138 | 132, 43, 137 | 3brtr4d 5142 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π))))βπ) β€ ((π β β β¦ ((absβ(π΄βπ)) / π))βπ)) |
139 | 86 | rpge0d 12968 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 0 β€ (πβ(π β π))) |
140 | 45, 87, 93, 139 | mulge0d 11739 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 0 β€
((absβ(π΄βπ)) Β· (πβ(π β π)))) |
141 | 140, 43 | breqtrrd 5138 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β 0 β€ ((π β β β¦
((absβ(π΄βπ)) Β· (πβ(π β π))))βπ)) |
142 | 1, 4, 26, 29, 37, 89, 138, 141 | climsqz2 15531 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π)))) β 0) |
143 | 27 | mptex 7178 |
. . . . . . . . . . 11
β’ (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β V |
144 | 143 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β V) |
145 | 38 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π΄βπ) Β· (πβ(π β π))) = ((π΄βπ) Β· (πβ(π β π)))) |
146 | | eqid 2737 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) = (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) |
147 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ ((π΄βπ) Β· (πβ(π β π))) β V |
148 | 145, 146,
147 | fvmpt 6953 |
. . . . . . . . . . . . . 14
β’ (π β β β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) = ((π΄βπ) Β· (πβ(π β π)))) |
149 | 148 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (0...π)) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) = ((π΄βπ) Β· (πβ(π β π)))) |
150 | 18 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β π΄:β0βΆβ) |
151 | 150, 19, 20 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0...π)) β (π΄βπ) β β) |
152 | 127 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (0...π)) β π β β) |
153 | 134 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (0...π)) β π β 0) |
154 | 82 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β€) |
155 | 48, 154, 83 | syl2anr 598 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (0...π)) β (π β π) β β€) |
156 | 152, 153,
155 | expclzd 14063 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (0...π)) β (πβ(π β π)) β β) |
157 | 151, 156 | mulcld 11182 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (0...π)) β ((π΄βπ) Β· (πβ(π β π))) β β) |
158 | 149, 157 | eqeltrd 2838 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (0...π)) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) β β) |
159 | 158 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) β β) |
160 | 159 | adantlr 714 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) β β) |
161 | 87 | recnd 11190 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (πβ(π β π)) β β) |
162 | 44, 161 | absmuld 15346 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ((π΄βπ) Β· (πβ(π β π)))) = ((absβ(π΄βπ)) Β· (absβ(πβ(π β π))))) |
163 | 87, 139 | absidd 15314 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ(πβ(π β π))) = (πβ(π β π))) |
164 | 163 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((absβ(π΄βπ)) Β· (absβ(πβ(π β π)))) = ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
165 | 162, 164 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ((π΄βπ) Β· (πβ(π β π)))) = ((absβ(π΄βπ)) Β· (πβ(π β π)))) |
166 | 148 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) = ((π΄βπ) Β· (πβ(π β π)))) |
167 | 166 | fveq2d 6851 |
. . . . . . . . . . 11
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β (absβ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ)) = (absβ((π΄βπ) Β· (πβ(π β π))))) |
168 | 165, 167,
43 | 3eqtr4rd 2788 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π < π) β§ π β β) β ((π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π))))βπ) = (absβ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ))) |
169 | 1, 4, 144, 29, 160, 168 | climabs0 15474 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π < π) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β 0 β (π β β β¦ ((absβ(π΄βπ)) Β· (πβ(π β π)))) β 0)) |
170 | 142, 169 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β 0) |
171 | 108 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π < π) β π β β) |
172 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π < π) β π < π) |
173 | 171, 172 | ltned 11298 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π < π) β π β π) |
174 | | velsn 4607 |
. . . . . . . . . . 11
β’ (π β {π} β π = π) |
175 | 174 | necon3bbii 2992 |
. . . . . . . . . 10
β’ (Β¬
π β {π} β π β π) |
176 | 173, 175 | sylibr 233 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π < π) β Β¬ π β {π}) |
177 | 176 | iffalsed 4502 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π < π) β if(π β {π}, (π΄βπ), 0) = 0) |
178 | 170, 177 | breqtrrd 5138 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π < π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β if(π β {π}, (π΄βπ), 0)) |
179 | | nncn 12168 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
180 | 179 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β π β β) |
181 | | nnne0 12194 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β 0) |
182 | 181 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β π β 0) |
183 | 84 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β (π β π) β β€) |
184 | 180, 182,
183 | expclzd 14063 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β (πβ(π β π)) β β) |
185 | 184 | mul02d 11360 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β (0 Β· (πβ(π β π))) = 0) |
186 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β (π΄βπ) = 0) |
187 | 186 | oveq1d 7377 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β ((π΄βπ) Β· (πβ(π β π))) = (0 Β· (πβ(π β π)))) |
188 | 186 | ifeq1d 4510 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β if(π β {π}, (π΄βπ), 0) = if(π β {π}, 0, 0)) |
189 | | ifid 4531 |
. . . . . . . . . . . . 13
β’ if(π β {π}, 0, 0) = 0 |
190 | 188, 189 | eqtrdi 2793 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β if(π β {π}, (π΄βπ), 0) = 0) |
191 | 185, 187,
190 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) = 0) β ((π΄βπ) Β· (πβ(π β π))) = if(π β {π}, (π΄βπ), 0)) |
192 | 21 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (0...π)) β§ π β€ π) β (π΄βπ) β β) |
193 | 192 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (π΄βπ) β β) |
194 | 193 | mulid1d 11179 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β ((π΄βπ) Β· 1) = (π΄βπ)) |
195 | | nn0ssre 12424 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β0 β β |
196 | 50, 195 | sstrdi 3961 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (β‘π΄ β (π β {0})) β
β) |
197 | 196 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β (β‘π΄ β (π β {0})) β
β) |
198 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β (β‘π΄ β (π β {0})) β
β
) |
199 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β βπ₯ β β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π₯) |
200 | 19 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β π β β0) |
201 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π΄:β0βΆ(π βͺ {0}) β§ π β β0)
β (π΄βπ) β (π βͺ {0})) |
202 | 17, 19, 201 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β (0...π)) β (π΄βπ) β (π βͺ {0})) |
203 | 202 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β ((π΄βπ) β (π βͺ {0}) β§ (π΄βπ) β 0)) |
204 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΄βπ) β ((π βͺ {0}) β {0}) β ((π΄βπ) β (π βͺ {0}) β§ (π΄βπ) β 0)) |
205 | 203, 204 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β (π΄βπ) β ((π βͺ {0}) β {0})) |
206 | | difun2 4445 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π βͺ {0}) β {0}) =
(π β
{0}) |
207 | 205, 206 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β (π΄βπ) β (π β {0})) |
208 | | elpreima 7013 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΄ Fn β0 β
(π β (β‘π΄ β (π β {0})) β (π β β0 β§ (π΄βπ) β (π β {0})))) |
209 | 57, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (π β (β‘π΄ β (π β {0})) β (π β β0 β§ (π΄βπ) β (π β {0})))) |
210 | 209 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β (π β (β‘π΄ β (π β {0})) β (π β β0 β§ (π΄βπ) β (π β {0})))) |
211 | 200, 207,
210 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β π β (β‘π΄ β (π β {0}))) |
212 | 197, 198,
199, 211 | suprubd 12124 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β π β€ sup((β‘π΄ β (π β {0})), β, <
)) |
213 | 212, 51 | breqtrrdi 5152 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (0...π)) β§ (π΄βπ) β 0) β π β€ π) |
214 | 213 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β€ π) |
215 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β€ π) |
216 | 108 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β β) |
217 | 111 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β β) |
218 | 216, 217 | letri3d 11304 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (π = π β (π β€ π β§ π β€ π))) |
219 | 214, 215,
218 | mpbir2and 712 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π = π) |
220 | 219 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (π β π) = (π β π)) |
221 | 117 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β β) |
222 | 221 | subidd 11507 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (π β π) = 0) |
223 | 220, 222 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (π β π) = 0) |
224 | 223 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (πβ(π β π)) = (πβ0)) |
225 | 179 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β β) |
226 | 225 | exp0d 14052 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (πβ0) = 1) |
227 | 224, 226 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β (πβ(π β π)) = 1) |
228 | 227 | oveq2d 7378 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β ((π΄βπ) Β· (πβ(π β π))) = ((π΄βπ) Β· 1)) |
229 | 219, 174 | sylibr 233 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β π β {π}) |
230 | 229 | iftrued 4499 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β if(π β {π}, (π΄βπ), 0) = (π΄βπ)) |
231 | 194, 228,
230 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’
(((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β§ (π΄βπ) β 0) β ((π΄βπ) Β· (πβ(π β π))) = if(π β {π}, (π΄βπ), 0)) |
232 | 191, 231 | pm2.61dane 3033 |
. . . . . . . . . 10
β’ ((((π β§ π β (0...π)) β§ π β€ π) β§ π β β) β ((π΄βπ) Β· (πβ(π β π))) = if(π β {π}, (π΄βπ), 0)) |
233 | 232 | mpteq2dva 5210 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β€ π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) = (π β β β¦ if(π β {π}, (π΄βπ), 0))) |
234 | | fconstmpt 5699 |
. . . . . . . . 9
β’ (β
Γ {if(π β {π}, (π΄βπ), 0)}) = (π β β β¦ if(π β {π}, (π΄βπ), 0)) |
235 | 233, 234 | eqtr4di 2795 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β€ π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) = (β Γ {if(π β {π}, (π΄βπ), 0)})) |
236 | | ifcl 4536 |
. . . . . . . . . 10
β’ (((π΄βπ) β β β§ 0 β β)
β if(π β {π}, (π΄βπ), 0) β β) |
237 | 192, 7, 236 | sylancl 587 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β€ π) β if(π β {π}, (π΄βπ), 0) β β) |
238 | | 1z 12540 |
. . . . . . . . 9
β’ 1 β
β€ |
239 | 1 | eqimss2i 4008 |
. . . . . . . . . 10
β’
(β€β₯β1) β β |
240 | 239, 27 | climconst2 15437 |
. . . . . . . . 9
β’
((if(π β {π}, (π΄βπ), 0) β β β§ 1 β β€)
β (β Γ {if(π β {π}, (π΄βπ), 0)}) β if(π β {π}, (π΄βπ), 0)) |
241 | 237, 238,
240 | sylancl 587 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β€ π) β (β Γ {if(π β {π}, (π΄βπ), 0)}) β if(π β {π}, (π΄βπ), 0)) |
242 | 235, 241 | eqbrtrd 5132 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π β€ π) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β if(π β {π}, (π΄βπ), 0)) |
243 | 178, 242,
108, 111 | ltlecasei 11270 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (π β β β¦ ((π΄βπ) Β· (πβ(π β π)))) β if(π β {π}, (π΄βπ), 0)) |
244 | | snex 5393 |
. . . . . . . 8
β’ {0}
β V |
245 | 27, 244 | xpex 7692 |
. . . . . . 7
β’ (β
Γ {0}) β V |
246 | 245 | a1i 11 |
. . . . . 6
β’ (π β (β Γ {0})
β V) |
247 | 159 | anasss 468 |
. . . . . 6
β’ ((π β§ (π β (0...π) β§ π β β)) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) β β) |
248 | | plyeq0.5 |
. . . . . . . . . . . 12
β’ (π β 0π =
(π§ β β β¦
Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))) |
249 | 248 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (π β
(0πβπ) = ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ)) |
250 | 249 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(0πβπ) = ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ)) |
251 | 127 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
252 | | 0pval 25051 |
. . . . . . . . . . 11
β’ (π β β β
(0πβπ) = 0) |
253 | 251, 252 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β
(0πβπ) = 0) |
254 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π§ = π β (π§βπ) = (πβπ)) |
255 | 254 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π§ = π β ((π΄βπ) Β· (π§βπ)) = ((π΄βπ) Β· (πβπ))) |
256 | 255 | sumeq2sdv 15596 |
. . . . . . . . . . . 12
β’ (π§ = π β Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
257 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π§ β β β¦
Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ))) |
258 | | sumex 15579 |
. . . . . . . . . . . 12
β’
Ξ£π β
(0...π)((π΄βπ) Β· (πβπ)) β V |
259 | 256, 257,
258 | fvmpt 6953 |
. . . . . . . . . . 11
β’ (π β β β ((π§ β β β¦
Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
260 | 251, 259 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((π§ β β β¦ Ξ£π β (0...π)((π΄βπ) Β· (π§βπ)))βπ) = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
261 | 250, 253,
260 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ ((π β§ π β β) β 0 = Ξ£π β (0...π)((π΄βπ) Β· (πβπ))) |
262 | 261 | oveq1d 7377 |
. . . . . . . 8
β’ ((π β§ π β β) β (0 / (πβπ)) = (Ξ£π β (0...π)((π΄βπ) Β· (πβπ)) / (πβπ))) |
263 | | expcl 13992 |
. . . . . . . . . 10
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
264 | 127, 81, 263 | syl2anr 598 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) β β) |
265 | 134 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β 0) |
266 | 251, 265,
154 | expne0d 14064 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) β 0) |
267 | 264, 266 | div0d 11937 |
. . . . . . . 8
β’ ((π β§ π β β) β (0 / (πβπ)) = 0) |
268 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ π β β) β (0...π) β Fin) |
269 | | expcl 13992 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β (πβπ) β
β) |
270 | 251, 19, 269 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0...π)) β (πβπ) β β) |
271 | 151, 270 | mulcld 11182 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0...π)) β ((π΄βπ) Β· (πβπ)) β β) |
272 | 268, 264,
271, 266 | fsumdivc 15678 |
. . . . . . . 8
β’ ((π β§ π β β) β (Ξ£π β (0...π)((π΄βπ) Β· (πβπ)) / (πβπ)) = Ξ£π β (0...π)(((π΄βπ) Β· (πβπ)) / (πβπ))) |
273 | 262, 267,
272 | 3eqtr3d 2785 |
. . . . . . 7
β’ ((π β§ π β β) β 0 = Ξ£π β (0...π)(((π΄βπ) Β· (πβπ)) / (πβπ))) |
274 | | fvconst2g 7156 |
. . . . . . . 8
β’ ((0
β β β§ π
β β) β ((β Γ {0})βπ) = 0) |
275 | 8, 274 | sylan 581 |
. . . . . . 7
β’ ((π β§ π β β) β ((β Γ
{0})βπ) =
0) |
276 | 154 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0...π)) β π β β€) |
277 | 48 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (0...π)) β π β β€) |
278 | 152, 153,
276, 277 | expsubd 14069 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0...π)) β (πβ(π β π)) = ((πβπ) / (πβπ))) |
279 | 278 | oveq2d 7378 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0...π)) β ((π΄βπ) Β· (πβ(π β π))) = ((π΄βπ) Β· ((πβπ) / (πβπ)))) |
280 | 264 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0...π)) β (πβπ) β β) |
281 | 266 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (0...π)) β (πβπ) β 0) |
282 | 151, 270,
280, 281 | divassd 11973 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (0...π)) β (((π΄βπ) Β· (πβπ)) / (πβπ)) = ((π΄βπ) Β· ((πβπ) / (πβπ)))) |
283 | 279, 149,
282 | 3eqtr4d 2787 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (0...π)) β ((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) = (((π΄βπ) Β· (πβπ)) / (πβπ))) |
284 | 283 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (0...π)((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ) = Ξ£π β (0...π)(((π΄βπ) Β· (πβπ)) / (πβπ))) |
285 | 273, 275,
284 | 3eqtr4d 2787 |
. . . . . 6
β’ ((π β§ π β β) β ((β Γ
{0})βπ) =
Ξ£π β (0...π)((π β β β¦ ((π΄βπ) Β· (πβ(π β π))))βπ)) |
286 | 1, 2, 3, 243, 246, 247, 285 | climfsum 15712 |
. . . . 5
β’ (π β (β Γ {0})
β Ξ£π β
(0...π)if(π β {π}, (π΄βπ), 0)) |
287 | | suprleub 12128 |
. . . . . . . . . . . 12
β’ ((((β‘π΄ β (π β {0})) β β β§ (β‘π΄ β (π β {0})) β β
β§
βπ₯ β β
βπ§ β (β‘π΄ β (π β {0}))π§ β€ π₯) β§ π β β) β (sup((β‘π΄ β (π β {0})), β, < ) β€ π β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π)) |
288 | 196, 54, 77, 56, 287 | syl31anc 1374 |
. . . . . . . . . . 11
β’ (π β (sup((β‘π΄ β (π β {0})), β, < ) β€ π β βπ§ β (β‘π΄ β (π β {0}))π§ β€ π)) |
289 | 75, 288 | mpbird 257 |
. . . . . . . . . 10
β’ (π β sup((β‘π΄ β (π β {0})), β, < ) β€ π) |
290 | 51, 289 | eqbrtrid 5145 |
. . . . . . . . 9
β’ (π β π β€ π) |
291 | | nn0uz 12812 |
. . . . . . . . . . 11
β’
β0 = (β€β₯β0) |
292 | 81, 291 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ (π β π β
(β€β₯β0)) |
293 | 55 | nn0zd 12532 |
. . . . . . . . . 10
β’ (π β π β β€) |
294 | | elfz5 13440 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β0) β§ π β β€) β (π β (0...π) β π β€ π)) |
295 | 292, 293,
294 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π β (0...π) β π β€ π)) |
296 | 290, 295 | mpbird 257 |
. . . . . . . 8
β’ (π β π β (0...π)) |
297 | 296 | snssd 4774 |
. . . . . . 7
β’ (π β {π} β (0...π)) |
298 | 18, 81 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (π β (π΄βπ) β β) |
299 | | elsni 4608 |
. . . . . . . . . . 11
β’ (π β {π} β π = π) |
300 | 299 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β {π} β (π΄βπ) = (π΄βπ)) |
301 | 300 | eleq1d 2823 |
. . . . . . . . 9
β’ (π β {π} β ((π΄βπ) β β β (π΄βπ) β β)) |
302 | 298, 301 | syl5ibrcom 247 |
. . . . . . . 8
β’ (π β (π β {π} β (π΄βπ) β β)) |
303 | 302 | ralrimiv 3143 |
. . . . . . 7
β’ (π β βπ β {π} (π΄βπ) β β) |
304 | 3 | olcd 873 |
. . . . . . 7
β’ (π β ((0...π) β (β€β₯β0)
β¨ (0...π) β
Fin)) |
305 | | sumss2 15618 |
. . . . . . 7
β’ ((({π} β (0...π) β§ βπ β {π} (π΄βπ) β β) β§ ((0...π) β
(β€β₯β0) β¨ (0...π) β Fin)) β Ξ£π β {π} (π΄βπ) = Ξ£π β (0...π)if(π β {π}, (π΄βπ), 0)) |
306 | 297, 303,
304, 305 | syl21anc 837 |
. . . . . 6
β’ (π β Ξ£π β {π} (π΄βπ) = Ξ£π β (0...π)if(π β {π}, (π΄βπ), 0)) |
307 | | ltso 11242 |
. . . . . . . . 9
β’ < Or
β |
308 | 307 | supex 9406 |
. . . . . . . 8
β’
sup((β‘π΄ β (π β {0})), β, < ) β
V |
309 | 51, 308 | eqeltri 2834 |
. . . . . . 7
β’ π β V |
310 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (π΄βπ) = (π΄βπ)) |
311 | 310 | sumsn 15638 |
. . . . . . 7
β’ ((π β V β§ (π΄βπ) β β) β Ξ£π β {π} (π΄βπ) = (π΄βπ)) |
312 | 309, 298,
311 | sylancr 588 |
. . . . . 6
β’ (π β Ξ£π β {π} (π΄βπ) = (π΄βπ)) |
313 | 306, 312 | eqtr3d 2779 |
. . . . 5
β’ (π β Ξ£π β (0...π)if(π β {π}, (π΄βπ), 0) = (π΄βπ)) |
314 | 286, 313 | breqtrd 5136 |
. . . 4
β’ (π β (β Γ {0})
β (π΄βπ)) |
315 | 239, 27 | climconst2 15437 |
. . . . 5
β’ ((0
β β β§ 1 β β€) β (β Γ {0}) β
0) |
316 | 7, 238, 315 | mp2an 691 |
. . . 4
β’ (β
Γ {0}) β 0 |
317 | | climuni 15441 |
. . . 4
β’
(((β Γ {0}) β (π΄βπ) β§ (β Γ {0}) β 0)
β (π΄βπ) = 0) |
318 | 314, 316,
317 | sylancl 587 |
. . 3
β’ (π β (π΄βπ) = 0) |
319 | | fvex 6860 |
. . . 4
β’ (π΄βπ) β V |
320 | 319 | elsn 4606 |
. . 3
β’ ((π΄βπ) β {0} β (π΄βπ) = 0) |
321 | 318, 320 | sylibr 233 |
. 2
β’ (π β (π΄βπ) β {0}) |
322 | | elpreima 7013 |
. . . . . 6
β’ (π΄ Fn β0 β
(π β (β‘π΄ β (π β {0})) β (π β β0 β§ (π΄βπ) β (π β {0})))) |
323 | 57, 322 | syl 17 |
. . . . 5
β’ (π β (π β (β‘π΄ β (π β {0})) β (π β β0 β§ (π΄βπ) β (π β {0})))) |
324 | 80, 323 | mpbid 231 |
. . . 4
β’ (π β (π β β0 β§ (π΄βπ) β (π β {0}))) |
325 | 324 | simprd 497 |
. . 3
β’ (π β (π΄βπ) β (π β {0})) |
326 | 325 | eldifbd 3928 |
. 2
β’ (π β Β¬ (π΄βπ) β {0}) |
327 | 321, 326 | pm2.65i 193 |
1
β’ Β¬
π |