Step | Hyp | Ref
| Expression |
1 | | fourierdlem15.3 |
. . . . . 6
β’ (π β π β (πβπ)) |
2 | | fourierdlem15.2 |
. . . . . . 7
β’ (π β π β β) |
3 | | fourierdlem15.1 |
. . . . . . . 8
β’ π = (π β β β¦ {π β (β βm
(0...π)) β£ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))}) |
4 | 3 | fourierdlem2 44436 |
. . . . . . 7
β’ (π β β β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
5 | 2, 4 | syl 17 |
. . . . . 6
β’ (π β (π β (πβπ) β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))))) |
6 | 1, 5 | mpbid 231 |
. . . . 5
β’ (π β (π β (β βm
(0...π)) β§ (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1))))) |
7 | 6 | simpld 496 |
. . . 4
β’ (π β π β (β βm
(0...π))) |
8 | | reex 11147 |
. . . . . 6
β’ β
β V |
9 | 8 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
10 | | ovex 7391 |
. . . . . 6
β’
(0...π) β
V |
11 | 10 | a1i 11 |
. . . . 5
β’ (π β (0...π) β V) |
12 | 9, 11 | elmapd 8782 |
. . . 4
β’ (π β (π β (β βm
(0...π)) β π:(0...π)βΆβ)) |
13 | 7, 12 | mpbid 231 |
. . 3
β’ (π β π:(0...π)βΆβ) |
14 | | ffn 6669 |
. . 3
β’ (π:(0...π)βΆβ β π Fn (0...π)) |
15 | 13, 14 | syl 17 |
. 2
β’ (π β π Fn (0...π)) |
16 | 6 | simprd 497 |
. . . . . . . . 9
β’ (π β (((πβ0) = π΄ β§ (πβπ) = π΅) β§ βπ β (0..^π)(πβπ) < (πβ(π + 1)))) |
17 | 16 | simpld 496 |
. . . . . . . 8
β’ (π β ((πβ0) = π΄ β§ (πβπ) = π΅)) |
18 | 17 | simpld 496 |
. . . . . . 7
β’ (π β (πβ0) = π΄) |
19 | | nnnn0 12425 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
20 | | nn0uz 12810 |
. . . . . . . . . . 11
β’
β0 = (β€β₯β0) |
21 | 19, 20 | eleqtrdi 2844 |
. . . . . . . . . 10
β’ (π β β β π β
(β€β₯β0)) |
22 | 2, 21 | syl 17 |
. . . . . . . . 9
β’ (π β π β
(β€β₯β0)) |
23 | | eluzfz1 13454 |
. . . . . . . . 9
β’ (π β
(β€β₯β0) β 0 β (0...π)) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (π β 0 β (0...π)) |
25 | 13, 24 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π β (πβ0) β β) |
26 | 18, 25 | eqeltrrd 2835 |
. . . . . 6
β’ (π β π΄ β β) |
27 | 26 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...π)) β π΄ β β) |
28 | 17 | simprd 497 |
. . . . . . 7
β’ (π β (πβπ) = π΅) |
29 | | eluzfz2 13455 |
. . . . . . . . 9
β’ (π β
(β€β₯β0) β π β (0...π)) |
30 | 22, 29 | syl 17 |
. . . . . . . 8
β’ (π β π β (0...π)) |
31 | 13, 30 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π β (πβπ) β β) |
32 | 28, 31 | eqeltrrd 2835 |
. . . . . 6
β’ (π β π΅ β β) |
33 | 32 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0...π)) β π΅ β β) |
34 | 13 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β (0...π)) β (πβπ) β β) |
35 | 18 | eqcomd 2739 |
. . . . . . 7
β’ (π β π΄ = (πβ0)) |
36 | 35 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π)) β π΄ = (πβ0)) |
37 | | elfzuz 13443 |
. . . . . . . 8
β’ (π β (0...π) β π β
(β€β₯β0)) |
38 | 37 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β
(β€β₯β0)) |
39 | 13 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (0...π)) β π:(0...π)βΆβ) |
40 | | 0zd 12516 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...π)) β 0 β β€) |
41 | | elfzel2 13445 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β€) |
42 | 41 | adantr 482 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...π)) β π β β€) |
43 | | elfzelz 13447 |
. . . . . . . . . . 11
β’ (π β (0...π) β π β β€) |
44 | 43 | adantl 483 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...π)) β π β β€) |
45 | | elfzle1 13450 |
. . . . . . . . . . 11
β’ (π β (0...π) β 0 β€ π) |
46 | 45 | adantl 483 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...π)) β 0 β€ π) |
47 | 43 | zred 12612 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
48 | 47 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...π)) β π β β) |
49 | | elfzelz 13447 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β€) |
50 | 49 | zred 12612 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...π)) β π β β) |
52 | 41 | zred 12612 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β) |
53 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...π)) β π β β) |
54 | | elfzle2 13451 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β€ π) |
55 | 54 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...π)) β π β€ π) |
56 | | elfzle2 13451 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β€ π) |
57 | 56 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...π)) β π β€ π) |
58 | 48, 51, 53, 55, 57 | letrd 11317 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...π)) β π β€ π) |
59 | 40, 42, 44, 46, 58 | elfzd 13438 |
. . . . . . . . 9
β’ ((π β (0...π) β§ π β (0...π)) β π β (0...π)) |
60 | 59 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (0...π)) β π β (0...π)) |
61 | 39, 60 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π β (0...π)) β (πβπ) β β) |
62 | | simpll 766 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (0...(π β 1))) β π) |
63 | | elfzle1 13450 |
. . . . . . . . . . 11
β’ (π β (0...(π β 1)) β 0 β€ π) |
64 | 63 | adantl 483 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...(π β 1))) β 0 β€ π) |
65 | | elfzelz 13447 |
. . . . . . . . . . . . 13
β’ (π β (0...(π β 1)) β π β β€) |
66 | 65 | zred 12612 |
. . . . . . . . . . . 12
β’ (π β (0...(π β 1)) β π β β) |
67 | 66 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β β) |
68 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β β) |
69 | 52 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β β) |
70 | | peano2rem 11473 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β) |
71 | 68, 70 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (0...(π β 1))) β (π β 1) β β) |
72 | | elfzle2 13451 |
. . . . . . . . . . . . 13
β’ (π β (0...(π β 1)) β π β€ (π β 1)) |
73 | 72 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β€ (π β 1)) |
74 | 68 | ltm1d 12092 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (0...(π β 1))) β (π β 1) < π) |
75 | 67, 71, 68, 73, 74 | lelttrd 11318 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π < π) |
76 | 56 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β€ π) |
77 | 67, 68, 69, 75, 76 | ltletrd 11320 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π < π) |
78 | 65 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β β€) |
79 | | 0zd 12516 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β 0 β
β€) |
80 | 41 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β β€) |
81 | | elfzo 13580 |
. . . . . . . . . . 11
β’ ((π β β€ β§ 0 β
β€ β§ π β
β€) β (π β
(0..^π) β (0 β€
π β§ π < π))) |
82 | 78, 79, 80, 81 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β (0...π) β§ π β (0...(π β 1))) β (π β (0..^π) β (0 β€ π β§ π < π))) |
83 | 64, 77, 82 | mpbir2and 712 |
. . . . . . . . 9
β’ ((π β (0...π) β§ π β (0...(π β 1))) β π β (0..^π)) |
84 | 83 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (0...(π β 1))) β π β (0..^π)) |
85 | 13 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π:(0...π)βΆβ) |
86 | | elfzofz 13594 |
. . . . . . . . . . 11
β’ (π β (0..^π) β π β (0...π)) |
87 | 86 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β π β (0...π)) |
88 | 85, 87 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβπ) β β) |
89 | | fzofzp1 13675 |
. . . . . . . . . . 11
β’ (π β (0..^π) β (π + 1) β (0...π)) |
90 | 89 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (π + 1) β (0...π)) |
91 | 85, 90 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) β β) |
92 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π = π β (π β (0..^π) β π β (0..^π))) |
93 | 92 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = π β ((π β§ π β (0..^π)) β (π β§ π β (0..^π)))) |
94 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ) = (πβπ)) |
95 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π = π β (π + 1) = (π + 1)) |
96 | 95 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
97 | 94, 96 | breq12d 5119 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ) < (πβ(π + 1)) β (πβπ) < (πβ(π + 1)))) |
98 | 93, 97 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = π β (((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) β ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))))) |
99 | 16 | simprd 497 |
. . . . . . . . . . 11
β’ (π β βπ β (0..^π)(πβπ) < (πβ(π + 1))) |
100 | 99 | r19.21bi 3233 |
. . . . . . . . . 10
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
101 | 98, 100 | chvarvv 2003 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (πβπ) < (πβ(π + 1))) |
102 | 88, 91, 101 | ltled 11308 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (πβπ) β€ (πβ(π + 1))) |
103 | 62, 84, 102 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π β (0...(π β 1))) β (πβπ) β€ (πβ(π + 1))) |
104 | 38, 61, 103 | monoord 13944 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβ0) β€ (πβπ)) |
105 | 36, 104 | eqbrtrd 5128 |
. . . . 5
β’ ((π β§ π β (0...π)) β π΄ β€ (πβπ)) |
106 | | elfzuz3 13444 |
. . . . . . . 8
β’ (π β (0...π) β π β (β€β₯βπ)) |
107 | 106 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0...π)) β π β (β€β₯βπ)) |
108 | 13 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (π...π)) β π:(0...π)βΆβ) |
109 | | fz0fzelfz0 13553 |
. . . . . . . . 9
β’ ((π β (0...π) β§ π β (π...π)) β π β (0...π)) |
110 | 109 | adantll 713 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (π...π)) β π β (0...π)) |
111 | 108, 110 | ffvelcdmd 7037 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π β (π...π)) β (πβπ) β β) |
112 | 13 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π:(0...π)βΆβ) |
113 | | 0zd 12516 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β 0 β
β€) |
114 | 41 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β β€) |
115 | | elfzelz 13447 |
. . . . . . . . . . 11
β’ (π β (π...(π β 1)) β π β β€) |
116 | 115 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β β€) |
117 | | 0red 11163 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (π...(π β 1))) β 0 β
β) |
118 | 50 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (π...(π β 1))) β π β β) |
119 | 115 | zred 12612 |
. . . . . . . . . . . . 13
β’ (π β (π...(π β 1)) β π β β) |
120 | 119 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (π...(π β 1))) β π β β) |
121 | | elfzle1 13450 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β 0 β€ π) |
122 | 121 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (π...(π β 1))) β 0 β€ π) |
123 | | elfzle1 13450 |
. . . . . . . . . . . . 13
β’ (π β (π...(π β 1)) β π β€ π) |
124 | 123 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (0...π) β§ π β (π...(π β 1))) β π β€ π) |
125 | 117, 118,
120, 122, 124 | letrd 11317 |
. . . . . . . . . . 11
β’ ((π β (0...π) β§ π β (π...(π β 1))) β 0 β€ π) |
126 | 125 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β 0 β€ π) |
127 | 119 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(π β 1))) β π β β) |
128 | 2 | nnred 12173 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
129 | 128 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(π β 1))) β π β β) |
130 | | 1red 11161 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π...(π β 1))) β 1 β
β) |
131 | 129, 130 | resubcld 11588 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(π β 1))) β (π β 1) β β) |
132 | | elfzle2 13451 |
. . . . . . . . . . . . . 14
β’ (π β (π...(π β 1)) β π β€ (π β 1)) |
133 | 132 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(π β 1))) β π β€ (π β 1)) |
134 | 129 | ltm1d 12092 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(π β 1))) β (π β 1) < π) |
135 | 127, 131,
129, 133, 134 | lelttrd 11318 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(π β 1))) β π < π) |
136 | 127, 129,
135 | ltled 11308 |
. . . . . . . . . . 11
β’ ((π β§ π β (π...(π β 1))) β π β€ π) |
137 | 136 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β€ π) |
138 | 113, 114,
116, 126, 137 | elfzd 13438 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β (0...π)) |
139 | 112, 138 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (πβπ) β β) |
140 | 116 | peano2zd 12615 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (π + 1) β β€) |
141 | 119 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β β) |
142 | | 1red 11161 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β 1 β
β) |
143 | | 0le1 11683 |
. . . . . . . . . . . 12
β’ 0 β€
1 |
144 | 143 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β 0 β€
1) |
145 | 141, 142,
126, 144 | addge0d 11736 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β 0 β€ (π + 1)) |
146 | 127, 131,
130, 133 | leadd1dd 11774 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β€ ((π β 1) + 1)) |
147 | 2 | nncnd 12174 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
148 | 147 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(π β 1))) β π β β) |
149 | | 1cnd 11155 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π...(π β 1))) β 1 β
β) |
150 | 148, 149 | npcand 11521 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...(π β 1))) β ((π β 1) + 1) = π) |
151 | 146, 150 | breqtrd 5132 |
. . . . . . . . . . 11
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β€ π) |
152 | 151 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (π + 1) β€ π) |
153 | 113, 114,
140, 145, 152 | elfzd 13438 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (π + 1) β (0...π)) |
154 | 112, 153 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (πβ(π + 1)) β β) |
155 | | simpll 766 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π) |
156 | 135 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π < π) |
157 | 116, 113,
114, 81 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (π β (0..^π) β (0 β€ π β§ π < π))) |
158 | 126, 156,
157 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β π β (0..^π)) |
159 | 155, 158,
101 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (πβπ) < (πβ(π + 1))) |
160 | 139, 154,
159 | ltled 11308 |
. . . . . . 7
β’ (((π β§ π β (0...π)) β§ π β (π...(π β 1))) β (πβπ) β€ (πβ(π + 1))) |
161 | 107, 111,
160 | monoord 13944 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβπ) β€ (πβπ)) |
162 | 28 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (0...π)) β (πβπ) = π΅) |
163 | 161, 162 | breqtrd 5132 |
. . . . 5
β’ ((π β§ π β (0...π)) β (πβπ) β€ π΅) |
164 | 27, 33, 34, 105, 163 | eliccd 43828 |
. . . 4
β’ ((π β§ π β (0...π)) β (πβπ) β (π΄[,]π΅)) |
165 | 164 | ralrimiva 3140 |
. . 3
β’ (π β βπ β (0...π)(πβπ) β (π΄[,]π΅)) |
166 | | fnfvrnss 7069 |
. . 3
β’ ((π Fn (0...π) β§ βπ β (0...π)(πβπ) β (π΄[,]π΅)) β ran π β (π΄[,]π΅)) |
167 | 15, 165, 166 | syl2anc 585 |
. 2
β’ (π β ran π β (π΄[,]π΅)) |
168 | | df-f 6501 |
. 2
β’ (π:(0...π)βΆ(π΄[,]π΅) β (π Fn (0...π) β§ ran π β (π΄[,]π΅))) |
169 | 15, 167, 168 | sylanbrc 584 |
1
β’ (π β π:(0...π)βΆ(π΄[,]π΅)) |