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