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 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( 𝐿 ‘ ( 𝐸 ‘ 𝑥 ) ) } ) ) )