Metamath Proof Explorer

Theorem fourierdlem11

Description: If there is a partition, than the lower bound is strictly less than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem11.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem11.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem11.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
Assertion fourierdlem11 ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem11.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem11.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fourierdlem11.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
4 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
5 2 4 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
6 3 5 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
7 6 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
8 7 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
9 8 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
10 6 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
11 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
12 10 11 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
13 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
14 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
15 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
16 15 leidd ⊢ ( 𝜑 → 0 ≤ 0 )
17 2 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
18 2 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
19 15 17 18 ltled ⊢ ( 𝜑 → 0 ≤ 𝑀 )
20 13 14 13 16 19 elfzd ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
21 12 20 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
22 9 21 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
23 8 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
24 17 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
25 13 14 14 19 24 elfzd ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
26 12 25 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
27 23 26 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
28 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
29 0le1 ⊢ 0 ≤ 1
30 29 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
31 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
32 13 14 28 30 31 elfzd ⊢ ( 𝜑 → 1 ∈ ( 0 ... 𝑀 ) )
33 12 32 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ℝ )
34 elfzo ⊢ ( ( 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 0 ∧ 0 < 𝑀 ) ) )
35 13 13 14 34 syl3anc ⊢ ( 𝜑 → ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 0 ∧ 0 < 𝑀 ) ) )
36 16 18 35 mpbir2and ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
37 0re ⊢ 0 ∈ ℝ
38 eleq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 0 ∈ ( 0 ..^ 𝑀 ) ) )
39 38 anbi2d ⊢ ( 𝑖 = 0 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) ) )
40 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 0 ) )
41 oveq1 ⊢ ( 𝑖 = 0 → ( 𝑖 + 1 ) = ( 0 + 1 ) )
42 41 fveq2d ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 0 + 1 ) ) )
43 40 42 breq12d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) )
44 39 43 imbi12d ⊢ ( 𝑖 = 0 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) ) )
45 7 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
46 45 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
47 44 46 vtoclg ⊢ ( 0 ∈ ℝ → ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) ) )
48 37 47 ax-mp ⊢ ( ( 𝜑 ∧ 0 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) )
49 36 48 mpdan ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) < ( 𝑄 ‘ ( 0 + 1 ) ) )
50 0p1e1 ⊢ ( 0 + 1 ) = 1
51 50 a1i ⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
52 51 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 0 + 1 ) ) = ( 𝑄 ‘ 1 ) )
53 49 9 52 3brtr3d ⊢ ( 𝜑 → 𝐴 < ( 𝑄 ‘ 1 ) )
54 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
55 2 54 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
56 12 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
57 0zd ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℤ )
58 elfzel2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑀 ∈ ℤ )
59 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℤ )
60 0red ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
61 59 zred ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ℝ )
62 1red ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
63 0lt1 ⊢ 0 < 1
64 63 a1i ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 < 1 )
65 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑖 )
66 60 62 61 64 65 ltletrd ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 < 𝑖 )
67 60 61 66 ltled ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 0 ≤ 𝑖 )
68 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ≤ 𝑀 )
69 57 58 59 67 68 elfzd ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
71 56 70 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
72 12 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
73 0zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 ∈ ℤ )
74 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℤ )
75 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑖 ∈ ℤ )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ℤ )
77 0red ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 0 ∈ ℝ )
78 75 zred ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑖 ∈ ℝ )
79 1red ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 1 ∈ ℝ )
80 63 a1i ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 0 < 1 )
81 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 1 ≤ 𝑖 )
82 77 79 78 80 81 ltletrd ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 0 < 𝑖 )
83 77 78 82 ltled ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 0 ≤ 𝑖 )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 ≤ 𝑖 )
85 78 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ℝ )
86 17 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℝ )
87 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
88 86 87 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 1 ) ∈ ℝ )
89 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑖 ≤ ( 𝑀 − 1 ) )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ≤ ( 𝑀 − 1 ) )
91 86 ltm1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 1 ) < 𝑀 )
92 85 88 86 90 91 lelttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 < 𝑀 )
93 85 86 92 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ≤ 𝑀 )
94 73 74 76 84 93 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
95 72 94 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
96 76 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℤ )
97 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 ∈ ℝ )
98 peano2re ⊢ ( 𝑖 ∈ ℝ → ( 𝑖 + 1 ) ∈ ℝ )
99 85 98 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ℝ )
100 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℝ )
101 63 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 < 1 )
102 78 98 syl ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → ( 𝑖 + 1 ) ∈ ℝ )
103 78 ltp1d ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 𝑖 < ( 𝑖 + 1 ) )
104 79 78 102 81 103 lelttrd ⊢ ( 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) → 1 < ( 𝑖 + 1 ) )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 1 < ( 𝑖 + 1 ) )
106 97 100 99 101 105 lttrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 < ( 𝑖 + 1 ) )
107 97 99 106 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 0 ≤ ( 𝑖 + 1 ) )
108 85 88 100 90 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ ( ( 𝑀 − 1 ) + 1 ) )
109 2 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
110 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
111 109 110 npcand ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
112 111 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
113 108 112 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ≤ 𝑀 )
114 73 74 96 107 113 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
115 72 114 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
116 elfzo ⊢ ( ( 𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑖 ∧ 𝑖 < 𝑀 ) ) )
117 76 73 74 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑖 ∧ 𝑖 < 𝑀 ) ) )
118 84 92 117 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
119 118 46 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
120 95 115 119 ltled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
121 55 71 120 monoord ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ≤ ( 𝑄 ‘ 𝑀 ) )
122 121 23 breqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ≤ 𝐵 )
123 22 33 27 53 122 ltletrd ⊢ ( 𝜑 → 𝐴 < 𝐵 )
124 22 27 123 3jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )