Step | Hyp | Ref
| Expression |
1 | | fourierdlem25.i |
. . 3
β’ πΌ = sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) |
2 | | ssrab2 4038 |
. . . 4
β’ {π β (0..^π) β£ (πβπ) < πΆ} β (0..^π) |
3 | | ltso 11240 |
. . . . . 6
β’ < Or
β |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β < Or
β) |
5 | | fzofi 13885 |
. . . . . . 7
β’
(0..^π) β
Fin |
6 | | ssfi 9120 |
. . . . . . 7
β’
(((0..^π) β Fin
β§ {π β (0..^π) β£ (πβπ) < πΆ} β (0..^π)) β {π β (0..^π) β£ (πβπ) < πΆ} β Fin) |
7 | 5, 2, 6 | mp2an 691 |
. . . . . 6
β’ {π β (0..^π) β£ (πβπ) < πΆ} β Fin |
8 | 7 | a1i 11 |
. . . . 5
β’ (π β {π β (0..^π) β£ (πβπ) < πΆ} β Fin) |
9 | | 0zd 12516 |
. . . . . . . 8
β’ (π β 0 β
β€) |
10 | | fourierdlem25.m |
. . . . . . . . 9
β’ (π β π β β) |
11 | 10 | nnzd 12531 |
. . . . . . . 8
β’ (π β π β β€) |
12 | 10 | nngt0d 12207 |
. . . . . . . 8
β’ (π β 0 < π) |
13 | | fzolb 13584 |
. . . . . . . 8
β’ (0 β
(0..^π) β (0 β
β€ β§ π β
β€ β§ 0 < π)) |
14 | 9, 11, 12, 13 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β 0 β (0..^π)) |
15 | | fourierdlem25.qf |
. . . . . . . . 9
β’ (π β π:(0...π)βΆβ) |
16 | | elfzofz 13594 |
. . . . . . . . . 10
β’ (0 β
(0..^π) β 0 β
(0...π)) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
β’ (π β 0 β (0...π)) |
18 | 15, 17 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π β (πβ0) β β) |
19 | 10 | nnnn0d 12478 |
. . . . . . . . . . . . 13
β’ (π β π β
β0) |
20 | | nn0uz 12810 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
21 | 19, 20 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ (π β π β
(β€β₯β0)) |
22 | | eluzfz2 13455 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β0) β π β (0...π)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (0...π)) |
24 | 15, 23 | ffvelcdmd 7037 |
. . . . . . . . . 10
β’ (π β (πβπ) β β) |
25 | 18, 24 | iccssred 13357 |
. . . . . . . . 9
β’ (π β ((πβ0)[,](πβπ)) β β) |
26 | | fourierdlem25.cel |
. . . . . . . . 9
β’ (π β πΆ β ((πβ0)[,](πβπ))) |
27 | 25, 26 | sseldd 3946 |
. . . . . . . 8
β’ (π β πΆ β β) |
28 | 18 | rexrd 11210 |
. . . . . . . . 9
β’ (π β (πβ0) β
β*) |
29 | 24 | rexrd 11210 |
. . . . . . . . 9
β’ (π β (πβπ) β
β*) |
30 | | iccgelb 13326 |
. . . . . . . . 9
β’ (((πβ0) β
β* β§ (πβπ) β β* β§ πΆ β ((πβ0)[,](πβπ))) β (πβ0) β€ πΆ) |
31 | 28, 29, 26, 30 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (πβ0) β€ πΆ) |
32 | | fourierdlem25.cnel |
. . . . . . . . . 10
β’ (π β Β¬ πΆ β ran π) |
33 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ πΆ = (πβ0)) β πΆ = (πβ0)) |
34 | 15 | ffnd 6670 |
. . . . . . . . . . . . 13
β’ (π β π Fn (0...π)) |
35 | 34 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ = (πβ0)) β π Fn (0...π)) |
36 | 17 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ = (πβ0)) β 0 β (0...π)) |
37 | | fnfvelrn 7032 |
. . . . . . . . . . . 12
β’ ((π Fn (0...π) β§ 0 β (0...π)) β (πβ0) β ran π) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ πΆ = (πβ0)) β (πβ0) β ran π) |
39 | 33, 38 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ πΆ = (πβ0)) β πΆ β ran π) |
40 | 32, 39 | mtand 815 |
. . . . . . . . 9
β’ (π β Β¬ πΆ = (πβ0)) |
41 | 40 | neqned 2947 |
. . . . . . . 8
β’ (π β πΆ β (πβ0)) |
42 | 18, 27, 31, 41 | leneltd 11314 |
. . . . . . 7
β’ (π β (πβ0) < πΆ) |
43 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = 0 β (πβπ) = (πβ0)) |
44 | 43 | breq1d 5116 |
. . . . . . . 8
β’ (π = 0 β ((πβπ) < πΆ β (πβ0) < πΆ)) |
45 | 44 | elrab 3646 |
. . . . . . 7
β’ (0 β
{π β (0..^π) β£ (πβπ) < πΆ} β (0 β (0..^π) β§ (πβ0) < πΆ)) |
46 | 14, 42, 45 | sylanbrc 584 |
. . . . . 6
β’ (π β 0 β {π β (0..^π) β£ (πβπ) < πΆ}) |
47 | 46 | ne0d 4296 |
. . . . 5
β’ (π β {π β (0..^π) β£ (πβπ) < πΆ} β β
) |
48 | | fzossfz 13597 |
. . . . . . . 8
β’
(0..^π) β
(0...π) |
49 | | fzssz 13449 |
. . . . . . . . 9
β’
(0...π) β
β€ |
50 | | zssre 12511 |
. . . . . . . . 9
β’ β€
β β |
51 | 49, 50 | sstri 3954 |
. . . . . . . 8
β’
(0...π) β
β |
52 | 48, 51 | sstri 3954 |
. . . . . . 7
β’
(0..^π) β
β |
53 | 2, 52 | sstri 3954 |
. . . . . 6
β’ {π β (0..^π) β£ (πβπ) < πΆ} β β |
54 | 53 | a1i 11 |
. . . . 5
β’ (π β {π β (0..^π) β£ (πβπ) < πΆ} β β) |
55 | | fisupcl 9410 |
. . . . 5
β’ (( <
Or β β§ ({π β
(0..^π) β£ (πβπ) < πΆ} β Fin β§ {π β (0..^π) β£ (πβπ) < πΆ} β β
β§ {π β (0..^π) β£ (πβπ) < πΆ} β β)) β sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) β {π β (0..^π) β£ (πβπ) < πΆ}) |
56 | 4, 8, 47, 54, 55 | syl13anc 1373 |
. . . 4
β’ (π β sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) β {π β (0..^π) β£ (πβπ) < πΆ}) |
57 | 2, 56 | sselid 3943 |
. . 3
β’ (π β sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < ) β (0..^π)) |
58 | 1, 57 | eqeltrid 2838 |
. 2
β’ (π β πΌ β (0..^π)) |
59 | 48, 58 | sselid 3943 |
. . . . 5
β’ (π β πΌ β (0...π)) |
60 | 15, 59 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πβπΌ) β β) |
61 | 60 | rexrd 11210 |
. . 3
β’ (π β (πβπΌ) β
β*) |
62 | | fzofzp1 13675 |
. . . . . 6
β’ (πΌ β (0..^π) β (πΌ + 1) β (0...π)) |
63 | 58, 62 | syl 17 |
. . . . 5
β’ (π β (πΌ + 1) β (0...π)) |
64 | 15, 63 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πβ(πΌ + 1)) β β) |
65 | 64 | rexrd 11210 |
. . 3
β’ (π β (πβ(πΌ + 1)) β
β*) |
66 | 1, 56 | eqeltrid 2838 |
. . . . 5
β’ (π β πΌ β {π β (0..^π) β£ (πβπ) < πΆ}) |
67 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
68 | 67 | breq1d 5116 |
. . . . . 6
β’ (π = πΌ β ((πβπ) < πΆ β (πβπΌ) < πΆ)) |
69 | 68 | elrab 3646 |
. . . . 5
β’ (πΌ β {π β (0..^π) β£ (πβπ) < πΆ} β (πΌ β (0..^π) β§ (πβπΌ) < πΆ)) |
70 | 66, 69 | sylib 217 |
. . . 4
β’ (π β (πΌ β (0..^π) β§ (πβπΌ) < πΆ)) |
71 | 70 | simprd 497 |
. . 3
β’ (π β (πβπΌ) < πΆ) |
72 | 52, 58 | sselid 3943 |
. . . . . . . . 9
β’ (π β πΌ β β) |
73 | | ltp1 12000 |
. . . . . . . . . 10
β’ (πΌ β β β πΌ < (πΌ + 1)) |
74 | | id 22 |
. . . . . . . . . . 11
β’ (πΌ β β β πΌ β
β) |
75 | | peano2re 11333 |
. . . . . . . . . . 11
β’ (πΌ β β β (πΌ + 1) β
β) |
76 | 74, 75 | ltnled 11307 |
. . . . . . . . . 10
β’ (πΌ β β β (πΌ < (πΌ + 1) β Β¬ (πΌ + 1) β€ πΌ)) |
77 | 73, 76 | mpbid 231 |
. . . . . . . . 9
β’ (πΌ β β β Β¬
(πΌ + 1) β€ πΌ) |
78 | 72, 77 | syl 17 |
. . . . . . . 8
β’ (π β Β¬ (πΌ + 1) β€ πΌ) |
79 | 48, 49 | sstri 3954 |
. . . . . . . . . . . 12
β’
(0..^π) β
β€ |
80 | 2, 79 | sstri 3954 |
. . . . . . . . . . 11
β’ {π β (0..^π) β£ (πβπ) < πΆ} β β€ |
81 | 80 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β {π β (0..^π) β£ (πβπ) < πΆ} β β€) |
82 | | elrabi 3640 |
. . . . . . . . . . . . . . 15
β’ (β β {π β (0..^π) β£ (πβπ) < πΆ} β β β (0..^π)) |
83 | | elfzo0le 13622 |
. . . . . . . . . . . . . . 15
β’ (β β (0..^π) β β β€ π) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . 14
β’ (β β {π β (0..^π) β£ (πβπ) < πΆ} β β β€ π) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ β β {π β (0..^π) β£ (πβπ) < πΆ}) β β β€ π) |
86 | 85 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π) |
87 | | breq2 5110 |
. . . . . . . . . . . . . 14
β’ (π = π β (β β€ π β β β€ π)) |
88 | 87 | ralbidv 3171 |
. . . . . . . . . . . . 13
β’ (π = π β (ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π β ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π)) |
89 | 88 | rspcev 3580 |
. . . . . . . . . . . 12
β’ ((π β β€ β§
ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π) β βπ β β€ ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π) |
90 | 11, 86, 89 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β βπ β β€ ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π) |
91 | 90 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β βπ β β€ ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π) |
92 | | elfzuz 13443 |
. . . . . . . . . . . . . 14
β’ ((πΌ + 1) β (0...π) β (πΌ + 1) β
(β€β₯β0)) |
93 | 63, 92 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (πΌ + 1) β
(β€β₯β0)) |
94 | 93 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β
(β€β₯β0)) |
95 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β π β β€) |
96 | 51, 63 | sselid 3943 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ + 1) β β) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β β) |
98 | 95 | zred 12612 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β π β β) |
99 | | elfzle2 13451 |
. . . . . . . . . . . . . . 15
β’ ((πΌ + 1) β (0...π) β (πΌ + 1) β€ π) |
100 | 63, 99 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (πΌ + 1) β€ π) |
101 | 100 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β€ π) |
102 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πβ(πΌ + 1)) < πΆ) |
103 | 64 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πβ(πΌ + 1)) β β) |
104 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β πΆ β β) |
105 | 103, 104 | ltnled 11307 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β ((πβ(πΌ + 1)) < πΆ β Β¬ πΆ β€ (πβ(πΌ + 1)))) |
106 | 102, 105 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β Β¬ πΆ β€ (πβ(πΌ + 1))) |
107 | | iccleub 13325 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβ0) β
β* β§ (πβπ) β β* β§ πΆ β ((πβ0)[,](πβπ))) β πΆ β€ (πβπ)) |
108 | 28, 29, 26, 107 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΆ β€ (πβπ)) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = (πΌ + 1)) β πΆ β€ (πβπ)) |
110 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
111 | 110 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π = (πΌ + 1)) β (πβπ) = (πβ(πΌ + 1))) |
112 | 109, 111 | breqtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = (πΌ + 1)) β πΆ β€ (πβ(πΌ + 1))) |
113 | 112 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (πβ(πΌ + 1)) < πΆ) β§ π = (πΌ + 1)) β πΆ β€ (πβ(πΌ + 1))) |
114 | 106, 113 | mtand 815 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β Β¬ π = (πΌ + 1)) |
115 | 114 | neqned 2947 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β π β (πΌ + 1)) |
116 | 97, 98, 101, 115 | leneltd 11314 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) < π) |
117 | | elfzo2 13581 |
. . . . . . . . . . . 12
β’ ((πΌ + 1) β (0..^π) β ((πΌ + 1) β
(β€β₯β0) β§ π β β€ β§ (πΌ + 1) < π)) |
118 | 94, 95, 116, 117 | syl3anbrc 1344 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β (0..^π)) |
119 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
120 | 119 | breq1d 5116 |
. . . . . . . . . . . 12
β’ (π = (πΌ + 1) β ((πβπ) < πΆ β (πβ(πΌ + 1)) < πΆ)) |
121 | 120 | elrab 3646 |
. . . . . . . . . . 11
β’ ((πΌ + 1) β {π β (0..^π) β£ (πβπ) < πΆ} β ((πΌ + 1) β (0..^π) β§ (πβ(πΌ + 1)) < πΆ)) |
122 | 118, 102,
121 | sylanbrc 584 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β {π β (0..^π) β£ (πβπ) < πΆ}) |
123 | | suprzub 12869 |
. . . . . . . . . 10
β’ (({π β (0..^π) β£ (πβπ) < πΆ} β β€ β§ βπ β β€ ββ β {π β (0..^π) β£ (πβπ) < πΆ}β β€ π β§ (πΌ + 1) β {π β (0..^π) β£ (πβπ) < πΆ}) β (πΌ + 1) β€ sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < )) |
124 | 81, 91, 122, 123 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β€ sup({π β (0..^π) β£ (πβπ) < πΆ}, β, < )) |
125 | 124, 1 | breqtrrdi 5148 |
. . . . . . . 8
β’ ((π β§ (πβ(πΌ + 1)) < πΆ) β (πΌ + 1) β€ πΌ) |
126 | 78, 125 | mtand 815 |
. . . . . . 7
β’ (π β Β¬ (πβ(πΌ + 1)) < πΆ) |
127 | | eqcom 2740 |
. . . . . . . . . . 11
β’ ((πβ(πΌ + 1)) = πΆ β πΆ = (πβ(πΌ + 1))) |
128 | 127 | biimpi 215 |
. . . . . . . . . 10
β’ ((πβ(πΌ + 1)) = πΆ β πΆ = (πβ(πΌ + 1))) |
129 | 128 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΌ + 1)) = πΆ) β πΆ = (πβ(πΌ + 1))) |
130 | 34 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) = πΆ) β π Fn (0...π)) |
131 | 63 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) = πΆ) β (πΌ + 1) β (0...π)) |
132 | | fnfvelrn 7032 |
. . . . . . . . . 10
β’ ((π Fn (0...π) β§ (πΌ + 1) β (0...π)) β (πβ(πΌ + 1)) β ran π) |
133 | 130, 131,
132 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΌ + 1)) = πΆ) β (πβ(πΌ + 1)) β ran π) |
134 | 129, 133 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ (πβ(πΌ + 1)) = πΆ) β πΆ β ran π) |
135 | 32, 134 | mtand 815 |
. . . . . . 7
β’ (π β Β¬ (πβ(πΌ + 1)) = πΆ) |
136 | 126, 135 | jca 513 |
. . . . . 6
β’ (π β (Β¬ (πβ(πΌ + 1)) < πΆ β§ Β¬ (πβ(πΌ + 1)) = πΆ)) |
137 | | pm4.56 988 |
. . . . . 6
β’ ((Β¬
(πβ(πΌ + 1)) < πΆ β§ Β¬ (πβ(πΌ + 1)) = πΆ) β Β¬ ((πβ(πΌ + 1)) < πΆ β¨ (πβ(πΌ + 1)) = πΆ)) |
138 | 136, 137 | sylib 217 |
. . . . 5
β’ (π β Β¬ ((πβ(πΌ + 1)) < πΆ β¨ (πβ(πΌ + 1)) = πΆ)) |
139 | 64, 27 | leloed 11303 |
. . . . 5
β’ (π β ((πβ(πΌ + 1)) β€ πΆ β ((πβ(πΌ + 1)) < πΆ β¨ (πβ(πΌ + 1)) = πΆ))) |
140 | 138, 139 | mtbird 325 |
. . . 4
β’ (π β Β¬ (πβ(πΌ + 1)) β€ πΆ) |
141 | 27, 64 | ltnled 11307 |
. . . 4
β’ (π β (πΆ < (πβ(πΌ + 1)) β Β¬ (πβ(πΌ + 1)) β€ πΆ)) |
142 | 140, 141 | mpbird 257 |
. . 3
β’ (π β πΆ < (πβ(πΌ + 1))) |
143 | 61, 65, 27, 71, 142 | eliood 43822 |
. 2
β’ (π β πΆ β ((πβπΌ)(,)(πβ(πΌ + 1)))) |
144 | | fveq2 6843 |
. . . . 5
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
145 | | oveq1 7365 |
. . . . . 6
β’ (π = πΌ β (π + 1) = (πΌ + 1)) |
146 | 145 | fveq2d 6847 |
. . . . 5
β’ (π = πΌ β (πβ(π + 1)) = (πβ(πΌ + 1))) |
147 | 144, 146 | oveq12d 7376 |
. . . 4
β’ (π = πΌ β ((πβπ)(,)(πβ(π + 1))) = ((πβπΌ)(,)(πβ(πΌ + 1)))) |
148 | 147 | eleq2d 2820 |
. . 3
β’ (π = πΌ β (πΆ β ((πβπ)(,)(πβ(π + 1))) β πΆ β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
149 | 148 | rspcev 3580 |
. 2
β’ ((πΌ β (0..^π) β§ πΆ β ((πβπΌ)(,)(πβ(πΌ + 1)))) β βπ β (0..^π)πΆ β ((πβπ)(,)(πβ(π + 1)))) |
150 | 58, 143, 149 | syl2anc 585 |
1
β’ (π β βπ β (0..^π)πΆ β ((πβπ)(,)(πβ(π + 1)))) |