Metamath Proof Explorer

Theorem fourierdlem37

Description: I is a function that maps any real point to the point that in the partition that immediately precedes the corresponding periodic point in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem37.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem37.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem37.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem37.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem37.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
fourierdlem37.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
fourierdlem37.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
Assertion fourierdlem37 ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem37.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 fourierdlem37.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 fourierdlem37.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
4 fourierdlem37.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
5 fourierdlem37.e ⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
6 fourierdlem37.l ⊢ 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) )
7 fourierdlem37.i ⊢ 𝐼 = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) )
8 ssrab2 ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ( 0 ..^ 𝑀 )
9 ltso ⊢ < Or ℝ
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → < Or ℝ )
11 fzfi ⊢ ( 0 ... 𝑀 ) ∈ Fin
12 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
13 8 12 sstri ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ( 0 ... 𝑀 )
14 ssfi ⊢ ( ( ( 0 ... 𝑀 ) ∈ Fin ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ( 0 ... 𝑀 ) ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ∈ Fin )
15 11 13 14 mp2an ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ∈ Fin
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ∈ Fin )
17 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
18 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
19 2 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
20 fzolb ⊢ ( 0 ∈ ( 0 ..^ 𝑀 ) ↔ ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
21 17 18 19 20 syl3anbrc ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝑀 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ( 0 ..^ 𝑀 ) )
23 1 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
24 2 23 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
25 3 24 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
26 25 simprd ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
27 26 simplld ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
28 1 2 3 fourierdlem11 ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) )
29 28 simp1d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
30 27 29 eqeltrd ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
31 30 27 eqled ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ 𝐴 )
33 iftrue ⊢ ( ( 𝐸 ‘ 𝑥 ) = 𝐵 → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) = 𝐴 )
34 33 eqcomd ⊢ ( ( 𝐸 ‘ 𝑥 ) = 𝐵 → 𝐴 = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → 𝐴 = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
36 32 35 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
37 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ∈ ℝ )
38 29 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
39 38 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
40 28 simp2d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
42 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
43 39 41 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
44 28 simp3d ⊢ ( 𝜑 → 𝐴 < 𝐵 )
45 29 40 44 4 5 fourierdlem4 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )
46 45 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) )
47 43 46 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐸 ‘ 𝑥 ) ∈ ℝ )
48 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) = 𝐴 )
49 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) ) )
50 39 41 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) ) )
51 46 50 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐸 ‘ 𝑥 ) ∈ ℝ ∧ 𝐴 < ( 𝐸 ‘ 𝑥 ) ∧ ( 𝐸 ‘ 𝑥 ) ≤ 𝐵 ) )
52 51 simp2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 < ( 𝐸 ‘ 𝑥 ) )
53 48 52 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) < ( 𝐸 ‘ 𝑥 ) )
54 37 47 53 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐸 ‘ 𝑥 ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐸 ‘ 𝑥 ) )
56 iffalse ⊢ ( ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) = ( 𝐸 ‘ 𝑥 ) )
57 56 eqcomd ⊢ ( ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 → ( 𝐸 ‘ 𝑥 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
58 57 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝐸 ‘ 𝑥 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
59 55 58 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
60 36 59 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
61 6 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐿 = ( 𝑦 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) ) )
62 eqeq1 ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → ( 𝑦 = 𝐵 ↔ ( 𝐸 ‘ 𝑥 ) = 𝐵 ) )
63 id ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → 𝑦 = ( 𝐸 ‘ 𝑥 ) )
64 62 63 ifbieq2d ⊢ ( 𝑦 = ( 𝐸 ‘ 𝑥 ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
65 64 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 = ( 𝐸 ‘ 𝑥 ) ) → if ( 𝑦 = 𝐵 , 𝐴 , 𝑦 ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
66 38 47 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) ∈ ℝ )
67 61 65 46 66 fvmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) = if ( ( 𝐸 ‘ 𝑥 ) = 𝐵 , 𝐴 , ( 𝐸 ‘ 𝑥 ) ) )
68 60 67 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) )
69 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 0 ) )
70 69 breq1d ⊢ ( 𝑖 = 0 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
71 70 elrab ⊢ ( 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ↔ ( 0 ∈ ( 0 ..^ 𝑀 ) ∧ ( 𝑄 ‘ 0 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) ) )
72 22 68 71 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } )
73 72 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ )
74 fzssz ⊢ ( 0 ... 𝑀 ) ⊆ ℤ
75 12 74 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℤ
76 zssre ⊢ ℤ ⊆ ℝ
77 75 76 sstri ⊢ ( 0 ..^ 𝑀 ) ⊆ ℝ
78 8 77 sstri ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ℝ
79 78 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ℝ )
80 fisupcl ⊢ ( ( < Or ℝ ∧ ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ∈ Fin ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ≠ ∅ ∧ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ⊆ ℝ ) ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } )
81 10 16 73 79 80 syl13anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } )
82 8 81 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) )
83 82 7 fmptd ⊢ ( 𝜑 → 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) )
84 81 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) )
85 83 84 jca ⊢ ( 𝜑 → ( 𝐼 : ℝ ⟶ ( 0 ..^ 𝑀 ) ∧ ( 𝑥 ∈ ℝ → sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } , ℝ , < ) ∈ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )