Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem25 Structured version   Visualization version   GIF version

Theorem fourierdlem25 43356
Description: If 𝐶 is not in the range of the partition, then it is in an open interval induced by the partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem25.m (𝜑𝑀 ∈ ℕ)
fourierdlem25.qf (𝜑𝑄:(0...𝑀)⟶ℝ)
fourierdlem25.cel (𝜑𝐶 ∈ ((𝑄‘0)[,](𝑄𝑀)))
fourierdlem25.cnel (𝜑 → ¬ 𝐶 ∈ ran 𝑄)
fourierdlem25.i 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < )
Assertion
Ref Expression
fourierdlem25 (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))))
Distinct variable groups:   𝐶,𝑘   𝐶,𝑗   𝑗,𝐼   𝑘,𝐼   𝑘,𝑀   𝑗,𝑀   𝑄,𝑘   𝑄,𝑗
Allowed substitution hints:   𝜑(𝑗,𝑘)

Proof of Theorem fourierdlem25
Dummy variables 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem25.i . . 3 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < )
2 ssrab2 3998 . . . 4 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ (0..^𝑀)
3 ltso 10918 . . . . . 6 < Or ℝ
43a1i 11 . . . . 5 (𝜑 → < Or ℝ)
5 fzofi 13552 . . . . . . 7 (0..^𝑀) ∈ Fin
6 ssfi 8856 . . . . . . 7 (((0..^𝑀) ∈ Fin ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ (0..^𝑀)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ∈ Fin)
75, 2, 6mp2an 692 . . . . . 6 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ∈ Fin
87a1i 11 . . . . 5 (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ∈ Fin)
9 0zd 12193 . . . . . . . 8 (𝜑 → 0 ∈ ℤ)
10 fourierdlem25.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
1110nnzd 12286 . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
1210nngt0d 11884 . . . . . . . 8 (𝜑 → 0 < 𝑀)
13 fzolb 13254 . . . . . . . 8 (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
149, 11, 12, 13syl3anbrc 1345 . . . . . . 7 (𝜑 → 0 ∈ (0..^𝑀))
15 fourierdlem25.qf . . . . . . . . 9 (𝜑𝑄:(0...𝑀)⟶ℝ)
16 elfzofz 13263 . . . . . . . . . 10 (0 ∈ (0..^𝑀) → 0 ∈ (0...𝑀))
1714, 16syl 17 . . . . . . . . 9 (𝜑 → 0 ∈ (0...𝑀))
1815, 17ffvelrnd 6910 . . . . . . . 8 (𝜑 → (𝑄‘0) ∈ ℝ)
1910nnnn0d 12155 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ0)
20 nn0uz 12481 . . . . . . . . . . . . 13 0 = (ℤ‘0)
2119, 20eleqtrdi 2848 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (ℤ‘0))
22 eluzfz2 13125 . . . . . . . . . . . 12 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
2321, 22syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ (0...𝑀))
2415, 23ffvelrnd 6910 . . . . . . . . . 10 (𝜑 → (𝑄𝑀) ∈ ℝ)
2518, 24iccssred 13027 . . . . . . . . 9 (𝜑 → ((𝑄‘0)[,](𝑄𝑀)) ⊆ ℝ)
26 fourierdlem25.cel . . . . . . . . 9 (𝜑𝐶 ∈ ((𝑄‘0)[,](𝑄𝑀)))
2725, 26sseldd 3907 . . . . . . . 8 (𝜑𝐶 ∈ ℝ)
2818rexrd 10888 . . . . . . . . 9 (𝜑 → (𝑄‘0) ∈ ℝ*)
2924rexrd 10888 . . . . . . . . 9 (𝜑 → (𝑄𝑀) ∈ ℝ*)
30 iccgelb 12996 . . . . . . . . 9 (((𝑄‘0) ∈ ℝ* ∧ (𝑄𝑀) ∈ ℝ*𝐶 ∈ ((𝑄‘0)[,](𝑄𝑀))) → (𝑄‘0) ≤ 𝐶)
3128, 29, 26, 30syl3anc 1373 . . . . . . . 8 (𝜑 → (𝑄‘0) ≤ 𝐶)
32 fourierdlem25.cnel . . . . . . . . . 10 (𝜑 → ¬ 𝐶 ∈ ran 𝑄)
33 simpr 488 . . . . . . . . . . 11 ((𝜑𝐶 = (𝑄‘0)) → 𝐶 = (𝑄‘0))
3415ffnd 6551 . . . . . . . . . . . . 13 (𝜑𝑄 Fn (0...𝑀))
3534adantr 484 . . . . . . . . . . . 12 ((𝜑𝐶 = (𝑄‘0)) → 𝑄 Fn (0...𝑀))
3617adantr 484 . . . . . . . . . . . 12 ((𝜑𝐶 = (𝑄‘0)) → 0 ∈ (0...𝑀))
37 fnfvelrn 6906 . . . . . . . . . . . 12 ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
3835, 36, 37syl2anc 587 . . . . . . . . . . 11 ((𝜑𝐶 = (𝑄‘0)) → (𝑄‘0) ∈ ran 𝑄)
3933, 38eqeltrd 2838 . . . . . . . . . 10 ((𝜑𝐶 = (𝑄‘0)) → 𝐶 ∈ ran 𝑄)
4032, 39mtand 816 . . . . . . . . 9 (𝜑 → ¬ 𝐶 = (𝑄‘0))
4140neqned 2947 . . . . . . . 8 (𝜑𝐶 ≠ (𝑄‘0))
4218, 27, 31, 41leneltd 10991 . . . . . . 7 (𝜑 → (𝑄‘0) < 𝐶)
43 fveq2 6722 . . . . . . . . 9 (𝑘 = 0 → (𝑄𝑘) = (𝑄‘0))
4443breq1d 5068 . . . . . . . 8 (𝑘 = 0 → ((𝑄𝑘) < 𝐶 ↔ (𝑄‘0) < 𝐶))
4544elrab 3607 . . . . . . 7 (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) < 𝐶))
4614, 42, 45sylanbrc 586 . . . . . 6 (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶})
4746ne0d 4255 . . . . 5 (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ≠ ∅)
48 fzossfz 13266 . . . . . . . 8 (0..^𝑀) ⊆ (0...𝑀)
49 fzssz 13119 . . . . . . . . 9 (0...𝑀) ⊆ ℤ
50 zssre 12188 . . . . . . . . 9 ℤ ⊆ ℝ
5149, 50sstri 3915 . . . . . . . 8 (0...𝑀) ⊆ ℝ
5248, 51sstri 3915 . . . . . . 7 (0..^𝑀) ⊆ ℝ
532, 52sstri 3915 . . . . . 6 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℝ
5453a1i 11 . . . . 5 (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℝ)
55 fisupcl 9090 . . . . 5 (( < Or ℝ ∧ ({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ∈ Fin ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ≠ ∅ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℝ)) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶})
564, 8, 47, 54, 55syl13anc 1374 . . . 4 (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶})
572, 56sseldi 3904 . . 3 (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < ) ∈ (0..^𝑀))
581, 57eqeltrid 2842 . 2 (𝜑𝐼 ∈ (0..^𝑀))
5948, 58sseldi 3904 . . . . 5 (𝜑𝐼 ∈ (0...𝑀))
6015, 59ffvelrnd 6910 . . . 4 (𝜑 → (𝑄𝐼) ∈ ℝ)
6160rexrd 10888 . . 3 (𝜑 → (𝑄𝐼) ∈ ℝ*)
62 fzofzp1 13344 . . . . . 6 (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
6358, 62syl 17 . . . . 5 (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
6415, 63ffvelrnd 6910 . . . 4 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
6564rexrd 10888 . . 3 (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ*)
661, 56eqeltrid 2842 . . . . 5 (𝜑𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶})
67 fveq2 6722 . . . . . . 7 (𝑘 = 𝐼 → (𝑄𝑘) = (𝑄𝐼))
6867breq1d 5068 . . . . . 6 (𝑘 = 𝐼 → ((𝑄𝑘) < 𝐶 ↔ (𝑄𝐼) < 𝐶))
6968elrab 3607 . . . . 5 (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄𝐼) < 𝐶))
7066, 69sylib 221 . . . 4 (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄𝐼) < 𝐶))
7170simprd 499 . . 3 (𝜑 → (𝑄𝐼) < 𝐶)
7252, 58sseldi 3904 . . . . . . . . 9 (𝜑𝐼 ∈ ℝ)
73 ltp1 11677 . . . . . . . . . 10 (𝐼 ∈ ℝ → 𝐼 < (𝐼 + 1))
74 id 22 . . . . . . . . . . 11 (𝐼 ∈ ℝ → 𝐼 ∈ ℝ)
75 peano2re 11010 . . . . . . . . . . 11 (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
7674, 75ltnled 10984 . . . . . . . . . 10 (𝐼 ∈ ℝ → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
7773, 76mpbid 235 . . . . . . . . 9 (𝐼 ∈ ℝ → ¬ (𝐼 + 1) ≤ 𝐼)
7872, 77syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
7948, 49sstri 3915 . . . . . . . . . . . 12 (0..^𝑀) ⊆ ℤ
802, 79sstri 3915 . . . . . . . . . . 11 {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℤ
8180a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℤ)
82 elrabi 3601 . . . . . . . . . . . . . . 15 ( ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} → ∈ (0..^𝑀))
83 elfzo0le 13291 . . . . . . . . . . . . . . 15 ( ∈ (0..^𝑀) → 𝑀)
8482, 83syl 17 . . . . . . . . . . . . . 14 ( ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} → 𝑀)
8584adantl 485 . . . . . . . . . . . . 13 ((𝜑 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}) → 𝑀)
8685ralrimiva 3105 . . . . . . . . . . . 12 (𝜑 → ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑀)
87 breq2 5062 . . . . . . . . . . . . . 14 (𝑚 = 𝑀 → (𝑚𝑀))
8887ralbidv 3118 . . . . . . . . . . . . 13 (𝑚 = 𝑀 → (∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑚 ↔ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑀))
8988rspcev 3542 . . . . . . . . . . . 12 ((𝑀 ∈ ℤ ∧ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑀) → ∃𝑚 ∈ ℤ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑚)
9011, 86, 89syl2anc 587 . . . . . . . . . . 11 (𝜑 → ∃𝑚 ∈ ℤ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑚)
9190adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ∃𝑚 ∈ ℤ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑚)
92 elfzuz 13113 . . . . . . . . . . . . . 14 ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ∈ (ℤ‘0))
9363, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐼 + 1) ∈ (ℤ‘0))
9493adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ (ℤ‘0))
9511adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℤ)
9651, 63sseldi 3904 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ∈ ℝ)
9796adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ ℝ)
9895zred 12287 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℝ)
99 elfzle2 13121 . . . . . . . . . . . . . . 15 ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ≤ 𝑀)
10063, 99syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝐼 + 1) ≤ 𝑀)
101100adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝑀)
102 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) < 𝐶)
10364adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
10427adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝐶 ∈ ℝ)
105103, 104ltnled 10984 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ((𝑄‘(𝐼 + 1)) < 𝐶 ↔ ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1))))
106102, 105mpbid 235 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1)))
107 iccleub 12995 . . . . . . . . . . . . . . . . . . 19 (((𝑄‘0) ∈ ℝ* ∧ (𝑄𝑀) ∈ ℝ*𝐶 ∈ ((𝑄‘0)[,](𝑄𝑀))) → 𝐶 ≤ (𝑄𝑀))
10828, 29, 26, 107syl3anc 1373 . . . . . . . . . . . . . . . . . 18 (𝜑𝐶 ≤ (𝑄𝑀))
109108adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄𝑀))
110 fveq2 6722 . . . . . . . . . . . . . . . . . 18 (𝑀 = (𝐼 + 1) → (𝑄𝑀) = (𝑄‘(𝐼 + 1)))
111110adantl 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑀 = (𝐼 + 1)) → (𝑄𝑀) = (𝑄‘(𝐼 + 1)))
112109, 111breqtrd 5084 . . . . . . . . . . . . . . . 16 ((𝜑𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1)))
113112adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1)))
114106, 113mtand 816 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝑀 = (𝐼 + 1))
115114neqned 2947 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ≠ (𝐼 + 1))
11697, 98, 101, 115leneltd 10991 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) < 𝑀)
117 elfzo2 13251 . . . . . . . . . . . 12 ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (ℤ‘0) ∧ 𝑀 ∈ ℤ ∧ (𝐼 + 1) < 𝑀))
11894, 95, 116, 117syl3anbrc 1345 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ (0..^𝑀))
119 fveq2 6722 . . . . . . . . . . . . 13 (𝑘 = (𝐼 + 1) → (𝑄𝑘) = (𝑄‘(𝐼 + 1)))
120119breq1d 5068 . . . . . . . . . . . 12 (𝑘 = (𝐼 + 1) → ((𝑄𝑘) < 𝐶 ↔ (𝑄‘(𝐼 + 1)) < 𝐶))
121120elrab 3607 . . . . . . . . . . 11 ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) < 𝐶))
122118, 102, 121sylanbrc 586 . . . . . . . . . 10 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶})
123 suprzub 12540 . . . . . . . . . 10 (({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶} ⊆ ℤ ∧ ∃𝑚 ∈ ℤ ∀ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}𝑚 ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < ))
12481, 91, 122, 123syl3anc 1373 . . . . . . . . 9 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄𝑘) < 𝐶}, ℝ, < ))
125124, 1breqtrrdi 5100 . . . . . . . 8 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝐼)
12678, 125mtand 816 . . . . . . 7 (𝜑 → ¬ (𝑄‘(𝐼 + 1)) < 𝐶)
127 eqcom 2744 . . . . . . . . . . 11 ((𝑄‘(𝐼 + 1)) = 𝐶𝐶 = (𝑄‘(𝐼 + 1)))
128127biimpi 219 . . . . . . . . . 10 ((𝑄‘(𝐼 + 1)) = 𝐶𝐶 = (𝑄‘(𝐼 + 1)))
129128adantl 485 . . . . . . . . 9 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 = (𝑄‘(𝐼 + 1)))
13034adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝑄 Fn (0...𝑀))
13163adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝐼 + 1) ∈ (0...𝑀))
132 fnfvelrn 6906 . . . . . . . . . 10 ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
133130, 131, 132syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
134129, 133eqeltrd 2838 . . . . . . . 8 ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 ∈ ran 𝑄)
13532, 134mtand 816 . . . . . . 7 (𝜑 → ¬ (𝑄‘(𝐼 + 1)) = 𝐶)
136126, 135jca 515 . . . . . 6 (𝜑 → (¬ (𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶))
137 pm4.56 989 . . . . . 6 ((¬ (𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶) ↔ ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶))
138136, 137sylib 221 . . . . 5 (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶))
13964, 27leloed 10980 . . . . 5 (𝜑 → ((𝑄‘(𝐼 + 1)) ≤ 𝐶 ↔ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶)))
140138, 139mtbird 328 . . . 4 (𝜑 → ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶)
14127, 64ltnled 10984 . . . 4 (𝜑 → (𝐶 < (𝑄‘(𝐼 + 1)) ↔ ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶))
142140, 141mpbird 260 . . 3 (𝜑𝐶 < (𝑄‘(𝐼 + 1)))
14361, 65, 27, 71, 142eliood 42719 . 2 (𝜑𝐶 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
144 fveq2 6722 . . . . 5 (𝑗 = 𝐼 → (𝑄𝑗) = (𝑄𝐼))
145 oveq1 7225 . . . . . 6 (𝑗 = 𝐼 → (𝑗 + 1) = (𝐼 + 1))
146145fveq2d 6726 . . . . 5 (𝑗 = 𝐼 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝐼 + 1)))
147144, 146oveq12d 7236 . . . 4 (𝑗 = 𝐼 → ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1))))
148147eleq2d 2823 . . 3 (𝑗 = 𝐼 → (𝐶 ∈ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))) ↔ 𝐶 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))))
149148rspcev 3542 . 2 ((𝐼 ∈ (0..^𝑀) ∧ 𝐶 ∈ ((𝑄𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))))
15058, 143, 149syl2anc 587 1 (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄𝑗)(,)(𝑄‘(𝑗 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 847   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  wss 3871  c0 4242   class class class wbr 5058   Or wor 5472  ran crn 5557   Fn wfn 6380  wf 6381  cfv 6385  (class class class)co 7218  Fincfn 8631  supcsup 9061  cr 10733  0cc0 10734  1c1 10735   + caddc 10737  *cxr 10871   < clt 10872  cle 10873  cn 11835  0cn0 12095  cz 12181  cuz 12443  (,)cioo 12940  [,]cicc 12943  ...cfz 13100  ..^cfzo 13243
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-sup 9063  df-inf 9064  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-nn 11836  df-n0 12096  df-z 12182  df-uz 12444  df-ioo 12944  df-icc 12947  df-fz 13101  df-fzo 13244
This theorem is referenced by:  fourierdlem41  43372  fourierdlem48  43378  fourierdlem49  43379  fourierdlem70  43400  fourierdlem71  43401  fourierdlem103  43433  fourierdlem104  43434
  Copyright terms: Public domain W3C validator