Metamath Proof Explorer


Theorem fourierdlem20

Description: Every interval in the partition S is included in an interval of the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem20.m ( 𝜑𝑀 ∈ ℕ )
fourierdlem20.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem20.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem20.aleb ( 𝜑𝐴𝐵 )
fourierdlem20.q ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
fourierdlem20.q0 ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
fourierdlem20.qm ( 𝜑𝐵 ≤ ( 𝑄𝑀 ) )
fourierdlem20.j ( 𝜑𝐽 ∈ ( 0 ..^ 𝑁 ) )
fourierdlem20.t 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
fourierdlem20.s ( 𝜑𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
fourierdlem20.i 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < )
Assertion fourierdlem20 ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem20.m ( 𝜑𝑀 ∈ ℕ )
2 fourierdlem20.a ( 𝜑𝐴 ∈ ℝ )
3 fourierdlem20.b ( 𝜑𝐵 ∈ ℝ )
4 fourierdlem20.aleb ( 𝜑𝐴𝐵 )
5 fourierdlem20.q ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
6 fourierdlem20.q0 ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
7 fourierdlem20.qm ( 𝜑𝐵 ≤ ( 𝑄𝑀 ) )
8 fourierdlem20.j ( 𝜑𝐽 ∈ ( 0 ..^ 𝑁 ) )
9 fourierdlem20.t 𝑇 = ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
10 fourierdlem20.s ( 𝜑𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
11 fourierdlem20.i 𝐼 = sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < )
12 ssrab2 { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ( 0 ..^ 𝑀 )
13 fzossfz ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
14 fzssz ( 0 ... 𝑀 ) ⊆ ℤ
15 13 14 sstri ( 0 ..^ 𝑀 ) ⊆ ℤ
16 12 15 sstri { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℤ
17 16 a1i ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℤ )
18 0z 0 ∈ ℤ
19 0le0 0 ≤ 0
20 eluz2 ( 0 ∈ ( ℤ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0 ) )
21 18 18 19 20 mpbir3an 0 ∈ ( ℤ ‘ 0 )
22 21 a1i ( 𝜑 → 0 ∈ ( ℤ ‘ 0 ) )
23 1 nnzd ( 𝜑𝑀 ∈ ℤ )
24 1 nngt0d ( 𝜑 → 0 < 𝑀 )
25 elfzo2 ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ( ℤ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
26 22 23 24 25 syl3anbrc ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
27 13 26 sseldi ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
28 5 27 ffvelrnd ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
29 2 rexrd ( 𝜑𝐴 ∈ ℝ* )
30 3 rexrd ( 𝜑𝐵 ∈ ℝ* )
31 lbicc2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
32 29 30 4 31 syl3anc ( 𝜑𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
33 ubicc2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
34 29 30 4 33 syl3anc ( 𝜑𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
35 32 34 jca ( 𝜑 → ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) )
36 prssg ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
37 29 30 36 syl2anc ( 𝜑 → ( ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ) )
38 35 37 mpbid ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) )
39 inss2 ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 (,) 𝐵 )
40 ioossicc ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
41 39 40 sstri ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 )
42 41 a1i ( 𝜑 → ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
43 38 42 unssd ( 𝜑 → ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
44 9 43 eqsstrid ( 𝜑𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
45 2 3 iccssred ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
46 44 45 sstrd ( 𝜑𝑇 ⊆ ℝ )
47 isof1o ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto𝑇 )
48 f1of ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto𝑇𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
49 10 47 48 3syl ( 𝜑𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
50 elfzofz ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ( 0 ... 𝑁 ) )
51 8 50 syl ( 𝜑𝐽 ∈ ( 0 ... 𝑁 ) )
52 49 51 ffvelrnd ( 𝜑 → ( 𝑆𝐽 ) ∈ 𝑇 )
53 46 52 sseldd ( 𝜑 → ( 𝑆𝐽 ) ∈ ℝ )
54 44 52 sseldd ( 𝜑 → ( 𝑆𝐽 ) ∈ ( 𝐴 [,] 𝐵 ) )
55 iccgelb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ ( 𝑆𝐽 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑆𝐽 ) )
56 29 30 54 55 syl3anc ( 𝜑𝐴 ≤ ( 𝑆𝐽 ) )
57 28 2 53 6 56 letrd ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ ( 𝑆𝐽 ) )
58 fveq2 ( 𝑘 = 0 → ( 𝑄𝑘 ) = ( 𝑄 ‘ 0 ) )
59 58 breq1d ( 𝑘 = 0 → ( ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) ↔ ( 𝑄 ‘ 0 ) ≤ ( 𝑆𝐽 ) ) )
60 59 elrab ( 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) ≤ ( 𝑆𝐽 ) ) )
61 26 57 60 sylanbrc ( 𝜑 → 0 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } )
62 61 ne0d ( 𝜑 → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ≠ ∅ )
63 1 nnred ( 𝜑𝑀 ∈ ℝ )
64 12 sseli ( 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } → 𝑗 ∈ ( 0 ..^ 𝑀 ) )
65 elfzo0le ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗𝑀 )
66 64 65 syl ( 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } → 𝑗𝑀 )
67 66 adantl ( ( 𝜑𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ) → 𝑗𝑀 )
68 67 ralrimiva ( 𝜑 → ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑀 )
69 breq2 ( 𝑥 = 𝑀 → ( 𝑗𝑥𝑗𝑀 ) )
70 69 ralbidv ( 𝑥 = 𝑀 → ( ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 ↔ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑀 ) )
71 70 rspcev ( ( 𝑀 ∈ ℝ ∧ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑀 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 )
72 63 68 71 syl2anc ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 )
73 suprzcl ( ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℤ ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 ) → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } )
74 17 62 72 73 syl3anc ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } )
75 12 74 sseldi ( 𝜑 → sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
76 11 75 eqeltrid ( 𝜑𝐼 ∈ ( 0 ..^ 𝑀 ) )
77 13 76 sseldi ( 𝜑𝐼 ∈ ( 0 ... 𝑀 ) )
78 5 77 ffvelrnd ( 𝜑 → ( 𝑄𝐼 ) ∈ ℝ )
79 78 rexrd ( 𝜑 → ( 𝑄𝐼 ) ∈ ℝ* )
80 fzofzp1 ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
81 76 80 syl ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
82 5 81 ffvelrnd ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
83 82 rexrd ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
84 11 74 eqeltrid ( 𝜑𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } )
85 nfrab1 𝑘 { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) }
86 nfcv 𝑘
87 nfcv 𝑘 <
88 85 86 87 nfsup 𝑘 sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < )
89 11 88 nfcxfr 𝑘 𝐼
90 nfcv 𝑘 ( 0 ..^ 𝑀 )
91 nfcv 𝑘 𝑄
92 91 89 nffv 𝑘 ( 𝑄𝐼 )
93 nfcv 𝑘
94 nfcv 𝑘 ( 𝑆𝐽 )
95 92 93 94 nfbr 𝑘 ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 )
96 fveq2 ( 𝑘 = 𝐼 → ( 𝑄𝑘 ) = ( 𝑄𝐼 ) )
97 96 breq1d ( 𝑘 = 𝐼 → ( ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) ↔ ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 ) ) )
98 89 90 95 97 elrabf ( 𝐼 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ↔ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 ) ) )
99 84 98 sylib ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 ) ) )
100 99 simprd ( 𝜑 → ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 ) )
101 simpr ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
102 83 adantr ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
103 iccssxr ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
104 44 103 sstrdi ( 𝜑𝑇 ⊆ ℝ* )
105 fzofzp1 ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
106 8 105 syl ( 𝜑 → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
107 49 106 ffvelrnd ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ 𝑇 )
108 104 107 sseldd ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
109 108 adantr ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* )
110 xrltnle ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ* ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
111 102 109 110 syl2anc ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ↔ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
112 101 111 mpbird ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
113 fzssz ( 0 ... 𝑁 ) ⊆ ℤ
114 f1ofo ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto𝑇𝑆 : ( 0 ... 𝑁 ) –onto𝑇 )
115 10 47 114 3syl ( 𝜑𝑆 : ( 0 ... 𝑁 ) –onto𝑇 )
116 115 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝑆 : ( 0 ... 𝑁 ) –onto𝑇 )
117 ffun ( 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ → Fun 𝑄 )
118 5 117 syl ( 𝜑 → Fun 𝑄 )
119 5 fdmd ( 𝜑 → dom 𝑄 = ( 0 ... 𝑀 ) )
120 119 eqcomd ( 𝜑 → ( 0 ... 𝑀 ) = dom 𝑄 )
121 81 120 eleqtrd ( 𝜑 → ( 𝐼 + 1 ) ∈ dom 𝑄 )
122 fvelrn ( ( Fun 𝑄 ∧ ( 𝐼 + 1 ) ∈ dom 𝑄 ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
123 118 121 122 syl2anc ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
124 123 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ran 𝑄 )
125 29 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐴 ∈ ℝ* )
126 30 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐵 ∈ ℝ* )
127 82 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
128 45 54 sseldd ( 𝜑 → ( 𝑆𝐽 ) ∈ ℝ )
129 14 sseli ( 𝐼 ∈ ( 0 ... 𝑀 ) → 𝐼 ∈ ℤ )
130 zre ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
131 77 129 130 3syl ( 𝜑𝐼 ∈ ℝ )
132 131 adantr ( ( 𝜑 ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 ∈ ℝ )
133 132 ltp1d ( ( 𝜑 ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 < ( 𝐼 + 1 ) )
134 133 adantlr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝐼 < ( 𝐼 + 1 ) )
135 simplr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
136 128 ad2antrr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑆𝐽 ) ∈ ℝ )
137 simpr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
138 135 136 137 nltled ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) )
139 131 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → 𝐼 ∈ ℝ )
140 1red ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → 1 ∈ ℝ )
141 139 140 readdcld ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝐼 + 1 ) ∈ ℝ )
142 elfzoelz ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℤ )
143 142 zred ( 𝑗 ∈ ( 0 ..^ 𝑀 ) → 𝑗 ∈ ℝ )
144 143 ssriv ( 0 ..^ 𝑀 ) ⊆ ℝ
145 12 144 sstri { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℝ
146 145 a1i ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℝ )
147 62 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ≠ ∅ )
148 72 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 )
149 82 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
150 128 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑆𝐽 ) ∈ ℝ )
151 3 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → 𝐵 ∈ ℝ )
152 simpr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) )
153 46 107 sseldd ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
154 153 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
155 elfzoelz ( 𝐽 ∈ ( 0 ..^ 𝑁 ) → 𝐽 ∈ ℤ )
156 zre ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
157 8 155 156 3syl ( 𝜑𝐽 ∈ ℝ )
158 157 ltp1d ( 𝜑𝐽 < ( 𝐽 + 1 ) )
159 isorel ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
160 10 51 106 159 syl12anc ( 𝜑 → ( 𝐽 < ( 𝐽 + 1 ) ↔ ( 𝑆𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
161 158 160 mpbid ( 𝜑 → ( 𝑆𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
162 161 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑆𝐽 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
163 44 107 sseldd ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
164 iccleub ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
165 29 30 163 164 syl3anc ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
166 165 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
167 150 154 151 162 166 ltletrd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑆𝐽 ) < 𝐵 )
168 149 150 151 152 167 lelttrd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
169 168 adantr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
170 3 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ ℝ )
171 82 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
172 7 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ≤ ( 𝑄𝑀 ) )
173 23 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℤ )
174 81 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
175 fzval3 ( 𝑀 ∈ ℤ → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
176 23 175 syl ( 𝜑 → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
177 176 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 0 ... 𝑀 ) = ( 0 ..^ ( 𝑀 + 1 ) ) )
178 174 177 eleqtrd ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) )
179 simpr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
180 178 179 jca ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) )
181 elfzonelfzo ( 𝑀 ∈ ℤ → ( ( ( 𝐼 + 1 ) ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) ) )
182 173 180 181 sylc ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
183 fzval3 ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
184 23 183 syl ( 𝜑 → ( 𝑀 ... 𝑀 ) = ( 𝑀 ..^ ( 𝑀 + 1 ) ) )
185 184 eqcomd ( 𝜑 → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = ( 𝑀 ... 𝑀 ) )
186 185 adantr ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑀 ..^ ( 𝑀 + 1 ) ) = ( 𝑀 ... 𝑀 ) )
187 182 186 eleqtrd ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑀 ) )
188 elfz1eq ( ( 𝐼 + 1 ) ∈ ( 𝑀 ... 𝑀 ) → ( 𝐼 + 1 ) = 𝑀 )
189 187 188 syl ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐼 + 1 ) = 𝑀 )
190 189 eqcomd ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝑀 = ( 𝐼 + 1 ) )
191 190 fveq2d ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑀 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
192 172 191 breqtrd ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
193 170 171 192 lensymd ( ( 𝜑 ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
194 193 adantlr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) ∧ ¬ ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
195 169 194 condan ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) )
196 nfcv 𝑘 +
197 nfcv 𝑘 1
198 89 196 197 nfov 𝑘 ( 𝐼 + 1 )
199 91 198 nffv 𝑘 ( 𝑄 ‘ ( 𝐼 + 1 ) )
200 199 93 94 nfbr 𝑘 ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 )
201 fveq2 ( 𝑘 = ( 𝐼 + 1 ) → ( 𝑄𝑘 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
202 201 breq1d ( 𝑘 = ( 𝐼 + 1 ) → ( ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) ↔ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) )
203 198 90 200 202 elrabf ( ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ↔ ( ( 𝐼 + 1 ) ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) )
204 195 152 203 sylanbrc ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } )
205 suprub ( ( ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ⊆ ℝ ∧ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } 𝑗𝑥 ) ∧ ( 𝐼 + 1 ) ∈ { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < ) )
206 146 147 148 204 205 syl31anc ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝐼 + 1 ) ≤ sup ( { 𝑘 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄𝑘 ) ≤ ( 𝑆𝐽 ) } , ℝ , < ) )
207 206 11 breqtrrdi ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ( 𝐼 + 1 ) ≤ 𝐼 )
208 141 139 207 lensymd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
209 208 adantlr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ ( 𝑆𝐽 ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
210 138 209 syldan ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ∧ ¬ ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ 𝐼 < ( 𝐼 + 1 ) )
211 134 210 condan ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) → ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
212 82 211 mpdan ( 𝜑 → ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
213 2 128 82 56 212 lelttrd ( 𝜑𝐴 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
214 213 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐴 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
215 153 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∈ ℝ )
216 3 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → 𝐵 ∈ ℝ )
217 simpr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
218 165 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ 𝐵 )
219 127 215 216 217 218 ltletrd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < 𝐵 )
220 125 126 127 214 219 eliood ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 (,) 𝐵 ) )
221 124 220 elind ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) )
222 elun2 ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) )
223 221 222 syl ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( { 𝐴 , 𝐵 } ∪ ( ran 𝑄 ∩ ( 𝐴 (,) 𝐵 ) ) ) )
224 223 9 eleqtrrdi ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 )
225 foelrn ( ( 𝑆 : ( 0 ... 𝑁 ) –onto𝑇 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) )
226 116 224 225 syl2anc ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) )
227 212 adantr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝐽 ) < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
228 simpr ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) )
229 227 228 breqtrd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝐽 ) < ( 𝑆𝑗 ) )
230 229 adantlr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝐽 ) < ( 𝑆𝑗 ) )
231 10 ad2antrr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
232 51 anim1i ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) )
233 232 adantr ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) )
234 isorel ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝐽 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆𝐽 ) < ( 𝑆𝑗 ) ) )
235 231 233 234 syl2anc ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝐽 < 𝑗 ↔ ( 𝑆𝐽 ) < ( 𝑆𝑗 ) ) )
236 230 235 mpbird ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → 𝐽 < 𝑗 )
237 236 adantllr ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → 𝐽 < 𝑗 )
238 eqcom ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ↔ ( 𝑆𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
239 238 biimpi ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) → ( 𝑆𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
240 239 adantl ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝑗 ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
241 simpl ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
242 240 241 eqbrtrd ( ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
243 242 adantll ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
244 243 adantlr ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) )
245 10 ad2antrr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
246 simpr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
247 106 ad2antrr ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) )
248 isorel ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐽 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
249 245 246 247 248 syl12anc ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
250 249 adantr ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝑗 < ( 𝐽 + 1 ) ↔ ( 𝑆𝑗 ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) )
251 244 250 mpbird ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → 𝑗 < ( 𝐽 + 1 ) )
252 237 251 jca ( ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) ) → ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
253 252 ex ( ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) → ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) )
254 253 reximdva ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝑄 ‘ ( 𝐼 + 1 ) ) = ( 𝑆𝑗 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) )
255 226 254 mpd ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
256 ssrexv ( ( 0 ... 𝑁 ) ⊆ ℤ → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) )
257 113 255 256 mpsyl ( ( 𝜑 ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) < ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
258 112 257 syldan ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
259 simplr ( ( ( 𝜑𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 ∈ ℤ )
260 8 155 syl ( 𝜑𝐽 ∈ ℤ )
261 260 ad2antrr ( ( ( 𝜑𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 ∈ ℤ )
262 simprl ( ( ( 𝜑𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) → 𝐽 < 𝑗 )
263 simprr ( ( ( 𝜑𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) → 𝑗 < ( 𝐽 + 1 ) )
264 btwnnz ( ( 𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) → ¬ 𝑗 ∈ ℤ )
265 261 262 263 264 syl3anc ( ( ( 𝜑𝑗 ∈ ℤ ) ∧ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) ) → ¬ 𝑗 ∈ ℤ )
266 259 265 pm2.65da ( ( 𝜑𝑗 ∈ ℤ ) → ¬ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
267 266 nrexdv ( 𝜑 → ¬ ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
268 267 adantr ( ( 𝜑 ∧ ¬ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → ¬ ∃ 𝑗 ∈ ℤ ( 𝐽 < 𝑗𝑗 < ( 𝐽 + 1 ) ) )
269 258 268 condan ( 𝜑 → ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
270 ioossioo ( ( ( ( 𝑄𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) ∧ ( ( 𝑄𝐼 ) ≤ ( 𝑆𝐽 ) ∧ ( 𝑆 ‘ ( 𝐽 + 1 ) ) ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
271 79 83 100 269 270 syl22anc ( 𝜑 → ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
272 fveq2 ( 𝑖 = 𝐼 → ( 𝑄𝑖 ) = ( 𝑄𝐼 ) )
273 oveq1 ( 𝑖 = 𝐼 → ( 𝑖 + 1 ) = ( 𝐼 + 1 ) )
274 273 fveq2d ( 𝑖 = 𝐼 → ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
275 272 274 oveq12d ( 𝑖 = 𝐼 → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑄𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
276 275 sseq2d ( 𝑖 = 𝐼 → ( ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
277 276 rspcev ( ( 𝐼 ∈ ( 0 ..^ 𝑀 ) ∧ ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
278 76 271 277 syl2anc ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑆𝐽 ) (,) ( 𝑆 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )