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 sseldi ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) < 𝐶 } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
58 5 57 eqeltrid ( 𝜑𝐼 ∈ ( 0 ..^ 𝑀 ) )
59 48 58 sseldi ( 𝜑𝐼 ∈ ( 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 sseldi ( 𝜑𝐼 ∈ ℝ )
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 sseldi ( 𝜑 → ( 𝐼 + 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 ) ) ) )