Metamath Proof Explorer

Theorem fourierdlem25

Description: If C is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem25.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem25.qf ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
fourierdlem25.cel ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
fourierdlem25.cnel ⊢ ( 𝜑 → ¬ 𝐶 ∈ ran 𝑄 )
fourierdlem25.i ⊢ 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < )
Assertion fourierdlem25 ( 𝜑 → ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) 𝐶 ∈ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem25.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 fourierdlem25.qf ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
3 fourierdlem25.cel ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) )
4 fourierdlem25.cnel ⊢ ( 𝜑 → ¬ 𝐶 ∈ ran 𝑄 )
5 fourierdlem25.i ⊢ 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < )
6 ssrab2 ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ( 0 ..^ 𝑀 )
7 ltso ⊢ < Or ℝ
8 7 a1i ⊢ ( 𝜑 → < Or ℝ )
9 fzofi ⊢ ( 0 ..^ 𝑀 ) ∈ Fin
10 ssfi ⊢ ( ( ( 0 ..^ 𝑀 ) ∈ Fin ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ( 0 ..^ 𝑀 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ∈ Fin )
11 9 6 10 mp2an ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ∈ Fin
12 11 a1i ⊢ ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ∈ Fin )
13 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
14 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
15 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
16 fzolb ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
17 13 14 15 16 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
18 elfzofz ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) → 0 ∈ ( 0 ... 𝑀 ) )
19 17 18 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
20 2 19 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
21 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
22 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
23 21 22 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
24 eluzfz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
25 23 24 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 0 ... 𝑀 ) )
26 2 25 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ )
27 20 26 iccssred ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) ⊆ ℝ )
28 27 3 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
29 20 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ* )
30 26 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ℝ* )
31 iccgelb ⊢ ( ( ( 𝑄 ‘ 0 ) ∈ ℝ* ∧ ( 𝑄 ‘ 𝑀 ) ∈ ℝ* ∧ 𝐶 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) ) → ( 𝑄 ‘ 0 ) ≤ 𝐶 )
32 29 30 3 31 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐶 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑄 ‘ 0 ) ) → 𝐶 = ( 𝑄 ‘ 0 ) )
34 2 ffnd ⊢ ( 𝜑 → 𝑄 Fn ( 0 ... 𝑀 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑄 ‘ 0 ) ) → 𝑄 Fn ( 0 ... 𝑀 ) )
36 19 adantr ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑄 ‘ 0 ) ) → 0 ∈ ( 0 ... 𝑀 ) )
37 fnfvelrn ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ 0 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 )
38 35 36 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑄 ‘ 0 ) ) → ( 𝑄 ‘ 0 ) ∈ ran 𝑄 )
39 33 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐶 = ( 𝑄 ‘ 0 ) ) → 𝐶 ∈ ran 𝑄 )
40 4 39 mtand ⊢ ( 𝜑 → ¬ 𝐶 = ( 𝑄 ‘ 0 ) )
41 40 neqned ⊢ ( 𝜑 → 𝐶 ≠ ( 𝑄 ‘ 0 ) )
42 20 28 32 41 leneltd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) < 𝐶 )
43 fveq2 ⊢ ( 𝑘 = 0 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 0 ) )
44 43 breq1d ⊢ ( 𝑘 = 0 → ( ( 𝑄 ‘ 𝑘 ) < 𝐶 ↔ ( 𝑄 ‘ 0 ) < 𝐶 ) )
45 44 elrab ⊢ ( 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) < 𝐶 ) )
46 17 42 45 sylanbrc ⊢ ( 𝜑 → 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } )
47 46 ne0d ⊢ ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ≠ ∅ )
48 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
49 fzssz ⊢ ( 0 ... 𝑀 ) ⊆ ℤ
50 zssre ⊢ ℤ ⊆ ℝ
51 49 50 sstri ⊢ ( 0 ... 𝑀 ) ⊆ ℝ
52 48 51 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℝ
53 6 52 sstri ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℝ
54 53 a1i ⊢ ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℝ )
55 fisupcl ⊢ ( ( < Or ℝ ∧ ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ∈ Fin ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ≠ ∅ ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℝ ) ) → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } )
56 8 12 47 54 55 syl13anc ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } )
57 6 56 sselid ⊢ ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
58 5 57 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
59 48 58 sselid ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
60 2 59 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ )
61 60 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
62 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
63 58 62 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
64 2 63 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
65 64 rexrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
66 5 56 eqeltrid ⊢ ( 𝜑 → 𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } )
67 fveq2 ⊢ ( 𝑘 = 𝐼 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝐼 ) )
68 67 breq1d ⊢ ( 𝑘 = 𝐼 → ( ( 𝑄 ‘ 𝑘 ) < 𝐶 ↔ ( 𝑄 ‘ 𝐼 ) < 𝐶 ) )
69 68 elrab ⊢ ( 𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ↔ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝐼 ) < 𝐶 ) )
70 66 69 sylib ⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 𝐼 ) < 𝐶 ) )
71 70 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) < 𝐶 )
72 52 58 sselid ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
73 ltp1 ⊢ ( 𝐼 ∈ ℝ → 𝐼 < ( 𝐼 + 1 ) )
74 id ⊢ ( 𝐼 ∈ ℝ → 𝐼 ∈ ℝ )
75 peano2re ⊢ ( 𝐼 ∈ ℝ → ( 𝐼 + 1 ) ∈ ℝ )
76 74 75 ltnled ⊢ ( 𝐼 ∈ ℝ → ( 𝐼 < ( 𝐼 + 1 ) ↔ ¬ ( 𝐼 + 1 ) ≤ 𝐼 ) )
77 73 76 mpbid ⊢ ( 𝐼 ∈ ℝ → ¬ ( 𝐼 + 1 ) ≤ 𝐼 )
78 72 77 syl ⊢ ( 𝜑 → ¬ ( 𝐼 + 1 ) ≤ 𝐼 )
79 48 49 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℤ
80 6 79 sstri ⊢ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℤ
81 80 a1i ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℤ )
82 elrabi ⊢ ( ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } → ℎ ∈ ( 0 ..^ 𝑀 ) )
83 elfzo0le ⊢ ( ℎ ∈ ( 0 ..^ 𝑀 ) → ℎ ≤ 𝑀 )
84 82 83 syl ⊢ ( ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } → ℎ ≤ 𝑀 )
85 84 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ) → ℎ ≤ 𝑀 )
86 85 ralrimiva ⊢ ( 𝜑 → ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑀 )
87 breq2 ⊢ ( 𝑚 = 𝑀 → ( ℎ ≤ 𝑚 ↔ ℎ ≤ 𝑀 ) )
88 87 ralbidv ⊢ ( 𝑚 = 𝑀 → ( ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑚 ↔ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑀 ) )
89 88 rspcev ⊢ ( ( 𝑀 ∈ ℤ ∧ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑀 ) → ∃ 𝑚 ∈ ℤ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑚 )
90 14 86 89 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℤ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑚 )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ∃ 𝑚 ∈ ℤ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑚 )
92 elfzuz ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
93 63 92 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
95 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → 𝑀 ∈ ℤ )
96 51 63 sselid ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ℝ )
97 96 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ∈ ℝ )
98 95 zred ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → 𝑀 ∈ ℝ )
99 elfzle2 ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) → ( 𝐼 + 1 ) ≤ 𝑀 )
100 63 99 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ≤ 𝑀 )
101 100 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ≤ 𝑀 )
102 simpr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 )
103 64 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
104 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → 𝐶 ∈ ℝ )
105 103 104 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ↔ ¬ 𝐶 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
106 102 105 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ¬ 𝐶 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
107 iccleub ⊢ ( ( ( 𝑄 ‘ 0 ) ∈ ℝ* ∧ ( 𝑄 ‘ 𝑀 ) ∈ ℝ* ∧ 𝐶 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄 ‘ 𝑀 ) ) ) → 𝐶 ≤ ( 𝑄 ‘ 𝑀 ) )
108 29 30 3 107 syl3anc ⊢ ( 𝜑 → 𝐶 ≤ ( 𝑄 ‘ 𝑀 ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝑀 = ( 𝐼 + 1 ) ) → 𝐶 ≤ ( 𝑄 ‘ 𝑀 ) )
110 fveq2 ⊢ ( 𝑀 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
111 110 adantl ⊢ ( ( 𝜑 ∧ 𝑀 = ( 𝐼 + 1 ) ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
112 109 111 breqtrd ⊢ ( ( 𝜑 ∧ 𝑀 = ( 𝐼 + 1 ) ) → 𝐶 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
113 112 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) ∧ 𝑀 = ( 𝐼 + 1 ) ) → 𝐶 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
114 106 113 mtand ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ¬ 𝑀 = ( 𝐼 + 1 ) )
115 114 neqned ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → 𝑀 ≠ ( 𝐼 + 1 ) )
116 97 98 101 115 leneltd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) < 𝑀 )
117 elfzo2 ⊢ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ↔ ( ( 𝐼 + 1 ) ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ ( 𝐼 + 1 ) < 𝑀 ) )
118 94 95 116 117 syl3anbrc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
119 fveq2 ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
120 119 breq1d ⊢ ( 𝑘 = ( 𝐼 + 1 ) → ( ( 𝑄 ‘ 𝑘 ) < 𝐶 ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) )
121 120 elrab ⊢ ( ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) )
122 118 102 121 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } )
123 suprzub ⊢ ( ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ⊆ ℤ ∧ ∃ 𝑚 ∈ ℤ ∀ ℎ ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ℎ ≤ 𝑚 ∧ ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < ) )
124 81 91 122 123 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑘 ) < 𝐶 } , ℝ , < ) )
125 124 5 breqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ) → ( 𝐼 + 1 ) ≤ 𝐼 )
126 78 125 mtand ⊢ ( 𝜑 → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 )
127 eqcom ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ↔ 𝐶 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
128 127 biimpi ⊢ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 → 𝐶 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
129 128 adantl ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) → 𝐶 = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
130 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) → 𝑄 Fn ( 0 ... 𝑀 ) )
131 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
132 fnfvelrn ⊢ ( ( 𝑄 Fn ( 0 ... 𝑀 ) ∧ ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
133 130 131 132 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
134 129 133 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) → 𝐶 ∈ ran 𝑄 )
135 4 134 mtand ⊢ ( 𝜑 → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 )
136 126 135 jca ⊢ ( 𝜑 → ( ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) )
137 pm4.56 ⊢ ( ( ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ∧ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) ↔ ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ∨ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) )
138 136 137 sylib ⊢ ( 𝜑 → ¬ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ∨ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) )
139 64 28 leloed ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐶 ↔ ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐶 ∨ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = 𝐶 ) ) )
140 138 139 mtbird ⊢ ( 𝜑 → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐶 )
141 28 64 ltnled ⊢ ( 𝜑 → ( 𝐶 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ↔ ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐶 ) )
142 140 141 mpbird ⊢ ( 𝜑 → 𝐶 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
143 61 65 28 71 142 eliood ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
144 fveq2 ⊢ ( 𝑗 = 𝐼 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝐼 ) )
145 oveq1 ⊢ ( 𝑗 = 𝐼 → ( 𝑗 + 1 ) = ( 𝐼 + 1 ) )
146 145 fveq2d ⊢ ( 𝑗 = 𝐼 → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
147 144 146 oveq12d ⊢ ( 𝑗 = 𝐼 → ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
148 147 eleq2d ⊢ ( 𝑗 = 𝐼 → ( 𝐶 ∈ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ↔ 𝐶 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
149 148 rspcev ⊢ ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ 𝐶 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) 𝐶 ∈ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )
150 58 143 149 syl2anc ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 0 ..^ 𝑀 ) 𝐶 ∈ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) )