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