Step |
Hyp |
Ref |
Expression |
1 |
|
fourierdlem12.1 |
|- 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 ) ) ) } ) |
2 |
|
fourierdlem12.2 |
|- ( ph -> M e. NN ) |
3 |
|
fourierdlem12.3 |
|- ( ph -> Q e. ( P ` M ) ) |
4 |
|
fourierdlem12.4 |
|- ( ph -> X e. ran Q ) |
5 |
1
|
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 ) ) ) ) ) ) |
6 |
2 5
|
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 ) ) ) ) ) ) |
7 |
3 6
|
mpbid |
|- ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) |
8 |
7
|
simpld |
|- ( ph -> Q e. ( RR ^m ( 0 ... M ) ) ) |
9 |
|
elmapi |
|- ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR ) |
10 |
|
ffn |
|- ( Q : ( 0 ... M ) --> RR -> Q Fn ( 0 ... M ) ) |
11 |
8 9 10
|
3syl |
|- ( ph -> Q Fn ( 0 ... M ) ) |
12 |
|
fvelrnb |
|- ( Q Fn ( 0 ... M ) -> ( X e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = X ) ) |
13 |
11 12
|
syl |
|- ( ph -> ( X e. ran Q <-> E. j e. ( 0 ... M ) ( Q ` j ) = X ) ) |
14 |
4 13
|
mpbid |
|- ( ph -> E. j e. ( 0 ... M ) ( Q ` j ) = X ) |
15 |
14
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> E. j e. ( 0 ... M ) ( Q ` j ) = X ) |
16 |
8 9
|
syl |
|- ( ph -> Q : ( 0 ... M ) --> RR ) |
17 |
16
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR ) |
18 |
|
fzofzp1 |
|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) ) |
19 |
18
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) ) |
20 |
17 19
|
ffvelrnd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR ) |
21 |
20
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ i < j ) -> ( Q ` ( i + 1 ) ) e. RR ) |
22 |
21
|
3ad2antl1 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) e. RR ) |
23 |
|
frn |
|- ( Q : ( 0 ... M ) --> RR -> ran Q C_ RR ) |
24 |
16 23
|
syl |
|- ( ph -> ran Q C_ RR ) |
25 |
24 4
|
sseldd |
|- ( ph -> X e. RR ) |
26 |
25
|
ad2antrr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ i < j ) -> X e. RR ) |
27 |
26
|
3ad2antl1 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> X e. RR ) |
28 |
17
|
ffvelrnda |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR ) |
29 |
28
|
3adant3 |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) e. RR ) |
30 |
29
|
adantr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` j ) e. RR ) |
31 |
|
simpr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i < j ) |
32 |
|
elfzoelz |
|- ( i e. ( 0 ..^ M ) -> i e. ZZ ) |
33 |
32
|
ad2antrr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> i e. ZZ ) |
34 |
|
elfzelz |
|- ( j e. ( 0 ... M ) -> j e. ZZ ) |
35 |
34
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ZZ ) |
36 |
|
zltp1le |
|- ( ( i e. ZZ /\ j e. ZZ ) -> ( i < j <-> ( i + 1 ) <_ j ) ) |
37 |
33 35 36
|
syl2anc |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i < j <-> ( i + 1 ) <_ j ) ) |
38 |
31 37
|
mpbid |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i + 1 ) <_ j ) |
39 |
33
|
peano2zd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( i + 1 ) e. ZZ ) |
40 |
|
eluz |
|- ( ( ( i + 1 ) e. ZZ /\ j e. ZZ ) -> ( j e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ j ) ) |
41 |
39 35 40
|
syl2anc |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( j e. ( ZZ>= ` ( i + 1 ) ) <-> ( i + 1 ) <_ j ) ) |
42 |
38 41
|
mpbird |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ( ZZ>= ` ( i + 1 ) ) ) |
43 |
42
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> j e. ( ZZ>= ` ( i + 1 ) ) ) |
44 |
17
|
ad2antrr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> Q : ( 0 ... M ) --> RR ) |
45 |
|
0zd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 e. ZZ ) |
46 |
|
elfzel2 |
|- ( j e. ( 0 ... M ) -> M e. ZZ ) |
47 |
46
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> M e. ZZ ) |
48 |
|
elfzelz |
|- ( w e. ( ( i + 1 ) ... j ) -> w e. ZZ ) |
49 |
48
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ZZ ) |
50 |
|
0red |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 e. RR ) |
51 |
48
|
zred |
|- ( w e. ( ( i + 1 ) ... j ) -> w e. RR ) |
52 |
51
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. RR ) |
53 |
32
|
peano2zd |
|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ZZ ) |
54 |
53
|
zred |
|- ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. RR ) |
55 |
54
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( i + 1 ) e. RR ) |
56 |
32
|
zred |
|- ( i e. ( 0 ..^ M ) -> i e. RR ) |
57 |
56
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> i e. RR ) |
58 |
|
elfzole1 |
|- ( i e. ( 0 ..^ M ) -> 0 <_ i ) |
59 |
58
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ i ) |
60 |
57
|
ltp1d |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> i < ( i + 1 ) ) |
61 |
50 57 55 59 60
|
lelttrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 < ( i + 1 ) ) |
62 |
|
elfzle1 |
|- ( w e. ( ( i + 1 ) ... j ) -> ( i + 1 ) <_ w ) |
63 |
62
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( i + 1 ) <_ w ) |
64 |
50 55 52 61 63
|
ltletrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 < w ) |
65 |
50 52 64
|
ltled |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ w ) |
66 |
65
|
adantlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> 0 <_ w ) |
67 |
51
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. RR ) |
68 |
34
|
zred |
|- ( j e. ( 0 ... M ) -> j e. RR ) |
69 |
68
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> j e. RR ) |
70 |
46
|
zred |
|- ( j e. ( 0 ... M ) -> M e. RR ) |
71 |
70
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> M e. RR ) |
72 |
|
elfzle2 |
|- ( w e. ( ( i + 1 ) ... j ) -> w <_ j ) |
73 |
72
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ j ) |
74 |
|
elfzle2 |
|- ( j e. ( 0 ... M ) -> j <_ M ) |
75 |
74
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> j <_ M ) |
76 |
67 69 71 73 75
|
letrd |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ M ) |
77 |
76
|
adantll |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w <_ M ) |
78 |
45 47 49 66 77
|
elfzd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ( 0 ... M ) ) |
79 |
78
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> w e. ( 0 ... M ) ) |
80 |
44 79
|
ffvelrnd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( Q ` w ) e. RR ) |
81 |
80
|
adantlr |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... j ) ) -> ( Q ` w ) e. RR ) |
82 |
|
simp-4l |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ph ) |
83 |
|
0red |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. RR ) |
84 |
|
elfzelz |
|- ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w e. ZZ ) |
85 |
84
|
zred |
|- ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w e. RR ) |
86 |
85
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR ) |
87 |
|
0red |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. RR ) |
88 |
54
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( i + 1 ) e. RR ) |
89 |
85
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR ) |
90 |
|
0red |
|- ( i e. ( 0 ..^ M ) -> 0 e. RR ) |
91 |
56
|
ltp1d |
|- ( i e. ( 0 ..^ M ) -> i < ( i + 1 ) ) |
92 |
90 56 54 58 91
|
lelttrd |
|- ( i e. ( 0 ..^ M ) -> 0 < ( i + 1 ) ) |
93 |
92
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < ( i + 1 ) ) |
94 |
|
elfzle1 |
|- ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> ( i + 1 ) <_ w ) |
95 |
94
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( i + 1 ) <_ w ) |
96 |
87 88 89 93 95
|
ltletrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < w ) |
97 |
96
|
adantlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 < w ) |
98 |
83 86 97
|
ltled |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w ) |
99 |
98
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w ) |
100 |
99
|
adantlr |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 <_ w ) |
101 |
85
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. RR ) |
102 |
|
peano2rem |
|- ( j e. RR -> ( j - 1 ) e. RR ) |
103 |
68 102
|
syl |
|- ( j e. ( 0 ... M ) -> ( j - 1 ) e. RR ) |
104 |
103
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( j - 1 ) e. RR ) |
105 |
70
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> M e. RR ) |
106 |
|
elfzle2 |
|- ( w e. ( ( i + 1 ) ... ( j - 1 ) ) -> w <_ ( j - 1 ) ) |
107 |
106
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w <_ ( j - 1 ) ) |
108 |
|
zlem1lt |
|- ( ( j e. ZZ /\ M e. ZZ ) -> ( j <_ M <-> ( j - 1 ) < M ) ) |
109 |
34 46 108
|
syl2anc |
|- ( j e. ( 0 ... M ) -> ( j <_ M <-> ( j - 1 ) < M ) ) |
110 |
74 109
|
mpbid |
|- ( j e. ( 0 ... M ) -> ( j - 1 ) < M ) |
111 |
110
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( j - 1 ) < M ) |
112 |
101 104 105 107 111
|
lelttrd |
|- ( ( j e. ( 0 ... M ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M ) |
113 |
112
|
adantlr |
|- ( ( ( j e. ( 0 ... M ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M ) |
114 |
113
|
adantlll |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w < M ) |
115 |
84
|
adantl |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. ZZ ) |
116 |
|
0zd |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> 0 e. ZZ ) |
117 |
46
|
ad3antlr |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> M e. ZZ ) |
118 |
|
elfzo |
|- ( ( w e. ZZ /\ 0 e. ZZ /\ M e. ZZ ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) ) |
119 |
115 116 117 118
|
syl3anc |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) ) |
120 |
100 114 119
|
mpbir2and |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> w e. ( 0 ..^ M ) ) |
121 |
16
|
adantr |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR ) |
122 |
|
elfzofz |
|- ( w e. ( 0 ..^ M ) -> w e. ( 0 ... M ) ) |
123 |
122
|
adantl |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> w e. ( 0 ... M ) ) |
124 |
121 123
|
ffvelrnd |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) e. RR ) |
125 |
|
fzofzp1 |
|- ( w e. ( 0 ..^ M ) -> ( w + 1 ) e. ( 0 ... M ) ) |
126 |
125
|
adantl |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( w + 1 ) e. ( 0 ... M ) ) |
127 |
121 126
|
ffvelrnd |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` ( w + 1 ) ) e. RR ) |
128 |
|
eleq1w |
|- ( i = w -> ( i e. ( 0 ..^ M ) <-> w e. ( 0 ..^ M ) ) ) |
129 |
128
|
anbi2d |
|- ( i = w -> ( ( ph /\ i e. ( 0 ..^ M ) ) <-> ( ph /\ w e. ( 0 ..^ M ) ) ) ) |
130 |
|
fveq2 |
|- ( i = w -> ( Q ` i ) = ( Q ` w ) ) |
131 |
|
oveq1 |
|- ( i = w -> ( i + 1 ) = ( w + 1 ) ) |
132 |
131
|
fveq2d |
|- ( i = w -> ( Q ` ( i + 1 ) ) = ( Q ` ( w + 1 ) ) ) |
133 |
130 132
|
breq12d |
|- ( i = w -> ( ( Q ` i ) < ( Q ` ( i + 1 ) ) <-> ( Q ` w ) < ( Q ` ( w + 1 ) ) ) ) |
134 |
129 133
|
imbi12d |
|- ( i = w -> ( ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) <-> ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) < ( Q ` ( w + 1 ) ) ) ) ) |
135 |
7
|
simprrd |
|- ( ph -> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) |
136 |
135
|
r19.21bi |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) < ( Q ` ( i + 1 ) ) ) |
137 |
134 136
|
chvarvv |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) < ( Q ` ( w + 1 ) ) ) |
138 |
124 127 137
|
ltled |
|- ( ( ph /\ w e. ( 0 ..^ M ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) ) |
139 |
82 120 138
|
syl2anc |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) /\ w e. ( ( i + 1 ) ... ( j - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) ) |
140 |
43 81 139
|
monoord |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` j ) ) |
141 |
140
|
3adantl3 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ ( Q ` j ) ) |
142 |
16
|
ffvelrnda |
|- ( ( ph /\ j e. ( 0 ... M ) ) -> ( Q ` j ) e. RR ) |
143 |
142
|
3adant3 |
|- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) e. RR ) |
144 |
|
simp3 |
|- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) = X ) |
145 |
143 144
|
eqled |
|- ( ( ph /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) <_ X ) |
146 |
145
|
3adant1r |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> ( Q ` j ) <_ X ) |
147 |
146
|
adantr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` j ) <_ X ) |
148 |
22 30 27 141 147
|
letrd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> ( Q ` ( i + 1 ) ) <_ X ) |
149 |
22 27 148
|
lensymd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> -. X < ( Q ` ( i + 1 ) ) ) |
150 |
149
|
intnand |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ i < j ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) |
151 |
68
|
ad2antlr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> j e. RR ) |
152 |
56
|
ad3antlr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> i e. RR ) |
153 |
|
simpr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> -. i < j ) |
154 |
151 152 153
|
nltled |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ -. i < j ) -> j <_ i ) |
155 |
154
|
3adantl3 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> j <_ i ) |
156 |
|
eqcom |
|- ( ( Q ` j ) = X <-> X = ( Q ` j ) ) |
157 |
156
|
biimpi |
|- ( ( Q ` j ) = X -> X = ( Q ` j ) ) |
158 |
157
|
adantr |
|- ( ( ( Q ` j ) = X /\ j <_ i ) -> X = ( Q ` j ) ) |
159 |
158
|
3ad2antl3 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> X = ( Q ` j ) ) |
160 |
34
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> j e. ZZ ) |
161 |
32
|
ad2antrr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ZZ ) |
162 |
|
simpr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> j <_ i ) |
163 |
|
eluz2 |
|- ( i e. ( ZZ>= ` j ) <-> ( j e. ZZ /\ i e. ZZ /\ j <_ i ) ) |
164 |
160 161 162 163
|
syl3anbrc |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ( ZZ>= ` j ) ) |
165 |
164
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> i e. ( ZZ>= ` j ) ) |
166 |
17
|
ad2antrr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> Q : ( 0 ... M ) --> RR ) |
167 |
|
0zd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> 0 e. ZZ ) |
168 |
46
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> M e. ZZ ) |
169 |
|
elfzelz |
|- ( w e. ( j ... i ) -> w e. ZZ ) |
170 |
169
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w e. ZZ ) |
171 |
167 168 170
|
3jca |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) ) |
172 |
|
0red |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 e. RR ) |
173 |
68
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> j e. RR ) |
174 |
169
|
zred |
|- ( w e. ( j ... i ) -> w e. RR ) |
175 |
174
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> w e. RR ) |
176 |
|
elfzle1 |
|- ( j e. ( 0 ... M ) -> 0 <_ j ) |
177 |
176
|
adantr |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 <_ j ) |
178 |
|
elfzle1 |
|- ( w e. ( j ... i ) -> j <_ w ) |
179 |
178
|
adantl |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> j <_ w ) |
180 |
172 173 175 177 179
|
letrd |
|- ( ( j e. ( 0 ... M ) /\ w e. ( j ... i ) ) -> 0 <_ w ) |
181 |
180
|
adantll |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> 0 <_ w ) |
182 |
174
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w e. RR ) |
183 |
|
elfzoel2 |
|- ( i e. ( 0 ..^ M ) -> M e. ZZ ) |
184 |
183
|
zred |
|- ( i e. ( 0 ..^ M ) -> M e. RR ) |
185 |
184
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> M e. RR ) |
186 |
56
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> i e. RR ) |
187 |
|
elfzle2 |
|- ( w e. ( j ... i ) -> w <_ i ) |
188 |
187
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w <_ i ) |
189 |
|
elfzolt2 |
|- ( i e. ( 0 ..^ M ) -> i < M ) |
190 |
189
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> i < M ) |
191 |
182 186 185 188 190
|
lelttrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w < M ) |
192 |
182 185 191
|
ltled |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... i ) ) -> w <_ M ) |
193 |
192
|
adantlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w <_ M ) |
194 |
171 181 193
|
jca32 |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) ) |
195 |
194
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) ) |
196 |
|
elfz2 |
|- ( w e. ( 0 ... M ) <-> ( ( 0 e. ZZ /\ M e. ZZ /\ w e. ZZ ) /\ ( 0 <_ w /\ w <_ M ) ) ) |
197 |
195 196
|
sylibr |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> w e. ( 0 ... M ) ) |
198 |
166 197
|
ffvelrnd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... i ) ) -> ( Q ` w ) e. RR ) |
199 |
198
|
adantlr |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) /\ w e. ( j ... i ) ) -> ( Q ` w ) e. RR ) |
200 |
|
simplll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ph ) |
201 |
|
0red |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 e. RR ) |
202 |
68
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> j e. RR ) |
203 |
|
elfzelz |
|- ( w e. ( j ... ( i - 1 ) ) -> w e. ZZ ) |
204 |
203
|
zred |
|- ( w e. ( j ... ( i - 1 ) ) -> w e. RR ) |
205 |
204
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. RR ) |
206 |
176
|
ad2antlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 <_ j ) |
207 |
|
elfzle1 |
|- ( w e. ( j ... ( i - 1 ) ) -> j <_ w ) |
208 |
207
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> j <_ w ) |
209 |
201 202 205 206 208
|
letrd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 <_ w ) |
210 |
204
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. RR ) |
211 |
56
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> i e. RR ) |
212 |
184
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> M e. RR ) |
213 |
|
peano2rem |
|- ( i e. RR -> ( i - 1 ) e. RR ) |
214 |
211 213
|
syl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( i - 1 ) e. RR ) |
215 |
|
elfzle2 |
|- ( w e. ( j ... ( i - 1 ) ) -> w <_ ( i - 1 ) ) |
216 |
215
|
adantl |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w <_ ( i - 1 ) ) |
217 |
211
|
ltm1d |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( i - 1 ) < i ) |
218 |
210 214 211 216 217
|
lelttrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < i ) |
219 |
189
|
adantr |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> i < M ) |
220 |
210 211 212 218 219
|
lttrd |
|- ( ( i e. ( 0 ..^ M ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < M ) |
221 |
220
|
adantlr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w < M ) |
222 |
203
|
adantl |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ZZ ) |
223 |
|
0zd |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> 0 e. ZZ ) |
224 |
183
|
ad2antrr |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> M e. ZZ ) |
225 |
222 223 224 118
|
syl3anc |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( w e. ( 0 ..^ M ) <-> ( 0 <_ w /\ w < M ) ) ) |
226 |
209 221 225
|
mpbir2and |
|- ( ( ( i e. ( 0 ..^ M ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ( 0 ..^ M ) ) |
227 |
226
|
adantlll |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> w e. ( 0 ..^ M ) ) |
228 |
200 227 138
|
syl2anc |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) ) |
229 |
228
|
adantlr |
|- ( ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) /\ w e. ( j ... ( i - 1 ) ) ) -> ( Q ` w ) <_ ( Q ` ( w + 1 ) ) ) |
230 |
165 199 229
|
monoord |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) ) /\ j <_ i ) -> ( Q ` j ) <_ ( Q ` i ) ) |
231 |
230
|
3adantl3 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> ( Q ` j ) <_ ( Q ` i ) ) |
232 |
159 231
|
eqbrtrd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> X <_ ( Q ` i ) ) |
233 |
25
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> X e. RR ) |
234 |
|
elfzofz |
|- ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) ) |
235 |
234
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) ) |
236 |
17 235
|
ffvelrnd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR ) |
237 |
233 236
|
lenltd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) ) |
238 |
237
|
adantr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j <_ i ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) ) |
239 |
238
|
3ad2antl1 |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> ( X <_ ( Q ` i ) <-> -. ( Q ` i ) < X ) ) |
240 |
232 239
|
mpbid |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ j <_ i ) -> -. ( Q ` i ) < X ) |
241 |
155 240
|
syldan |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> -. ( Q ` i ) < X ) |
242 |
241
|
intnanrd |
|- ( ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) /\ -. i < j ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) |
243 |
150 242
|
pm2.61dan |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) |
244 |
243
|
intnand |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) ) |
245 |
|
elioo3g |
|- ( X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) <-> ( ( ( Q ` i ) e. RR* /\ ( Q ` ( i + 1 ) ) e. RR* /\ X e. RR* ) /\ ( ( Q ` i ) < X /\ X < ( Q ` ( i + 1 ) ) ) ) ) |
246 |
244 245
|
sylnibr |
|- ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ j e. ( 0 ... M ) /\ ( Q ` j ) = X ) -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |
247 |
246
|
rexlimdv3a |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( E. j e. ( 0 ... M ) ( Q ` j ) = X -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) ) |
248 |
15 247
|
mpd |
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> -. X e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) |