Step | Hyp | Ref
| Expression |
1 | | fourierdlem20.i |
. . 3
β’ πΌ = sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) |
2 | | ssrab2 4038 |
. . . 4
β’ {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β (0..^π) |
3 | | fzossfz 13597 |
. . . . . . . 8
β’
(0..^π) β
(0...π) |
4 | | fzssz 13449 |
. . . . . . . 8
β’
(0...π) β
β€ |
5 | 3, 4 | sstri 3954 |
. . . . . . 7
β’
(0..^π) β
β€ |
6 | 2, 5 | sstri 3954 |
. . . . . 6
β’ {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β€ |
7 | 6 | a1i 11 |
. . . . 5
β’ (π β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β€) |
8 | | 0z 12515 |
. . . . . . . . . 10
β’ 0 β
β€ |
9 | | 0le0 12259 |
. . . . . . . . . 10
β’ 0 β€
0 |
10 | | eluz2 12774 |
. . . . . . . . . 10
β’ (0 β
(β€β₯β0) β (0 β β€ β§ 0 β
β€ β§ 0 β€ 0)) |
11 | 8, 8, 9, 10 | mpbir3an 1342 |
. . . . . . . . 9
β’ 0 β
(β€β₯β0) |
12 | 11 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β
(β€β₯β0)) |
13 | | fourierdlem20.m |
. . . . . . . . 9
β’ (π β π β β) |
14 | 13 | nnzd 12531 |
. . . . . . . 8
β’ (π β π β β€) |
15 | 13 | nngt0d 12207 |
. . . . . . . 8
β’ (π β 0 < π) |
16 | | elfzo2 13581 |
. . . . . . . 8
β’ (0 β
(0..^π) β (0 β
(β€β₯β0) β§ π β β€ β§ 0 < π)) |
17 | 12, 14, 15, 16 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β 0 β (0..^π)) |
18 | | fourierdlem20.q |
. . . . . . . . 9
β’ (π β π:(0...π)βΆβ) |
19 | 3, 17 | sselid 3943 |
. . . . . . . . 9
β’ (π β 0 β (0...π)) |
20 | 18, 19 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π β (πβ0) β β) |
21 | | fourierdlem20.a |
. . . . . . . 8
β’ (π β π΄ β β) |
22 | | fourierdlem20.t |
. . . . . . . . . . 11
β’ π = ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) |
23 | 21 | rexrd 11210 |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β
β*) |
24 | | fourierdlem20.b |
. . . . . . . . . . . . . . . 16
β’ (π β π΅ β β) |
25 | 24 | rexrd 11210 |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β
β*) |
26 | | fourierdlem20.aleb |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β€ π΅) |
27 | | lbicc2 13387 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΄ β (π΄[,]π΅)) |
28 | 23, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π΄[,]π΅)) |
29 | | ubicc2 13388 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β β*
β§ π΅ β
β* β§ π΄
β€ π΅) β π΅ β (π΄[,]π΅)) |
30 | 23, 25, 26, 29 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β (π΄[,]π΅)) |
31 | 28, 30 | jca 513 |
. . . . . . . . . . . . 13
β’ (π β (π΄ β (π΄[,]π΅) β§ π΅ β (π΄[,]π΅))) |
32 | | prssg 4780 |
. . . . . . . . . . . . . 14
β’ ((π΄ β β*
β§ π΅ β
β*) β ((π΄ β (π΄[,]π΅) β§ π΅ β (π΄[,]π΅)) β {π΄, π΅} β (π΄[,]π΅))) |
33 | 23, 25, 32 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β ((π΄ β (π΄[,]π΅) β§ π΅ β (π΄[,]π΅)) β {π΄, π΅} β (π΄[,]π΅))) |
34 | 31, 33 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β {π΄, π΅} β (π΄[,]π΅)) |
35 | | inss2 4190 |
. . . . . . . . . . . . . 14
β’ (ran
π β© (π΄(,)π΅)) β (π΄(,)π΅) |
36 | | ioossicc 13356 |
. . . . . . . . . . . . . 14
β’ (π΄(,)π΅) β (π΄[,]π΅) |
37 | 35, 36 | sstri 3954 |
. . . . . . . . . . . . 13
β’ (ran
π β© (π΄(,)π΅)) β (π΄[,]π΅) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (ran π β© (π΄(,)π΅)) β (π΄[,]π΅)) |
39 | 34, 38 | unssd 4147 |
. . . . . . . . . . 11
β’ (π β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅))) β (π΄[,]π΅)) |
40 | 22, 39 | eqsstrid 3993 |
. . . . . . . . . 10
β’ (π β π β (π΄[,]π΅)) |
41 | 21, 24 | iccssred 13357 |
. . . . . . . . . 10
β’ (π β (π΄[,]π΅) β β) |
42 | 40, 41 | sstrd 3955 |
. . . . . . . . 9
β’ (π β π β β) |
43 | | fourierdlem20.s |
. . . . . . . . . . 11
β’ (π β π Isom < , < ((0...π), π)) |
44 | | isof1o 7269 |
. . . . . . . . . . 11
β’ (π Isom < , < ((0...π), π) β π:(0...π)β1-1-ontoβπ) |
45 | | f1of 6785 |
. . . . . . . . . . 11
β’ (π:(0...π)β1-1-ontoβπ β π:(0...π)βΆπ) |
46 | 43, 44, 45 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π:(0...π)βΆπ) |
47 | | fourierdlem20.j |
. . . . . . . . . . 11
β’ (π β π½ β (0..^π)) |
48 | | elfzofz 13594 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β π½ β (0...π)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . 10
β’ (π β π½ β (0...π)) |
50 | 46, 49 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (π β (πβπ½) β π) |
51 | 42, 50 | sseldd 3946 |
. . . . . . . 8
β’ (π β (πβπ½) β β) |
52 | | fourierdlem20.q0 |
. . . . . . . 8
β’ (π β (πβ0) β€ π΄) |
53 | 40, 50 | sseldd 3946 |
. . . . . . . . 9
β’ (π β (πβπ½) β (π΄[,]π΅)) |
54 | | iccgelb 13326 |
. . . . . . . . 9
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πβπ½) β (π΄[,]π΅)) β π΄ β€ (πβπ½)) |
55 | 23, 25, 53, 54 | syl3anc 1372 |
. . . . . . . 8
β’ (π β π΄ β€ (πβπ½)) |
56 | 20, 21, 51, 52, 55 | letrd 11317 |
. . . . . . 7
β’ (π β (πβ0) β€ (πβπ½)) |
57 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = 0 β (πβπ) = (πβ0)) |
58 | 57 | breq1d 5116 |
. . . . . . . 8
β’ (π = 0 β ((πβπ) β€ (πβπ½) β (πβ0) β€ (πβπ½))) |
59 | 58 | elrab 3646 |
. . . . . . 7
β’ (0 β
{π β (0..^π) β£ (πβπ) β€ (πβπ½)} β (0 β (0..^π) β§ (πβ0) β€ (πβπ½))) |
60 | 17, 56, 59 | sylanbrc 584 |
. . . . . 6
β’ (π β 0 β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) |
61 | 60 | ne0d 4296 |
. . . . 5
β’ (π β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β
) |
62 | 13 | nnred 12173 |
. . . . . 6
β’ (π β π β β) |
63 | 2 | sseli 3941 |
. . . . . . . . 9
β’ (π β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β π β (0..^π)) |
64 | | elfzo0le 13622 |
. . . . . . . . 9
β’ (π β (0..^π) β π β€ π) |
65 | 63, 64 | syl 17 |
. . . . . . . 8
β’ (π β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β π β€ π) |
66 | 65 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) β π β€ π) |
67 | 66 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π) |
68 | | breq2 5110 |
. . . . . . . 8
β’ (π₯ = π β (π β€ π₯ β π β€ π)) |
69 | 68 | ralbidv 3171 |
. . . . . . 7
β’ (π₯ = π β (βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯ β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π)) |
70 | 69 | rspcev 3580 |
. . . . . 6
β’ ((π β β β§
βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π) β βπ₯ β β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯) |
71 | 62, 67, 70 | syl2anc 585 |
. . . . 5
β’ (π β βπ₯ β β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯) |
72 | | suprzcl 12588 |
. . . . 5
β’ (({π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β€ β§ {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β
β§ βπ₯ β β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯) β sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) |
73 | 7, 61, 71, 72 | syl3anc 1372 |
. . . 4
β’ (π β sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) |
74 | 2, 73 | sselid 3943 |
. . 3
β’ (π β sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) β (0..^π)) |
75 | 1, 74 | eqeltrid 2838 |
. 2
β’ (π β πΌ β (0..^π)) |
76 | 3, 75 | sselid 3943 |
. . . . 5
β’ (π β πΌ β (0...π)) |
77 | 18, 76 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πβπΌ) β β) |
78 | 77 | rexrd 11210 |
. . 3
β’ (π β (πβπΌ) β
β*) |
79 | | fzofzp1 13675 |
. . . . . 6
β’ (πΌ β (0..^π) β (πΌ + 1) β (0...π)) |
80 | 75, 79 | syl 17 |
. . . . 5
β’ (π β (πΌ + 1) β (0...π)) |
81 | 18, 80 | ffvelcdmd 7037 |
. . . 4
β’ (π β (πβ(πΌ + 1)) β β) |
82 | 81 | rexrd 11210 |
. . 3
β’ (π β (πβ(πΌ + 1)) β
β*) |
83 | 1, 73 | eqeltrid 2838 |
. . . . 5
β’ (π β πΌ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) |
84 | | nfrab1 3425 |
. . . . . . . 8
β’
β²π{π β (0..^π) β£ (πβπ) β€ (πβπ½)} |
85 | | nfcv 2904 |
. . . . . . . 8
β’
β²πβ |
86 | | nfcv 2904 |
. . . . . . . 8
β’
β²π
< |
87 | 84, 85, 86 | nfsup 9392 |
. . . . . . 7
β’
β²πsup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < ) |
88 | 1, 87 | nfcxfr 2902 |
. . . . . 6
β’
β²ππΌ |
89 | | nfcv 2904 |
. . . . . 6
β’
β²π(0..^π) |
90 | | nfcv 2904 |
. . . . . . . 8
β’
β²ππ |
91 | 90, 88 | nffv 6853 |
. . . . . . 7
β’
β²π(πβπΌ) |
92 | | nfcv 2904 |
. . . . . . 7
β’
β²π
β€ |
93 | | nfcv 2904 |
. . . . . . 7
β’
β²π(πβπ½) |
94 | 91, 92, 93 | nfbr 5153 |
. . . . . 6
β’
β²π(πβπΌ) β€ (πβπ½) |
95 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
96 | 95 | breq1d 5116 |
. . . . . 6
β’ (π = πΌ β ((πβπ) β€ (πβπ½) β (πβπΌ) β€ (πβπ½))) |
97 | 88, 89, 94, 96 | elrabf 3642 |
. . . . 5
β’ (πΌ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β (πΌ β (0..^π) β§ (πβπΌ) β€ (πβπ½))) |
98 | 83, 97 | sylib 217 |
. . . 4
β’ (π β (πΌ β (0..^π) β§ (πβπΌ) β€ (πβπ½))) |
99 | 98 | simprd 497 |
. . 3
β’ (π β (πβπΌ) β€ (πβπ½)) |
100 | | simpr 486 |
. . . . . 6
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) |
101 | 82 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β (πβ(πΌ + 1)) β
β*) |
102 | | iccssxr 13353 |
. . . . . . . . . 10
β’ (π΄[,]π΅) β
β* |
103 | 40, 102 | sstrdi 3957 |
. . . . . . . . 9
β’ (π β π β
β*) |
104 | | fzofzp1 13675 |
. . . . . . . . . . 11
β’ (π½ β (0..^π) β (π½ + 1) β (0...π)) |
105 | 47, 104 | syl 17 |
. . . . . . . . . 10
β’ (π β (π½ + 1) β (0...π)) |
106 | 46, 105 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (π β (πβ(π½ + 1)) β π) |
107 | 103, 106 | sseldd 3946 |
. . . . . . . 8
β’ (π β (πβ(π½ + 1)) β
β*) |
108 | 107 | adantr 482 |
. . . . . . 7
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β (πβ(π½ + 1)) β
β*) |
109 | | xrltnle 11227 |
. . . . . . 7
β’ (((πβ(πΌ + 1)) β β* β§
(πβ(π½ + 1)) β β*) β
((πβ(πΌ + 1)) < (πβ(π½ + 1)) β Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1)))) |
110 | 101, 108,
109 | syl2anc 585 |
. . . . . 6
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β ((πβ(πΌ + 1)) < (πβ(π½ + 1)) β Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1)))) |
111 | 100, 110 | mpbird 257 |
. . . . 5
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β (πβ(πΌ + 1)) < (πβ(π½ + 1))) |
112 | | fzssz 13449 |
. . . . . 6
β’
(0...π) β
β€ |
113 | | f1ofo 6792 |
. . . . . . . . . 10
β’ (π:(0...π)β1-1-ontoβπ β π:(0...π)βontoβπ) |
114 | 43, 44, 113 | 3syl 18 |
. . . . . . . . 9
β’ (π β π:(0...π)βontoβπ) |
115 | 114 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β π:(0...π)βontoβπ) |
116 | | ffun 6672 |
. . . . . . . . . . . . . 14
β’ (π:(0...π)βΆβ β Fun π) |
117 | 18, 116 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β Fun π) |
118 | 18 | fdmd 6680 |
. . . . . . . . . . . . . . 15
β’ (π β dom π = (0...π)) |
119 | 118 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) = dom π) |
120 | 80, 119 | eleqtrd 2836 |
. . . . . . . . . . . . 13
β’ (π β (πΌ + 1) β dom π) |
121 | | fvelrn 7028 |
. . . . . . . . . . . . 13
β’ ((Fun
π β§ (πΌ + 1) β dom π) β (πβ(πΌ + 1)) β ran π) |
122 | 117, 120,
121 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (πβ(πΌ + 1)) β ran π) |
123 | 122 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β ran π) |
124 | 23 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β π΄ β
β*) |
125 | 25 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β π΅ β
β*) |
126 | 81 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β β) |
127 | 41, 53 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ½) β β) |
128 | 4 | sseli 3941 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΌ β (0...π) β πΌ β β€) |
129 | | zre 12508 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΌ β β€ β πΌ β
β) |
130 | 76, 128, 129 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΌ β β) |
131 | 130 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β πΌ β β) |
132 | 131 | ltp1d 12090 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β πΌ < (πΌ + 1)) |
133 | 132 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β πΌ < (πΌ + 1)) |
134 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β (πβ(πΌ + 1)) β β) |
135 | 127 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β (πβπ½) β β) |
136 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β Β¬ (πβπ½) < (πβ(πΌ + 1))) |
137 | 134, 135,
136 | nltled 11310 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β (πβ(πΌ + 1)) β€ (πβπ½)) |
138 | 130 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β πΌ β β) |
139 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β 1 β β) |
140 | 138, 139 | readdcld 11189 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πΌ + 1) β β) |
141 | | elfzoelz 13578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (0..^π) β π β β€) |
142 | 141 | zred 12612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (0..^π) β π β β) |
143 | 142 | ssriv 3949 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(0..^π) β
β |
144 | 2, 143 | sstri 3954 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β) |
146 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β
) |
147 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β βπ₯ β β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯) |
148 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβ(πΌ + 1)) β β) |
149 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβπ½) β β) |
150 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β π΅ β β) |
151 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβ(πΌ + 1)) β€ (πβπ½)) |
152 | 42, 106 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (πβ(π½ + 1)) β β) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβ(π½ + 1)) β β) |
154 | | elfzoelz 13578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π½ β (0..^π) β π½ β β€) |
155 | | zre 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π½ β β€ β π½ β
β) |
156 | 47, 154, 155 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π½ β β) |
157 | 156 | ltp1d 12090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π½ < (π½ + 1)) |
158 | | isorel 7272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π Isom < , < ((0...π), π) β§ (π½ β (0...π) β§ (π½ + 1) β (0...π))) β (π½ < (π½ + 1) β (πβπ½) < (πβ(π½ + 1)))) |
159 | 43, 49, 105, 158 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (π½ < (π½ + 1) β (πβπ½) < (πβ(π½ + 1)))) |
160 | 157, 159 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (πβπ½) < (πβ(π½ + 1))) |
161 | 160 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβπ½) < (πβ(π½ + 1))) |
162 | 40, 106 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (πβ(π½ + 1)) β (π΄[,]π΅)) |
163 | | iccleub 13325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π΄ β β*
β§ π΅ β
β* β§ (πβ(π½ + 1)) β (π΄[,]π΅)) β (πβ(π½ + 1)) β€ π΅) |
164 | 23, 25, 162, 163 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β (πβ(π½ + 1)) β€ π΅) |
165 | 164 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβ(π½ + 1)) β€ π΅) |
166 | 149, 153,
150, 161, 165 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβπ½) < π΅) |
167 | 148, 149,
150, 151, 166 | lelttrd 11318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πβ(πΌ + 1)) < π΅) |
168 | 167 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β§ Β¬ (πΌ + 1) β (0..^π)) β (πβ(πΌ + 1)) < π΅) |
169 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β π΅ β β) |
170 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πβ(πΌ + 1)) β β) |
171 | | fourierdlem20.qm |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π΅ β€ (πβπ)) |
172 | 171 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β π΅ β€ (πβπ)) |
173 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β π β β€) |
174 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) β (0...π)) |
175 | | fzval3 13647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β β€ β
(0...π) = (0..^(π + 1))) |
176 | 14, 175 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β (0...π) = (0..^(π + 1))) |
177 | 176 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (0...π) = (0..^(π + 1))) |
178 | 174, 177 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) β (0..^(π + 1))) |
179 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β Β¬ (πΌ + 1) β (0..^π)) |
180 | 178, 179 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β ((πΌ + 1) β (0..^(π + 1)) β§ Β¬ (πΌ + 1) β (0..^π))) |
181 | | elfzonelfzo 13680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β β€ β (((πΌ + 1) β (0..^(π + 1)) β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) β (π..^(π + 1)))) |
182 | 173, 180,
181 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) β (π..^(π + 1))) |
183 | | fzval3 13647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β β€ β (π...π) = (π..^(π + 1))) |
184 | 14, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (π...π) = (π..^(π + 1))) |
185 | 184 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (π..^(π + 1)) = (π...π)) |
186 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (π..^(π + 1)) = (π...π)) |
187 | 182, 186 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) β (π...π)) |
188 | | elfz1eq 13458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΌ + 1) β (π...π) β (πΌ + 1) = π) |
189 | 187, 188 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πΌ + 1) = π) |
190 | 189 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β π = (πΌ + 1)) |
191 | 190 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β (πβπ) = (πβ(πΌ + 1))) |
192 | 172, 191 | breqtrd 5132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β π΅ β€ (πβ(πΌ + 1))) |
193 | 169, 170,
192 | lensymd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ Β¬ (πΌ + 1) β (0..^π)) β Β¬ (πβ(πΌ + 1)) < π΅) |
194 | 193 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β§ Β¬ (πΌ + 1) β (0..^π)) β Β¬ (πβ(πΌ + 1)) < π΅) |
195 | 168, 194 | condan 817 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πΌ + 1) β (0..^π)) |
196 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π
+ |
197 | | nfcv 2904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π1 |
198 | 88, 196, 197 | nfov 7388 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(πΌ + 1) |
199 | 90, 198 | nffv 6853 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
β²π(πβ(πΌ + 1)) |
200 | 199, 92, 93 | nfbr 5153 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
β²π(πβ(πΌ + 1)) β€ (πβπ½) |
201 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (πΌ + 1) β (πβπ) = (πβ(πΌ + 1))) |
202 | 201 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πΌ + 1) β ((πβπ) β€ (πβπ½) β (πβ(πΌ + 1)) β€ (πβπ½))) |
203 | 198, 89, 200, 202 | elrabf 3642 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΌ + 1) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β ((πΌ + 1) β (0..^π) β§ (πβ(πΌ + 1)) β€ (πβπ½))) |
204 | 195, 151,
203 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πΌ + 1) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) |
205 | | suprub 12121 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((({π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β β§ {π β (0..^π) β£ (πβπ) β€ (πβπ½)} β β
β§ βπ₯ β β βπ β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}π β€ π₯) β§ (πΌ + 1) β {π β (0..^π) β£ (πβπ) β€ (πβπ½)}) β (πΌ + 1) β€ sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < )) |
206 | 145, 146,
147, 204, 205 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πΌ + 1) β€ sup({π β (0..^π) β£ (πβπ) β€ (πβπ½)}, β, < )) |
207 | 206, 1 | breqtrrdi 5148 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β (πΌ + 1) β€ πΌ) |
208 | 140, 138,
207 | lensymd 11311 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (πβ(πΌ + 1)) β€ (πβπ½)) β Β¬ πΌ < (πΌ + 1)) |
209 | 208 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ (πβ(πΌ + 1)) β€ (πβπ½)) β Β¬ πΌ < (πΌ + 1)) |
210 | 137, 209 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (πβ(πΌ + 1)) β β) β§ Β¬ (πβπ½) < (πβ(πΌ + 1))) β Β¬ πΌ < (πΌ + 1)) |
211 | 133, 210 | condan 817 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (πβ(πΌ + 1)) β β) β (πβπ½) < (πβ(πΌ + 1))) |
212 | 81, 211 | mpdan 686 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ½) < (πβ(πΌ + 1))) |
213 | 21, 127, 81, 55, 212 | lelttrd 11318 |
. . . . . . . . . . . . 13
β’ (π β π΄ < (πβ(πΌ + 1))) |
214 | 213 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β π΄ < (πβ(πΌ + 1))) |
215 | 152 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(π½ + 1)) β β) |
216 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β π΅ β β) |
217 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) < (πβ(π½ + 1))) |
218 | 164 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(π½ + 1)) β€ π΅) |
219 | 126, 215,
216, 217, 218 | ltletrd 11320 |
. . . . . . . . . . . 12
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) < π΅) |
220 | 124, 125,
126, 214, 219 | eliood 43822 |
. . . . . . . . . . 11
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β (π΄(,)π΅)) |
221 | 123, 220 | elind 4155 |
. . . . . . . . . 10
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β (ran π β© (π΄(,)π΅))) |
222 | | elun2 4138 |
. . . . . . . . . 10
β’ ((πβ(πΌ + 1)) β (ran π β© (π΄(,)π΅)) β (πβ(πΌ + 1)) β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅)))) |
223 | 221, 222 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β ({π΄, π΅} βͺ (ran π β© (π΄(,)π΅)))) |
224 | 223, 22 | eleqtrrdi 2845 |
. . . . . . . 8
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (πβ(πΌ + 1)) β π) |
225 | | foelrn 7057 |
. . . . . . . 8
β’ ((π:(0...π)βontoβπ β§ (πβ(πΌ + 1)) β π) β βπ β (0...π)(πβ(πΌ + 1)) = (πβπ)) |
226 | 115, 224,
225 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β βπ β (0...π)(πβ(πΌ + 1)) = (πβπ)) |
227 | 212 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ½) < (πβ(πΌ + 1))) |
228 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πβ(πΌ + 1)) = (πβπ)) β (πβ(πΌ + 1)) = (πβπ)) |
229 | 227, 228 | breqtrd 5132 |
. . . . . . . . . . . . 13
β’ ((π β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ½) < (πβπ)) |
230 | 229 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ½) < (πβπ)) |
231 | 43 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β π Isom < , < ((0...π), π)) |
232 | 49 | anim1i 616 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0...π)) β (π½ β (0...π) β§ π β (0...π))) |
233 | 232 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (π½ β (0...π) β§ π β (0...π))) |
234 | | isorel 7272 |
. . . . . . . . . . . . 13
β’ ((π Isom < , < ((0...π), π) β§ (π½ β (0...π) β§ π β (0...π))) β (π½ < π β (πβπ½) < (πβπ))) |
235 | 231, 233,
234 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (π½ < π β (πβπ½) < (πβπ))) |
236 | 230, 235 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β π½ < π) |
237 | 236 | adantllr 718 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β π½ < π) |
238 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(πΌ + 1)) = (πβπ) β (πβπ) = (πβ(πΌ + 1))) |
239 | 238 | biimpi 215 |
. . . . . . . . . . . . . . 15
β’ ((πβ(πΌ + 1)) = (πβπ) β (πβπ) = (πβ(πΌ + 1))) |
240 | 239 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((πβ(πΌ + 1)) < (πβ(π½ + 1)) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ) = (πβ(πΌ + 1))) |
241 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ (((πβ(πΌ + 1)) < (πβ(π½ + 1)) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβ(πΌ + 1)) < (πβ(π½ + 1))) |
242 | 240, 241 | eqbrtrd 5128 |
. . . . . . . . . . . . 13
β’ (((πβ(πΌ + 1)) < (πβ(π½ + 1)) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ) < (πβ(π½ + 1))) |
243 | 242 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ) < (πβ(π½ + 1))) |
244 | 243 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (πβπ) < (πβ(π½ + 1))) |
245 | 43 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β π Isom < , < ((0...π), π)) |
246 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β π β (0...π)) |
247 | 105 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β (π½ + 1) β (0...π)) |
248 | | isorel 7272 |
. . . . . . . . . . . . 13
β’ ((π Isom < , < ((0...π), π) β§ (π β (0...π) β§ (π½ + 1) β (0...π))) β (π < (π½ + 1) β (πβπ) < (πβ(π½ + 1)))) |
249 | 245, 246,
247, 248 | syl12anc 836 |
. . . . . . . . . . . 12
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β (π < (π½ + 1) β (πβπ) < (πβ(π½ + 1)))) |
250 | 249 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (π < (π½ + 1) β (πβπ) < (πβ(π½ + 1)))) |
251 | 244, 250 | mpbird 257 |
. . . . . . . . . 10
β’ ((((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β π < (π½ + 1)) |
252 | 237, 251 | jca 513 |
. . . . . . . . 9
β’ ((((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β§ (πβ(πΌ + 1)) = (πβπ)) β (π½ < π β§ π < (π½ + 1))) |
253 | 252 | ex 414 |
. . . . . . . 8
β’ (((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β§ π β (0...π)) β ((πβ(πΌ + 1)) = (πβπ) β (π½ < π β§ π < (π½ + 1)))) |
254 | 253 | reximdva 3162 |
. . . . . . 7
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β (βπ β (0...π)(πβ(πΌ + 1)) = (πβπ) β βπ β (0...π)(π½ < π β§ π < (π½ + 1)))) |
255 | 226, 254 | mpd 15 |
. . . . . 6
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β βπ β (0...π)(π½ < π β§ π < (π½ + 1))) |
256 | | ssrexv 4012 |
. . . . . 6
β’
((0...π) β
β€ β (βπ
β (0...π)(π½ < π β§ π < (π½ + 1)) β βπ β β€ (π½ < π β§ π < (π½ + 1)))) |
257 | 112, 255,
256 | mpsyl 68 |
. . . . 5
β’ ((π β§ (πβ(πΌ + 1)) < (πβ(π½ + 1))) β βπ β β€ (π½ < π β§ π < (π½ + 1))) |
258 | 111, 257 | syldan 592 |
. . . 4
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β βπ β β€ (π½ < π β§ π < (π½ + 1))) |
259 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β β€) β§ (π½ < π β§ π < (π½ + 1))) β π β β€) |
260 | 47, 154 | syl 17 |
. . . . . . . . 9
β’ (π β π½ β β€) |
261 | 260 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ (π½ < π β§ π < (π½ + 1))) β π½ β β€) |
262 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ (π½ < π β§ π < (π½ + 1))) β π½ < π) |
263 | | simprr 772 |
. . . . . . . 8
β’ (((π β§ π β β€) β§ (π½ < π β§ π < (π½ + 1))) β π < (π½ + 1)) |
264 | | btwnnz 12584 |
. . . . . . . 8
β’ ((π½ β β€ β§ π½ < π β§ π < (π½ + 1)) β Β¬ π β β€) |
265 | 261, 262,
263, 264 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π β β€) β§ (π½ < π β§ π < (π½ + 1))) β Β¬ π β β€) |
266 | 259, 265 | pm2.65da 816 |
. . . . . 6
β’ ((π β§ π β β€) β Β¬ (π½ < π β§ π < (π½ + 1))) |
267 | 266 | nrexdv 3143 |
. . . . 5
β’ (π β Β¬ βπ β β€ (π½ < π β§ π < (π½ + 1))) |
268 | 267 | adantr 482 |
. . . 4
β’ ((π β§ Β¬ (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) β Β¬ βπ β β€ (π½ < π β§ π < (π½ + 1))) |
269 | 258, 268 | condan 817 |
. . 3
β’ (π β (πβ(π½ + 1)) β€ (πβ(πΌ + 1))) |
270 | | ioossioo 13364 |
. . 3
β’ ((((πβπΌ) β β* β§ (πβ(πΌ + 1)) β β*) β§
((πβπΌ) β€ (πβπ½) β§ (πβ(π½ + 1)) β€ (πβ(πΌ + 1)))) β ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπΌ)(,)(πβ(πΌ + 1)))) |
271 | 78, 82, 99, 269, 270 | syl22anc 838 |
. 2
β’ (π β ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπΌ)(,)(πβ(πΌ + 1)))) |
272 | | fveq2 6843 |
. . . . 5
β’ (π = πΌ β (πβπ) = (πβπΌ)) |
273 | | oveq1 7365 |
. . . . . 6
β’ (π = πΌ β (π + 1) = (πΌ + 1)) |
274 | 273 | fveq2d 6847 |
. . . . 5
β’ (π = πΌ β (πβ(π + 1)) = (πβ(πΌ + 1))) |
275 | 272, 274 | oveq12d 7376 |
. . . 4
β’ (π = πΌ β ((πβπ)(,)(πβ(π + 1))) = ((πβπΌ)(,)(πβ(πΌ + 1)))) |
276 | 275 | sseq2d 3977 |
. . 3
β’ (π = πΌ β (((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1))) β ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπΌ)(,)(πβ(πΌ + 1))))) |
277 | 276 | rspcev 3580 |
. 2
β’ ((πΌ β (0..^π) β§ ((πβπ½)(,)(πβ(π½ + 1))) β ((πβπΌ)(,)(πβ(πΌ + 1)))) β βπ β (0..^π)((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) |
278 | 75, 271, 277 | syl2anc 585 |
1
β’ (π β βπ β (0..^π)((πβπ½)(,)(πβ(π½ + 1))) β ((πβπ)(,)(πβ(π + 1)))) |