Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑇 ∈ Fin )
fourierdlem52.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
fourierdlem52.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
fourierdlem52.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem52.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem52.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
fourierdlem52.at ⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
fourierdlem52.bt ⊢ ( 𝜑 → 𝐵 ∈ 𝑇 )
Assertion fourierdlem52 ( 𝜑 → ( ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 ‘ 0 ) = 𝐴 ) ∧ ( 𝑆 ‘ 𝑁 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem52.tf ⊢ ( 𝜑 → 𝑇 ∈ Fin )
2 fourierdlem52.n ⊢ 𝑁 = ( ( ♯ ‘ 𝑇 ) − 1 )
3 fourierdlem52.s ⊢ 𝑆 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
4 fourierdlem52.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 fourierdlem52.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
6 fourierdlem52.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐴 [,] 𝐵 ) )
7 fourierdlem52.at ⊢ ( 𝜑 → 𝐴 ∈ 𝑇 )
8 fourierdlem52.bt ⊢ ( 𝜑 → 𝐵 ∈ 𝑇 )
9 4 5 iccssred ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
10 6 9 sstrd ⊢ ( 𝜑 → 𝑇 ⊆ ℝ )
11 1 10 3 2 fourierdlem36 ⊢ ( 𝜑 → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
12 isof1o ⊢ ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) → 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 )
13 f1of ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
14 11 12 13 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ 𝑇 )
15 14 6 fssd ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) )
16 f1ofo ⊢ ( 𝑆 : ( 0 ... 𝑁 ) –1-1-onto→ 𝑇 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 )
17 11 12 16 3syl ⊢ ( 𝜑 → 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 )
18 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 ∧ 𝐴 ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐴 = ( 𝑆 ‘ 𝑗 ) )
19 17 7 18 syl2anc ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐴 = ( 𝑆 ‘ 𝑗 ) )
20 elfzle1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 0 ≤ 𝑗 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝑗 )
22 11 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
23 ressxr ⊢ ℝ ⊆ ℝ*
24 10 23 sstrdi ⊢ ( 𝜑 → 𝑇 ⊆ ℝ* )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 ⊆ ℝ* )
26 fzssz ⊢ ( 0 ... 𝑁 ) ⊆ ℤ
27 zssre ⊢ ℤ ⊆ ℝ
28 27 23 sstri ⊢ ℤ ⊆ ℝ*
29 26 28 sstri ⊢ ( 0 ... 𝑁 ) ⊆ ℝ*
30 25 29 jctil ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 0 ... 𝑁 ) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ* ) )
31 hashcl ⊢ ( 𝑇 ∈ Fin → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
32 1 31 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
33 7 ne0d ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
34 hashge1 ⊢ ( ( 𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ) → 1 ≤ ( ♯ ‘ 𝑇 ) )
35 1 33 34 syl2anc ⊢ ( 𝜑 → 1 ≤ ( ♯ ‘ 𝑇 ) )
36 elnnnn0c ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑇 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑇 ) ) )
37 32 35 36 sylanbrc ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) ∈ ℕ )
38 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑇 ) ∈ ℕ → ( ( ♯ ‘ 𝑇 ) − 1 ) ∈ ℕ0 )
39 37 38 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑇 ) − 1 ) ∈ ℕ0 )
40 2 39 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
41 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
42 40 41 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
43 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
44 42 43 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
45 44 anim1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) )
46 leisorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( ( 0 ... 𝑁 ) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ* ) ∧ ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ) → ( 0 ≤ 𝑗 ↔ ( 𝑆 ‘ 0 ) ≤ ( 𝑆 ‘ 𝑗 ) ) )
47 22 30 45 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 0 ≤ 𝑗 ↔ ( 𝑆 ‘ 0 ) ≤ ( 𝑆 ‘ 𝑗 ) ) )
48 21 47 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑆 ‘ 0 ) ≤ ( 𝑆 ‘ 𝑗 ) )
49 48 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐴 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 0 ) ≤ ( 𝑆 ‘ 𝑗 ) )
50 eqcom ⊢ ( 𝐴 = ( 𝑆 ‘ 𝑗 ) ↔ ( 𝑆 ‘ 𝑗 ) = 𝐴 )
51 50 biimpi ⊢ ( 𝐴 = ( 𝑆 ‘ 𝑗 ) → ( 𝑆 ‘ 𝑗 ) = 𝐴 )
52 51 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐴 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) = 𝐴 )
53 49 52 breqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐴 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 0 ) ≤ 𝐴 )
54 53 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐴 = ( 𝑆 ‘ 𝑗 ) → ( 𝑆 ‘ 0 ) ≤ 𝐴 ) )
55 19 54 mpd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ≤ 𝐴 )
56 4 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
57 5 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
58 15 44 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ( 𝐴 [,] 𝐵 ) )
59 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ 0 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑆 ‘ 0 ) )
60 56 57 58 59 syl3anc ⊢ ( 𝜑 → 𝐴 ≤ ( 𝑆 ‘ 0 ) )
61 9 58 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ℝ )
62 61 4 letri3d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 0 ) = 𝐴 ↔ ( ( 𝑆 ‘ 0 ) ≤ 𝐴 ∧ 𝐴 ≤ ( 𝑆 ‘ 0 ) ) ) )
63 55 60 62 mpbir2and ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = 𝐴 )
64 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
65 42 64 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
66 15 65 ffvelrnd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐴 [,] 𝐵 ) )
67 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑆 ‘ 𝑁 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑆 ‘ 𝑁 ) ≤ 𝐵 )
68 56 57 66 67 syl3anc ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ≤ 𝐵 )
69 foelrn ⊢ ( ( 𝑆 : ( 0 ... 𝑁 ) –onto→ 𝑇 ∧ 𝐵 ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐵 = ( 𝑆 ‘ 𝑗 ) )
70 17 8 69 syl2anc ⊢ ( 𝜑 → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐵 = ( 𝑆 ‘ 𝑗 ) )
71 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝐵 = ( 𝑆 ‘ 𝑗 ) )
72 elfzle2 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ≤ 𝑁 )
73 72 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝑗 ≤ 𝑁 )
74 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) )
75 30 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → ( ( 0 ... 𝑁 ) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ* ) )
76 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
77 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
78 leisorel ⊢ ( ( 𝑆 Isom < , < ( ( 0 ... 𝑁 ) , 𝑇 ) ∧ ( ( 0 ... 𝑁 ) ⊆ ℝ* ∧ 𝑇 ⊆ ℝ* ) ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) ) → ( 𝑗 ≤ 𝑁 ↔ ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑁 ) ) )
79 74 75 76 77 78 syl112anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑗 ≤ 𝑁 ↔ ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑁 ) ) )
80 73 79 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → ( 𝑆 ‘ 𝑗 ) ≤ ( 𝑆 ‘ 𝑁 ) )
81 71 80 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝐵 = ( 𝑆 ‘ 𝑗 ) ) → 𝐵 ≤ ( 𝑆 ‘ 𝑁 ) )
82 81 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝐵 = ( 𝑆 ‘ 𝑗 ) → 𝐵 ≤ ( 𝑆 ‘ 𝑁 ) ) )
83 70 82 mpd ⊢ ( 𝜑 → 𝐵 ≤ ( 𝑆 ‘ 𝑁 ) )
84 9 66 sseldd ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) ∈ ℝ )
85 84 5 letri3d ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑁 ) = 𝐵 ↔ ( ( 𝑆 ‘ 𝑁 ) ≤ 𝐵 ∧ 𝐵 ≤ ( 𝑆 ‘ 𝑁 ) ) ) )
86 68 83 85 mpbir2and ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑁 ) = 𝐵 )
87 15 63 86 jca31 ⊢ ( 𝜑 → ( ( 𝑆 : ( 0 ... 𝑁 ) ⟶ ( 𝐴 [,] 𝐵 ) ∧ ( 𝑆 ‘ 0 ) = 𝐴 ) ∧ ( 𝑆 ‘ 𝑁 ) = 𝐵 ) )