Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem63.t |
|- T = ( B - A ) |
2 |
|
fourierdlem63.p |
|- P = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
3 |
|
fourierdlem63.m |
|- ( ph -> M e. NN ) |
4 |
|
fourierdlem63.q |
|- ( ph -> Q e. ( P ` M ) ) |
5 |
|
fourierdlem63.c |
|- ( ph -> C e. RR ) |
6 |
|
fourierdlem63.d |
|- ( ph -> D e. RR ) |
7 |
|
fourierdlem63.cltd |
|- ( ph -> C < D ) |
8 |
|
fourierdlem63.o |
|- O = ( m e. NN |-> { p e. ( RR ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) |
9 |
|
fourierdlem63.h |
|- H = ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) |
10 |
|
fourierdlem63.n |
|- N = ( ( # ` H ) - 1 ) |
11 |
|
fourierdlem63.s |
|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) ) |
12 |
|
fourierdlem63.e |
|- E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) |
13 |
|
fourierdlem63.k |
|- ( ph -> K e. ( 0 ... M ) ) |
14 |
|
fourierdlem63.j |
|- ( ph -> J e. ( 0 ..^ N ) ) |
15 |
|
fourierdlem63.y |
|- ( ph -> Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) ) |
16 |
|
fourierdlem63.eyltqk |
|- ( ph -> ( E ` Y ) < ( Q ` K ) ) |
17 |
|
fourierdlem63.x |
|- X = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) |
18 |
12
|
a1i |
|- ( ph -> E = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) ) ) |
19 |
|
id |
|- ( x = ( S ` ( J + 1 ) ) -> x = ( S ` ( J + 1 ) ) ) |
20 |
|
oveq2 |
|- ( x = ( S ` ( J + 1 ) ) -> ( B - x ) = ( B - ( S ` ( J + 1 ) ) ) ) |
21 |
20
|
oveq1d |
|- ( x = ( S ` ( J + 1 ) ) -> ( ( B - x ) / T ) = ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) |
22 |
21
|
fveq2d |
|- ( x = ( S ` ( J + 1 ) ) -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) ) |
23 |
22
|
oveq1d |
|- ( x = ( S ` ( J + 1 ) ) -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) |
24 |
19 23
|
oveq12d |
|- ( x = ( S ` ( J + 1 ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) ) |
25 |
24
|
adantl |
|- ( ( ph /\ x = ( S ` ( J + 1 ) ) ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) ) |
26 |
1 2 3 4 5 6 7 8 9 10 11
|
fourierdlem54 |
|- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , H ) ) ) |
27 |
26
|
simpld |
|- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) ) |
28 |
27
|
simprd |
|- ( ph -> S e. ( O ` N ) ) |
29 |
27
|
simpld |
|- ( ph -> N e. NN ) |
30 |
8
|
fourierdlem2 |
|- ( N e. NN -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) ) |
31 |
29 30
|
syl |
|- ( ph -> ( S e. ( O ` N ) <-> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) ) |
32 |
28 31
|
mpbid |
|- ( ph -> ( S e. ( RR ^m ( 0 ... N ) ) /\ ( ( ( S ` 0 ) = C /\ ( S ` N ) = D ) /\ A. i e. ( 0 ..^ N ) ( S ` i ) < ( S ` ( i + 1 ) ) ) ) ) |
33 |
32
|
simpld |
|- ( ph -> S e. ( RR ^m ( 0 ... N ) ) ) |
34 |
|
elmapi |
|- ( S e. ( RR ^m ( 0 ... N ) ) -> S : ( 0 ... N ) --> RR ) |
35 |
33 34
|
syl |
|- ( ph -> S : ( 0 ... N ) --> RR ) |
36 |
|
fzofzp1 |
|- ( J e. ( 0 ..^ N ) -> ( J + 1 ) e. ( 0 ... N ) ) |
37 |
14 36
|
syl |
|- ( ph -> ( J + 1 ) e. ( 0 ... N ) ) |
38 |
35 37
|
ffvelrnd |
|- ( ph -> ( S ` ( J + 1 ) ) e. RR ) |
39 |
2 3 4
|
fourierdlem11 |
|- ( ph -> ( A e. RR /\ B e. RR /\ A < B ) ) |
40 |
39
|
simp2d |
|- ( ph -> B e. RR ) |
41 |
40 38
|
resubcld |
|- ( ph -> ( B - ( S ` ( J + 1 ) ) ) e. RR ) |
42 |
39
|
simp1d |
|- ( ph -> A e. RR ) |
43 |
40 42
|
resubcld |
|- ( ph -> ( B - A ) e. RR ) |
44 |
1 43
|
eqeltrid |
|- ( ph -> T e. RR ) |
45 |
39
|
simp3d |
|- ( ph -> A < B ) |
46 |
42 40
|
posdifd |
|- ( ph -> ( A < B <-> 0 < ( B - A ) ) ) |
47 |
45 46
|
mpbid |
|- ( ph -> 0 < ( B - A ) ) |
48 |
47 1
|
breqtrrdi |
|- ( ph -> 0 < T ) |
49 |
48
|
gt0ne0d |
|- ( ph -> T =/= 0 ) |
50 |
41 44 49
|
redivcld |
|- ( ph -> ( ( B - ( S ` ( J + 1 ) ) ) / T ) e. RR ) |
51 |
50
|
flcld |
|- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. ZZ ) |
52 |
51
|
zred |
|- ( ph -> ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) e. RR ) |
53 |
52 44
|
remulcld |
|- ( ph -> ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) e. RR ) |
54 |
38 53
|
readdcld |
|- ( ph -> ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) e. RR ) |
55 |
18 25 38 54
|
fvmptd |
|- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( |_ ` ( ( B - ( S ` ( J + 1 ) ) ) / T ) ) x. T ) ) ) |
56 |
55 54
|
eqeltrd |
|- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. RR ) |
57 |
2
|
fourierdlem2 |
|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
58 |
3 57
|
syl |
|- ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) ) |
59 |
4 58
|
mpbid |
|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) |
60 |
59
|
simpld |
|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) ) |
61 |
|
elmapi |
|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR ) |
62 |
60 61
|
syl |
|- ( ph -> Q : ( 0 ... M ) --> RR ) |
63 |
62 13
|
ffvelrnd |
|- ( ph -> ( Q ` K ) e. RR ) |
64 |
5
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C e. RR ) |
65 |
6
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> D e. RR ) |
66 |
42
|
rexrd |
|- ( ph -> A e. RR* ) |
67 |
|
iocssre |
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR ) |
68 |
66 40 67
|
syl2anc |
|- ( ph -> ( A (,] B ) C_ RR ) |
69 |
42 40 45 1 12
|
fourierdlem4 |
|- ( ph -> E : RR --> ( A (,] B ) ) |
70 |
|
elfzofz |
|- ( J e. ( 0 ..^ N ) -> J e. ( 0 ... N ) ) |
71 |
14 70
|
syl |
|- ( ph -> J e. ( 0 ... N ) ) |
72 |
35 71
|
ffvelrnd |
|- ( ph -> ( S ` J ) e. RR ) |
73 |
38
|
rexrd |
|- ( ph -> ( S ` ( J + 1 ) ) e. RR* ) |
74 |
|
elico2 |
|- ( ( ( S ` J ) e. RR /\ ( S ` ( J + 1 ) ) e. RR* ) -> ( Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) <-> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) ) |
75 |
72 73 74
|
syl2anc |
|- ( ph -> ( Y e. ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) <-> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) ) |
76 |
15 75
|
mpbid |
|- ( ph -> ( Y e. RR /\ ( S ` J ) <_ Y /\ Y < ( S ` ( J + 1 ) ) ) ) |
77 |
76
|
simp1d |
|- ( ph -> Y e. RR ) |
78 |
69 77
|
ffvelrnd |
|- ( ph -> ( E ` Y ) e. ( A (,] B ) ) |
79 |
68 78
|
sseldd |
|- ( ph -> ( E ` Y ) e. RR ) |
80 |
79 77
|
resubcld |
|- ( ph -> ( ( E ` Y ) - Y ) e. RR ) |
81 |
63 80
|
resubcld |
|- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR ) |
82 |
81
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. RR ) |
83 |
|
icossicc |
|- ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( ( S ` J ) [,] ( S ` ( J + 1 ) ) ) |
84 |
5
|
rexrd |
|- ( ph -> C e. RR* ) |
85 |
6
|
rexrd |
|- ( ph -> D e. RR* ) |
86 |
8 29 28
|
fourierdlem15 |
|- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) ) |
87 |
84 85 86 14
|
fourierdlem8 |
|- ( ph -> ( ( S ` J ) [,] ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) ) |
88 |
83 87
|
sstrid |
|- ( ph -> ( ( S ` J ) [,) ( S ` ( J + 1 ) ) ) C_ ( C [,] D ) ) |
89 |
88 15
|
sseldd |
|- ( ph -> Y e. ( C [,] D ) ) |
90 |
|
elicc2 |
|- ( ( C e. RR /\ D e. RR ) -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) ) |
91 |
5 6 90
|
syl2anc |
|- ( ph -> ( Y e. ( C [,] D ) <-> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) ) |
92 |
89 91
|
mpbid |
|- ( ph -> ( Y e. RR /\ C <_ Y /\ Y <_ D ) ) |
93 |
92
|
simp2d |
|- ( ph -> C <_ Y ) |
94 |
63 79
|
resubcld |
|- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR ) |
95 |
79 63
|
posdifd |
|- ( ph -> ( ( E ` Y ) < ( Q ` K ) <-> 0 < ( ( Q ` K ) - ( E ` Y ) ) ) ) |
96 |
16 95
|
mpbid |
|- ( ph -> 0 < ( ( Q ` K ) - ( E ` Y ) ) ) |
97 |
94 96
|
elrpd |
|- ( ph -> ( ( Q ` K ) - ( E ` Y ) ) e. RR+ ) |
98 |
77 97
|
ltaddrpd |
|- ( ph -> Y < ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) ) |
99 |
63
|
recnd |
|- ( ph -> ( Q ` K ) e. CC ) |
100 |
79
|
recnd |
|- ( ph -> ( E ` Y ) e. CC ) |
101 |
77
|
recnd |
|- ( ph -> Y e. CC ) |
102 |
99 100 101
|
subsub3d |
|- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) = ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) ) |
103 |
99 101
|
addcomd |
|- ( ph -> ( ( Q ` K ) + Y ) = ( Y + ( Q ` K ) ) ) |
104 |
103
|
oveq1d |
|- ( ph -> ( ( ( Q ` K ) + Y ) - ( E ` Y ) ) = ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) ) |
105 |
101 99 100
|
addsubassd |
|- ( ph -> ( ( Y + ( Q ` K ) ) - ( E ` Y ) ) = ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) ) |
106 |
102 104 105
|
3eqtrrd |
|- ( ph -> ( Y + ( ( Q ` K ) - ( E ` Y ) ) ) = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) ) |
107 |
98 106
|
breqtrd |
|- ( ph -> Y < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) ) |
108 |
5 77 81 93 107
|
lelttrd |
|- ( ph -> C < ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) ) |
109 |
5 81 108
|
ltled |
|- ( ph -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) ) |
110 |
109
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> C <_ ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) ) |
111 |
38
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. RR ) |
112 |
63
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. RR ) |
113 |
56 38
|
resubcld |
|- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR ) |
114 |
113
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) e. RR ) |
115 |
112 114
|
resubcld |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) e. RR ) |
116 |
76
|
simp3d |
|- ( ph -> Y < ( S ` ( J + 1 ) ) ) |
117 |
77 38 116
|
ltled |
|- ( ph -> Y <_ ( S ` ( J + 1 ) ) ) |
118 |
42 40 45 1 12 77 38 117
|
fourierdlem7 |
|- ( ph -> ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) <_ ( ( E ` Y ) - Y ) ) |
119 |
113 80 63 118
|
lesub2dd |
|- ( ph -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) ) |
120 |
119
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) ) |
121 |
99
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) e. CC ) |
122 |
56
|
recnd |
|- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) e. CC ) |
123 |
122
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. CC ) |
124 |
111
|
recnd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) e. CC ) |
125 |
121 123 124
|
subsubd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) = ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) ) |
126 |
99 122
|
subcld |
|- ( ph -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. CC ) |
127 |
38
|
recnd |
|- ( ph -> ( S ` ( J + 1 ) ) e. CC ) |
128 |
126 127
|
addcomd |
|- ( ph -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) ) |
129 |
128
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) + ( S ` ( J + 1 ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) ) |
130 |
125 129
|
eqtrd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) = ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) ) |
131 |
|
simpr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) |
132 |
56
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( E ` ( S ` ( J + 1 ) ) ) e. RR ) |
133 |
112 132
|
sublt0d |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) ) |
134 |
131 133
|
mpbird |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 ) |
135 |
112 132
|
resubcld |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR ) |
136 |
|
ltaddneg |
|- ( ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) e. RR /\ ( S ` ( J + 1 ) ) e. RR ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) ) ) |
137 |
135 111 136
|
syl2anc |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) < 0 <-> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) ) ) |
138 |
134 137
|
mpbid |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( S ` ( J + 1 ) ) + ( ( Q ` K ) - ( E ` ( S ` ( J + 1 ) ) ) ) ) < ( S ` ( J + 1 ) ) ) |
139 |
130 138
|
eqbrtrd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` ( S ` ( J + 1 ) ) ) - ( S ` ( J + 1 ) ) ) ) < ( S ` ( J + 1 ) ) ) |
140 |
82 115 111 120 139
|
lelttrd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < ( S ` ( J + 1 ) ) ) |
141 |
86 37
|
ffvelrnd |
|- ( ph -> ( S ` ( J + 1 ) ) e. ( C [,] D ) ) |
142 |
|
elicc2 |
|- ( ( C e. RR /\ D e. RR ) -> ( ( S ` ( J + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) ) |
143 |
5 6 142
|
syl2anc |
|- ( ph -> ( ( S ` ( J + 1 ) ) e. ( C [,] D ) <-> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) ) |
144 |
141 143
|
mpbid |
|- ( ph -> ( ( S ` ( J + 1 ) ) e. RR /\ C <_ ( S ` ( J + 1 ) ) /\ ( S ` ( J + 1 ) ) <_ D ) ) |
145 |
144
|
simp3d |
|- ( ph -> ( S ` ( J + 1 ) ) <_ D ) |
146 |
145
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( S ` ( J + 1 ) ) <_ D ) |
147 |
82 111 65 140 146
|
ltletrd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) < D ) |
148 |
82 65 147
|
ltled |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) <_ D ) |
149 |
64 65 82 110 148
|
eliccd |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) ) |
150 |
|
id |
|- ( x = Y -> x = Y ) |
151 |
|
oveq2 |
|- ( x = Y -> ( B - x ) = ( B - Y ) ) |
152 |
151
|
oveq1d |
|- ( x = Y -> ( ( B - x ) / T ) = ( ( B - Y ) / T ) ) |
153 |
152
|
fveq2d |
|- ( x = Y -> ( |_ ` ( ( B - x ) / T ) ) = ( |_ ` ( ( B - Y ) / T ) ) ) |
154 |
153
|
oveq1d |
|- ( x = Y -> ( ( |_ ` ( ( B - x ) / T ) ) x. T ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) |
155 |
150 154
|
oveq12d |
|- ( x = Y -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) ) |
156 |
155
|
adantl |
|- ( ( ph /\ x = Y ) -> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) ) |
157 |
40 77
|
resubcld |
|- ( ph -> ( B - Y ) e. RR ) |
158 |
157 44 49
|
redivcld |
|- ( ph -> ( ( B - Y ) / T ) e. RR ) |
159 |
158
|
flcld |
|- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. ZZ ) |
160 |
159
|
zred |
|- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. RR ) |
161 |
160 44
|
remulcld |
|- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. RR ) |
162 |
77 161
|
readdcld |
|- ( ph -> ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) e. RR ) |
163 |
18 156 77 162
|
fvmptd |
|- ( ph -> ( E ` Y ) = ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) ) |
164 |
163
|
oveq1d |
|- ( ph -> ( ( E ` Y ) - Y ) = ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) ) |
165 |
164
|
oveq1d |
|- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) ) |
166 |
161
|
recnd |
|- ( ph -> ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) e. CC ) |
167 |
101 166
|
pncan2d |
|- ( ph -> ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) = ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) |
168 |
167
|
oveq1d |
|- ( ph -> ( ( ( Y + ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) ) - Y ) / T ) = ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) ) |
169 |
160
|
recnd |
|- ( ph -> ( |_ ` ( ( B - Y ) / T ) ) e. CC ) |
170 |
44
|
recnd |
|- ( ph -> T e. CC ) |
171 |
169 170 49
|
divcan4d |
|- ( ph -> ( ( ( |_ ` ( ( B - Y ) / T ) ) x. T ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) ) |
172 |
165 168 171
|
3eqtrd |
|- ( ph -> ( ( ( E ` Y ) - Y ) / T ) = ( |_ ` ( ( B - Y ) / T ) ) ) |
173 |
172 159
|
eqeltrd |
|- ( ph -> ( ( ( E ` Y ) - Y ) / T ) e. ZZ ) |
174 |
80
|
recnd |
|- ( ph -> ( ( E ` Y ) - Y ) e. CC ) |
175 |
174 170 49
|
divcan1d |
|- ( ph -> ( ( ( ( E ` Y ) - Y ) / T ) x. T ) = ( ( E ` Y ) - Y ) ) |
176 |
175
|
oveq2d |
|- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) ) |
177 |
99 174
|
npcand |
|- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( E ` Y ) - Y ) ) = ( Q ` K ) ) |
178 |
176 177
|
eqtrd |
|- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) = ( Q ` K ) ) |
179 |
|
ffun |
|- ( Q : ( 0 ... M ) --> RR -> Fun Q ) |
180 |
62 179
|
syl |
|- ( ph -> Fun Q ) |
181 |
62
|
fdmd |
|- ( ph -> dom Q = ( 0 ... M ) ) |
182 |
13 181
|
eleqtrrd |
|- ( ph -> K e. dom Q ) |
183 |
|
fvelrn |
|- ( ( Fun Q /\ K e. dom Q ) -> ( Q ` K ) e. ran Q ) |
184 |
180 182 183
|
syl2anc |
|- ( ph -> ( Q ` K ) e. ran Q ) |
185 |
178 184
|
eqeltrd |
|- ( ph -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q ) |
186 |
|
oveq1 |
|- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( k x. T ) = ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) |
187 |
186
|
oveq2d |
|- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) ) |
188 |
187
|
eleq1d |
|- ( k = ( ( ( E ` Y ) - Y ) / T ) -> ( ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q ) ) |
189 |
188
|
rspcev |
|- ( ( ( ( ( E ` Y ) - Y ) / T ) e. ZZ /\ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( ( ( ( E ` Y ) - Y ) / T ) x. T ) ) e. ran Q ) -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) |
190 |
173 185 189
|
syl2anc |
|- ( ph -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) |
191 |
190
|
adantr |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) |
192 |
|
oveq1 |
|- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( x + ( k x. T ) ) = ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) ) |
193 |
192
|
eleq1d |
|- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( ( x + ( k x. T ) ) e. ran Q <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) ) |
194 |
193
|
rexbidv |
|- ( x = ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) -> ( E. k e. ZZ ( x + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) ) |
195 |
194
|
elrab |
|- ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } <-> ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( C [,] D ) /\ E. k e. ZZ ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) + ( k x. T ) ) e. ran Q ) ) |
196 |
149 191 195
|
sylanbrc |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) |
197 |
|
elun2 |
|- ( ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
198 |
196 197
|
syl |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> ( ( Q ` K ) - ( ( E ` Y ) - Y ) ) e. ( { C , D } u. { x e. ( C [,] D ) | E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } ) ) |
199 |
198 17 9
|
3eltr4g |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X e. H ) |
200 |
|
elfzelz |
|- ( j e. ( 0 ... N ) -> j e. ZZ ) |
201 |
200
|
ad2antlr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j e. ZZ ) |
202 |
|
elfzoelz |
|- ( J e. ( 0 ..^ N ) -> J e. ZZ ) |
203 |
14 202
|
syl |
|- ( ph -> J e. ZZ ) |
204 |
203
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J e. ZZ ) |
205 |
|
simpr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( S ` J ) < ( S ` j ) ) |
206 |
26
|
simprd |
|- ( ph -> S Isom < , < ( ( 0 ... N ) , H ) ) |
207 |
206
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> S Isom < , < ( ( 0 ... N ) , H ) ) |
208 |
71
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J e. ( 0 ... N ) ) |
209 |
|
simplr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> j e. ( 0 ... N ) ) |
210 |
|
isorel |
|- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( J e. ( 0 ... N ) /\ j e. ( 0 ... N ) ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) ) |
211 |
207 208 209 210
|
syl12anc |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> ( J < j <-> ( S ` J ) < ( S ` j ) ) ) |
212 |
205 211
|
mpbird |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` J ) < ( S ` j ) ) -> J < j ) |
213 |
212
|
adantrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> J < j ) |
214 |
|
simpr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( S ` j ) < ( S ` ( J + 1 ) ) ) |
215 |
206
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> S Isom < , < ( ( 0 ... N ) , H ) ) |
216 |
|
simplr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j e. ( 0 ... N ) ) |
217 |
37
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( J + 1 ) e. ( 0 ... N ) ) |
218 |
|
isorel |
|- ( ( S Isom < , < ( ( 0 ... N ) , H ) /\ ( j e. ( 0 ... N ) /\ ( J + 1 ) e. ( 0 ... N ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) ) |
219 |
215 216 217 218
|
syl12anc |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> ( j < ( J + 1 ) <-> ( S ` j ) < ( S ` ( J + 1 ) ) ) ) |
220 |
214 219
|
mpbird |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) -> j < ( J + 1 ) ) |
221 |
220
|
adantrl |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> j < ( J + 1 ) ) |
222 |
|
btwnnz |
|- ( ( J e. ZZ /\ J < j /\ j < ( J + 1 ) ) -> -. j e. ZZ ) |
223 |
204 213 221 222
|
syl3anc |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) -> -. j e. ZZ ) |
224 |
201 223
|
pm2.65da |
|- ( ( ph /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) |
225 |
224
|
adantlr |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) |
226 |
72
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) e. RR ) |
227 |
77
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y e. RR ) |
228 |
35
|
ffvelrnda |
|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( S ` j ) e. RR ) |
229 |
228
|
adantr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) e. RR ) |
230 |
76
|
simp2d |
|- ( ph -> ( S ` J ) <_ Y ) |
231 |
230
|
ad2antrr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) <_ Y ) |
232 |
107 17
|
breqtrrdi |
|- ( ph -> Y < X ) |
233 |
232
|
adantr |
|- ( ( ph /\ ( S ` j ) = X ) -> Y < X ) |
234 |
|
eqcom |
|- ( X = ( S ` j ) <-> ( S ` j ) = X ) |
235 |
234
|
biimpri |
|- ( ( S ` j ) = X -> X = ( S ` j ) ) |
236 |
235
|
adantl |
|- ( ( ph /\ ( S ` j ) = X ) -> X = ( S ` j ) ) |
237 |
233 236
|
breqtrd |
|- ( ( ph /\ ( S ` j ) = X ) -> Y < ( S ` j ) ) |
238 |
237
|
adantlr |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> Y < ( S ` j ) ) |
239 |
226 227 229 231 238
|
lelttrd |
|- ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) ) |
240 |
239
|
adantllr |
|- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` J ) < ( S ` j ) ) |
241 |
|
simpr |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) = X ) |
242 |
17 140
|
eqbrtrid |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> X < ( S ` ( J + 1 ) ) ) |
243 |
242
|
adantr |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> X < ( S ` ( J + 1 ) ) ) |
244 |
241 243
|
eqbrtrd |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) ) |
245 |
244
|
adantlr |
|- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( S ` j ) < ( S ` ( J + 1 ) ) ) |
246 |
240 245
|
jca |
|- ( ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) /\ ( S ` j ) = X ) -> ( ( S ` J ) < ( S ` j ) /\ ( S ` j ) < ( S ` ( J + 1 ) ) ) ) |
247 |
225 246
|
mtand |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ j e. ( 0 ... N ) ) -> -. ( S ` j ) = X ) |
248 |
247
|
nrexdv |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. E. j e. ( 0 ... N ) ( S ` j ) = X ) |
249 |
|
isof1o |
|- ( S Isom < , < ( ( 0 ... N ) , H ) -> S : ( 0 ... N ) -1-1-onto-> H ) |
250 |
206 249
|
syl |
|- ( ph -> S : ( 0 ... N ) -1-1-onto-> H ) |
251 |
|
f1ofo |
|- ( S : ( 0 ... N ) -1-1-onto-> H -> S : ( 0 ... N ) -onto-> H ) |
252 |
250 251
|
syl |
|- ( ph -> S : ( 0 ... N ) -onto-> H ) |
253 |
|
foelrn |
|- ( ( S : ( 0 ... N ) -onto-> H /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) ) |
254 |
252 253
|
sylan |
|- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) X = ( S ` j ) ) |
255 |
234
|
rexbii |
|- ( E. j e. ( 0 ... N ) X = ( S ` j ) <-> E. j e. ( 0 ... N ) ( S ` j ) = X ) |
256 |
254 255
|
sylib |
|- ( ( ph /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X ) |
257 |
256
|
adantlr |
|- ( ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) /\ X e. H ) -> E. j e. ( 0 ... N ) ( S ` j ) = X ) |
258 |
248 257
|
mtand |
|- ( ( ph /\ ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) -> -. X e. H ) |
259 |
199 258
|
pm2.65da |
|- ( ph -> -. ( Q ` K ) < ( E ` ( S ` ( J + 1 ) ) ) ) |
260 |
56 63 259
|
nltled |
|- ( ph -> ( E ` ( S ` ( J + 1 ) ) ) <_ ( Q ` K ) ) |