Metamath Proof Explorer

Theorem fourierdlem15

Description: The range of the partition is between its starting point and its ending point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem15.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem15.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem15.3 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
Assertion fourierdlem15 ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem15.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem15.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fourierdlem15.3 ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
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 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
8 reex ⊢ ℝ ∈ V
9 8 a1i ⊢ ( 𝜑 → ℝ ∈ V )
10 ovex ⊢ ( 0 ... 𝑀 ) ∈ V
11 10 a1i ⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
12 9 11 elmapd ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) )
13 7 12 mpbid ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
14 ffn ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → 𝑄 Fn ( 0 ... 𝑀 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
16 6 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
17 16 simpld ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) )
18 17 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
19 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
20 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
21 19 20 eleqtrdi ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
22 2 21 syl ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
23 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
24 22 23 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
25 13 24 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
26 18 25 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝐴 ∈ ℝ )
28 17 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
29 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
30 22 29 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
31 13 30 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
32 28 31 eqeltrrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝐵 ∈ ℝ )
34 13 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
35 18 eqcomd ⊢ ( 𝜑 → 𝐴 = ( 𝑄 ‘ 0 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝐴 = ( 𝑄 ‘ 0 ) )
37 elfzuz ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
39 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
40 0zd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 0 ∈ ℤ )
41 elfzel2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℤ )
42 41 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑀 ∈ ℤ )
43 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑖 ) → 𝑗 ∈ ℤ )
44 43 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ∈ ℤ )
45 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑖 ) → 0 ≤ 𝑗 )
46 45 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 0 ≤ 𝑗 )
47 43 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑖 ) → 𝑗 ∈ ℝ )
48 47 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ∈ ℝ )
49 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℤ )
50 49 zred ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ∈ ℝ )
51 50 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑖 ∈ ℝ )
52 41 zred ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ℝ )
53 52 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑀 ∈ ℝ )
54 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑖 ) → 𝑗 ≤ 𝑖 )
55 54 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ≤ 𝑖 )
56 elfzle2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑖 ≤ 𝑀 )
57 56 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑖 ≤ 𝑀 )
58 48 51 53 55 57 letrd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ≤ 𝑀 )
59 40 42 44 46 58 elfzd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
60 59 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
61 39 60 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑖 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
62 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝜑 )
63 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 0 ≤ 𝑗 )
64 63 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 0 ≤ 𝑗 )
65 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝑗 ∈ ℤ )
66 65 zred ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝑗 ∈ ℝ )
67 66 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℝ )
68 50 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑖 ∈ ℝ )
69 52 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℝ )
70 peano2rem ⊢ ( 𝑖 ∈ ℝ → ( 𝑖 − 1 ) ∈ ℝ )
71 68 70 syl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) ∈ ℝ )
72 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝑗 ≤ ( 𝑖 − 1 ) )
73 72 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 ≤ ( 𝑖 − 1 ) )
74 68 ltm1d ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑖 − 1 ) < 𝑖 )
75 67 71 68 73 74 lelttrd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 < 𝑖 )
76 56 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑖 ≤ 𝑀 )
77 67 68 69 75 76 ltletrd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 < 𝑀 )
78 65 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ℤ )
79 0zd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 0 ∈ ℤ )
80 41 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑀 ∈ ℤ )
81 elfzo ⊢ ( ( 𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 < 𝑀 ) ) )
82 78 79 80 81 syl3anc ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 < 𝑀 ) ) )
83 64 77 82 mpbir2and ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
84 83 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
85 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
86 elfzofz ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
87 86 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
88 85 87 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
89 fzofzp1 ⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
91 85 90 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
92 eleq1w ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) )
93 92 anbi2d ⊢ ( 𝑖 = 𝑗 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) ) )
94 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑗 ) )
95 oveq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 + 1 ) = ( 𝑗 + 1 ) )
96 95 fveq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
97 94 96 breq12d ⊢ ( 𝑖 = 𝑗 → ( ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
98 93 97 imbi12d ⊢ ( 𝑖 = 𝑗 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) )
99 16 simprd ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
100 99 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
101 98 100 chvarvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
102 88 91 101 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
103 62 84 102 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
104 38 61 103 monoord ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 0 ) ≤ ( 𝑄 ‘ 𝑖 ) )
105 36 104 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝑖 ) )
106 elfzuz3 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑖 ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑖 ) )
108 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
109 fz0fzelfz0 ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
110 109 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
111 108 110 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
112 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
113 0zd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ∈ ℤ )
114 41 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℤ )
115 elfzelz ⊢ ( 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑗 ∈ ℤ )
116 115 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ℤ )
117 0red ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ∈ ℝ )
118 50 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑖 ∈ ℝ )
119 115 zred ⊢ ( 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑗 ∈ ℝ )
120 119 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ℝ )
121 elfzle1 ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → 0 ≤ 𝑖 )
122 121 adantr ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ≤ 𝑖 )
123 elfzle1 ⊢ ( 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑖 ≤ 𝑗 )
124 123 adantl ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑖 ≤ 𝑗 )
125 117 118 120 122 124 letrd ⊢ ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ≤ 𝑗 )
126 125 adantll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ≤ 𝑗 )
127 119 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ℝ )
128 2 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℝ )
130 1red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℝ )
131 129 130 resubcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 1 ) ∈ ℝ )
132 elfzle2 ⊢ ( 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) → 𝑗 ≤ ( 𝑀 − 1 ) )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ≤ ( 𝑀 − 1 ) )
134 129 ltm1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑀 − 1 ) < 𝑀 )
135 127 131 129 133 134 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 < 𝑀 )
136 127 129 135 ltled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ≤ 𝑀 )
137 136 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ≤ 𝑀 )
138 113 114 116 126 137 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
139 112 138 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑗 ) ∈ ℝ )
140 116 peano2zd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℤ )
141 119 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ℝ )
142 1red ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℝ )
143 0le1 ⊢ 0 ≤ 1
144 143 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ≤ 1 )
145 141 142 126 144 addge0d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 0 ≤ ( 𝑗 + 1 ) )
146 127 131 130 133 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ ( ( 𝑀 − 1 ) + 1 ) )
147 2 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑀 ∈ ℂ )
149 1cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 1 ∈ ℂ )
150 148 149 npcand ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( ( 𝑀 − 1 ) + 1 ) = 𝑀 )
151 146 150 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑀 )
152 151 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 + 1 ) ≤ 𝑀 )
153 113 114 140 145 152 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ( 0 ... 𝑀 ) )
154 112 153 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
155 simpll ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝜑 )
156 135 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 < 𝑀 )
157 116 113 114 81 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 < 𝑀 ) ) )
158 126 156 157 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
159 155 158 101 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑗 ) < ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
160 139 154 159 ltled ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) ∧ 𝑗 ∈ ( 𝑖 ... ( 𝑀 − 1 ) ) ) → ( 𝑄 ‘ 𝑗 ) ≤ ( 𝑄 ‘ ( 𝑗 + 1 ) ) )
161 107 111 160 monoord ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ ( 𝑄 ‘ 𝑀 ) )
162 28 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑀 ) = 𝐵 )
163 161 162 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ≤ 𝐵 )
164 27 33 34 105 163 eliccd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( 𝐴 [,] 𝐵 ) )
165 164 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) ∈ ( 𝐴 [,] 𝐵 ) )
166 fnfvrnss ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ∀ 𝑖 ∈ ( 0 ... 𝑀 ) ( 𝑄 ‘ 𝑖 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) )
167 15 165 166 syl2anc ⊢ ( 𝜑 → ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) )
168 df-f ⊢ ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ran 𝑄 ⊆ ( 𝐴 [,] 𝐵 ) ) )
169 15 167 168 sylanbrc ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )