fourierdlem52

Description: d16:d17,d18:jca |- ( ph -> ( ( S 0 ) <_ A /\ A <_ ( S 0 ) ) ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem52.tf	$⊢ φ \to T \in Fin$
	fourierdlem52.n	$⊢ N = \|T\| - 1$
	fourierdlem52.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
	fourierdlem52.a	$⊢ φ \to A \in ℝ$
	fourierdlem52.b	$⊢ φ \to B \in ℝ$
	fourierdlem52.t	$⊢ φ \to T \subseteq [A, B]$
	fourierdlem52.at	$⊢ φ \to A \in T$
	fourierdlem52.bt	$⊢ φ \to B \in T$
Assertion	fourierdlem52	$⊢ φ \to ((S : (0 \dots N) ⟶ [A, B] \land S (0) = A) \land S (N) = B)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem52.tf	$⊢ φ \to T \in Fin$
2		fourierdlem52.n	$⊢ N = \|T\| - 1$
3		fourierdlem52.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
4		fourierdlem52.a	$⊢ φ \to A \in ℝ$
5		fourierdlem52.b	$⊢ φ \to B \in ℝ$
6		fourierdlem52.t	$⊢ φ \to T \subseteq [A, B]$
7		fourierdlem52.at	$⊢ φ \to A \in T$
8		fourierdlem52.bt	$⊢ φ \to B \in T$
9	4 5	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
10	6 9	sstrd	$⊢ φ \to T \subseteq ℝ$
11	1 10 3 2	fourierdlem36	$⊢ φ \to S {Isom}_{<, <} ((0 \dots N), T)$
12		isof1o	$⊢ S {Isom}_{<, <} ((0 \dots N), T) \to S : (0 \dots N) \underset{1-1 onto}{⟶} T$
13		f1of	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} T \to S : (0 \dots N) ⟶ T$
14	11 12 13	3syl	$⊢ φ \to S : (0 \dots N) ⟶ T$
15	14 6	fssd	$⊢ φ \to S : (0 \dots N) ⟶ [A, B]$
16		f1ofo	$⊢ S : (0 \dots N) \underset{1-1 onto}{⟶} T \to S : (0 \dots N) \underset{onto}{⟶} T$
17	11 12 16	3syl	$⊢ φ \to S : (0 \dots N) \underset{onto}{⟶} T$
18		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} T \land A \in T) \to \exists j \in (0 \dots N) A = S (j)$
19	17 7 18	syl2anc	$⊢ φ \to \exists j \in (0 \dots N) A = S (j)$
20		elfzle1	$⊢ j \in (0 \dots N) \to 0 \leq j$
21	20	adantl	$⊢ (φ \land j \in (0 \dots N)) \to 0 \leq j$
22	11	adantr	$⊢ (φ \land j \in (0 \dots N)) \to S {Isom}_{<, <} ((0 \dots N), T)$
23		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
24	10 23	sstrdi	$⊢ φ \to T \subseteq ℝ^{*}$
25	24	adantr	$⊢ (φ \land j \in (0 \dots N)) \to T \subseteq ℝ^{*}$
26		fzssz	$⊢ (0 \dots N) \subseteq ℤ$
27		zssre	$⊢ ℤ \subseteq ℝ$
28	27 23	sstri	$⊢ ℤ \subseteq ℝ^{*}$
29	26 28	sstri	$⊢ (0 \dots N) \subseteq ℝ^{*}$
30	25 29	jctil	$⊢ (φ \land j \in (0 \dots N)) \to ((0 \dots N) \subseteq ℝ^{} \land T \subseteq ℝ^{})$
31		hashcl	$⊢ T \in Fin \to \|T\| \in ℕ_{0}$
32	1 31	syl	$⊢ φ \to \|T\| \in ℕ_{0}$
33	7	ne0d	$⊢ φ \to T \neq \emptyset$
34		hashge1	$⊢ (T \in Fin \land T \neq \emptyset) \to 1 \leq \|T\|$
35	1 33 34	syl2anc	$⊢ φ \to 1 \leq \|T\|$
36		elnnnn0c	$⊢ \|T\| \in ℕ \leftrightarrow (\|T\| \in ℕ_{0} \land 1 \leq \|T\|)$
37	32 35 36	sylanbrc	$⊢ φ \to \|T\| \in ℕ$
38		nnm1nn0	$⊢ \|T\| \in ℕ \to \|T\| - 1 \in ℕ_{0}$
39	37 38	syl	$⊢ φ \to \|T\| - 1 \in ℕ_{0}$
40	2 39	eqeltrid	$⊢ φ \to N \in ℕ_{0}$
41		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
42	40 41	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
43		eluzfz1	$⊢ N \in ℤ_{\geq 0} \to 0 \in (0 \dots N)$
44	42 43	syl	$⊢ φ \to 0 \in (0 \dots N)$
45	44	anim1i	$⊢ (φ \land j \in (0 \dots N)) \to (0 \in (0 \dots N) \land j \in (0 \dots N))$
46		leisorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), T) \land ((0 \dots N) \subseteq ℝ^{} \land T \subseteq ℝ^{}) \land (0 \in (0 \dots N) \land j \in (0 \dots N))) \to (0 \leq j \leftrightarrow S (0) \leq S (j))$
47	22 30 45 46	syl3anc	$⊢ (φ \land j \in (0 \dots N)) \to (0 \leq j \leftrightarrow S (0) \leq S (j))$
48	21 47	mpbid	$⊢ (φ \land j \in (0 \dots N)) \to S (0) \leq S (j)$
49	48	3adant3	$⊢ (φ \land j \in (0 \dots N) \land A = S (j)) \to S (0) \leq S (j)$
50		eqcom	$⊢ A = S (j) \leftrightarrow S (j) = A$
51	50	biimpi	$⊢ A = S (j) \to S (j) = A$
52	51	3ad2ant3	$⊢ (φ \land j \in (0 \dots N) \land A = S (j)) \to S (j) = A$
53	49 52	breqtrd	$⊢ (φ \land j \in (0 \dots N) \land A = S (j)) \to S (0) \leq A$
54	53	rexlimdv3a	$⊢ φ \to (\exists j \in (0 \dots N) A = S (j) \to S (0) \leq A)$
55	19 54	mpd	$⊢ φ \to S (0) \leq A$
56	4	rexrd	$⊢ φ \to A \in ℝ^{*}$
57	5	rexrd	$⊢ φ \to B \in ℝ^{*}$
58	15 44	ffvelrnd	$⊢ φ \to S (0) \in [A, B]$
59		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land S (0) \in [A, B]) \to A \leq S (0)$
60	56 57 58 59	syl3anc	$⊢ φ \to A \leq S (0)$
61	9 58	sseldd	$⊢ φ \to S (0) \in ℝ$
62	61 4	letri3d	$⊢ φ \to (S (0) = A \leftrightarrow (S (0) \leq A \land A \leq S (0)))$
63	55 60 62	mpbir2and	$⊢ φ \to S (0) = A$
64		eluzfz2	$⊢ N \in ℤ_{\geq 0} \to N \in (0 \dots N)$
65	42 64	syl	$⊢ φ \to N \in (0 \dots N)$
66	15 65	ffvelrnd	$⊢ φ \to S (N) \in [A, B]$
67		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land S (N) \in [A, B]) \to S (N) \leq B$
68	56 57 66 67	syl3anc	$⊢ φ \to S (N) \leq B$
69		foelrn	$⊢ (S : (0 \dots N) \underset{onto}{⟶} T \land B \in T) \to \exists j \in (0 \dots N) B = S (j)$
70	17 8 69	syl2anc	$⊢ φ \to \exists j \in (0 \dots N) B = S (j)$
71		simp3	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to B = S (j)$
72		elfzle2	$⊢ j \in (0 \dots N) \to j \leq N$
73	72	3ad2ant2	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to j \leq N$
74	11	3ad2ant1	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to S {Isom}_{<, <} ((0 \dots N), T)$
75	30	3adant3	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to ((0 \dots N) \subseteq ℝ^{} \land T \subseteq ℝ^{})$
76		simp2	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to j \in (0 \dots N)$
77	65	3ad2ant1	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to N \in (0 \dots N)$
78		leisorel	$⊢ (S {Isom}_{<, <} ((0 \dots N), T) \land ((0 \dots N) \subseteq ℝ^{} \land T \subseteq ℝ^{}) \land (j \in (0 \dots N) \land N \in (0 \dots N))) \to (j \leq N \leftrightarrow S (j) \leq S (N))$
79	74 75 76 77 78	syl112anc	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to (j \leq N \leftrightarrow S (j) \leq S (N))$
80	73 79	mpbid	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to S (j) \leq S (N)$
81	71 80	eqbrtrd	$⊢ (φ \land j \in (0 \dots N) \land B = S (j)) \to B \leq S (N)$
82	81	rexlimdv3a	$⊢ φ \to (\exists j \in (0 \dots N) B = S (j) \to B \leq S (N))$
83	70 82	mpd	$⊢ φ \to B \leq S (N)$
84	9 66	sseldd	$⊢ φ \to S (N) \in ℝ$
85	84 5	letri3d	$⊢ φ \to (S (N) = B \leftrightarrow (S (N) \leq B \land B \leq S (N)))$
86	68 83 85	mpbir2and	$⊢ φ \to S (N) = B$
87	15 63 86	jca31	$⊢ φ \to ((S : (0 \dots N) ⟶ [A, B] \land S (0) = A) \land S (N) = B)$

Metamath Proof Explorer

Theorem fourierdlem52

Proof