fourierdlem25 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem25 40349

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.

Step	Hyp	Ref	Expression
1		fourierdlem25.i	. . 3 ⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < )
2		ssrab2 3687	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ (0..^𝑀)
3		ltso 10118	. . . . . 6 ⊢ < Or ℝ
4	3	a1i 11	. . . . 5 ⊢ (𝜑 → < Or ℝ)
5		fzofi 12773	. . . . . . 7 ⊢ (0..^𝑀) ∈ Fin
6		ssfi 8180	. . . . . . 7 ⊢ (((0..^𝑀) ∈ Fin ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ (0..^𝑀)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin)
7	5, 2, 6	mp2an 708	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin)
9		0zd 11389	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
10		fourierdlem25.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
11	10	nnzd 11481	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
12	10	nngt0d 11064	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
13		fzolb 12476	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
14	9, 11, 12, 13	syl3anbrc 1246	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
15		fourierdlem25.qf	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
16		elfzofz 12485	. . . . . . . . . 10 ⊢ (0 ∈ (0..^𝑀) → 0 ∈ (0...𝑀))
17	14, 16	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
18	15, 17	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
19	10	nnnn0d 11351	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ₀)
20		nn0uz 11722	. . . . . . . . . . . . 13 ⊢ ℕ₀ = (ℤ_≥‘0)
21	19, 20	syl6eleq 2711	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
22		eluzfz2 12349	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
24	15, 23	ffvelrnd 6360	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
25	18, 24	iccssred 39727	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) ⊆ ℝ)
26		fourierdlem25.cel	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀)))
27	25, 26	sseldd 3604	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ)
28	18	rexrd 10089	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ^*)
29	24	rexrd 10089	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ^*)
30		iccgelb 12230	. . . . . . . . 9 ⊢ (((𝑄‘0) ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ ℝ^* ∧ 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝑄‘0) ≤ 𝐶)
31	28, 29, 26, 30	syl3anc 1326	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐶)
32		fourierdlem25.cnel	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝐶 ∈ ran 𝑄)
33		simpr 477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝐶 = (𝑄‘0))
34		ffn 6045	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
35	15, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄 Fn (0...𝑀))
36	35	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝑄 Fn (0...𝑀))
37	17	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 0 ∈ (0...𝑀))
38		fnfvelrn 6356	. . . . . . . . . . . 12 ⊢ ((𝑄 Fn (0...𝑀) ∧ 0 ∈ (0...𝑀)) → (𝑄‘0) ∈ ran 𝑄)
39	36, 37, 38	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → (𝑄‘0) ∈ ran 𝑄)
40	33, 39	eqeltrd 2701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶 = (𝑄‘0)) → 𝐶 ∈ ran 𝑄)
41	32, 40	mtand 691	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐶 = (𝑄‘0))
42	41	neqned 2801	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ (𝑄‘0))
43	18, 27, 31, 42	leneltd 10191	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) < 𝐶)
44		fveq2 6191	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
45	44	breq1d 4663	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘0) < 𝐶))
46	45	elrab 3363	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) < 𝐶))
47	14, 43, 46	sylanbrc 698	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶})
48		ne0i 3921	. . . . . 6 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ≠ ∅)
49	47, 48	syl 17	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ≠ ∅)
50		fzossfz 12488	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
51		fzssz 12343	. . . . . . . . 9 ⊢ (0...𝑀) ⊆ ℤ
52		zssre 11384	. . . . . . . . 9 ⊢ ℤ ⊆ ℝ
53	51, 52	sstri 3612	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℝ
54	50, 53	sstri 3612	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℝ
55	2, 54	sstri 3612	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ
56	55	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ)
57		fisupcl 8375	. . . . 5 ⊢ (( < Or ℝ ∧ ({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ∈ Fin ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ≠ ∅ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℝ)) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶})
58	4, 8, 49, 56, 57	syl13anc 1328	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶})
59	2, 58	sseldi 3601	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ) ∈ (0..^𝑀))
60	1, 59	syl5eqel 2705	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
61	50, 60	sseldi 3601	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
62	15, 61	ffvelrnd 6360	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
63	62	rexrd 10089	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
64		fzofzp1 12565	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
65	60, 64	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
66	15, 65	ffvelrnd 6360	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
67	66	rexrd 10089	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
68	1, 58	syl5eqel 2705	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶})
69		fveq2 6191	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
70	69	breq1d 4663	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘𝐼) < 𝐶))
71	70	elrab 3363	. . . . 5 ⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) < 𝐶))
72	68, 71	sylib 208	. . . 4 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) < 𝐶))
73	72	simprd 479	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) < 𝐶)
74	54, 60	sseldi 3601	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ ℝ)
75		ltp1 10861	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → 𝐼 < (𝐼 + 1))
76		id 22	. . . . . . . . . . 11 ⊢ (𝐼 ∈ ℝ → 𝐼 ∈ ℝ)
77		peano2re 10209	. . . . . . . . . . 11 ⊢ (𝐼 ∈ ℝ → (𝐼 + 1) ∈ ℝ)
78	76, 77	ltnled 10184	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℝ → (𝐼 < (𝐼 + 1) ↔ ¬ (𝐼 + 1) ≤ 𝐼))
79	75, 78	mpbid 222	. . . . . . . . 9 ⊢ (𝐼 ∈ ℝ → ¬ (𝐼 + 1) ≤ 𝐼)
80	74, 79	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐼 + 1) ≤ 𝐼)
81	50, 51	sstri 3612	. . . . . . . . . . . 12 ⊢ (0..^𝑀) ⊆ ℤ
82	2, 81	sstri 3612	. . . . . . . . . . 11 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ
83	82	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ)
84		elrabi 3359	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} → ℎ ∈ (0..^𝑀))
85		elfzo0le 12511	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ (0..^𝑀) → ℎ ≤ 𝑀)
86	84, 85	syl 17	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} → ℎ ≤ 𝑀)
87	86	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) → ℎ ≤ 𝑀)
88	87	ralrimiva 2966	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀)
89		breq2 4657	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑀 → (ℎ ≤ 𝑚 ↔ ℎ ≤ 𝑀))
90	89	ralbidv 2986	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑀 → (∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚 ↔ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀))
91	90	rspcev 3309	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℤ ∧ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑀) → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚)
92	11, 88, 91	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚)
93	92	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚)
94		elfzuz 12338	. . . . . . . . . . . . . 14 ⊢ ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ∈ (ℤ_≥‘0))
95	65, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ (ℤ_≥‘0))
96	95	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ (ℤ_≥‘0))
97	11	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℤ)
98	53, 65	sseldi 3601	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 + 1) ∈ ℝ)
99	98	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ ℝ)
100	97	zred 11482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ∈ ℝ)
101		elfzle2 12345	. . . . . . . . . . . . . . 15 ⊢ ((𝐼 + 1) ∈ (0...𝑀) → (𝐼 + 1) ≤ 𝑀)
102	65, 101	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐼 + 1) ≤ 𝑀)
103	102	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝑀)
104		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) < 𝐶)
105	66	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
106	27	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝐶 ∈ ℝ)
107	105, 106	ltnled 10184	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ((𝑄‘(𝐼 + 1)) < 𝐶 ↔ ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1))))
108	104, 107	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝐶 ≤ (𝑄‘(𝐼 + 1)))
109		iccleub 12229	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑄‘0) ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ ℝ^* ∧ 𝐶 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐶 ≤ (𝑄‘𝑀))
110	28, 29, 26, 109	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ≤ (𝑄‘𝑀))
111	110	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘𝑀))
112		fveq2 6191	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 = (𝐼 + 1) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
113	112	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
114	111, 113	breqtrd 4679	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1)))
115	114	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) ∧ 𝑀 = (𝐼 + 1)) → 𝐶 ≤ (𝑄‘(𝐼 + 1)))
116	108, 115	mtand 691	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → ¬ 𝑀 = (𝐼 + 1))
117	116	neqned 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → 𝑀 ≠ (𝐼 + 1))
118	99, 100, 103, 117	leneltd 10191	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) < 𝑀)
119		elfzo2 12473	. . . . . . . . . . . 12 ⊢ ((𝐼 + 1) ∈ (0..^𝑀) ↔ ((𝐼 + 1) ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ (𝐼 + 1) < 𝑀))
120	96, 97, 118, 119	syl3anbrc 1246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ (0..^𝑀))
121		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
122	121	breq1d 4663	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) < 𝐶 ↔ (𝑄‘(𝐼 + 1)) < 𝐶))
123	122	elrab 3363	. . . . . . . . . . 11 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) < 𝐶))
124	120, 104, 123	sylanbrc 698	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶})
125		suprzub 11779	. . . . . . . . . 10 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶} ⊆ ℤ ∧ ∃𝑚 ∈ ℤ ∀ℎ ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}ℎ ≤ 𝑚 ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ))
126	83, 93, 124, 125	syl3anc 1326	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) < 𝐶}, ℝ, < ))
127	126, 1	syl6breqr 4695	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < 𝐶) → (𝐼 + 1) ≤ 𝐼)
128	80, 127	mtand 691	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) < 𝐶)
129		eqcom 2629	. . . . . . . . . . 11 ⊢ ((𝑄‘(𝐼 + 1)) = 𝐶 ↔ 𝐶 = (𝑄‘(𝐼 + 1)))
130	129	biimpi 206	. . . . . . . . . 10 ⊢ ((𝑄‘(𝐼 + 1)) = 𝐶 → 𝐶 = (𝑄‘(𝐼 + 1)))
131	130	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 = (𝑄‘(𝐼 + 1)))
132	35	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝑄 Fn (0...𝑀))
133	65	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝐼 + 1) ∈ (0...𝑀))
134		fnfvelrn 6356	. . . . . . . . . 10 ⊢ ((𝑄 Fn (0...𝑀) ∧ (𝐼 + 1) ∈ (0...𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
135	132, 133, 134	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
136	131, 135	eqeltrd 2701	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = 𝐶) → 𝐶 ∈ ran 𝑄)
137	32, 136	mtand 691	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) = 𝐶)
138	128, 137	jca 554	. . . . . 6 ⊢ (𝜑 → (¬ (𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶))
139		pm4.56 516	. . . . . 6 ⊢ ((¬ (𝑄‘(𝐼 + 1)) < 𝐶 ∧ ¬ (𝑄‘(𝐼 + 1)) = 𝐶) ↔ ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶))
140	138, 139	sylib 208	. . . . 5 ⊢ (𝜑 → ¬ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶))
141	66, 27	leloed 10180	. . . . 5 ⊢ (𝜑 → ((𝑄‘(𝐼 + 1)) ≤ 𝐶 ↔ ((𝑄‘(𝐼 + 1)) < 𝐶 ∨ (𝑄‘(𝐼 + 1)) = 𝐶)))
142	140, 141	mtbird 315	. . . 4 ⊢ (𝜑 → ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶)
143	27, 66	ltnled 10184	. . . 4 ⊢ (𝜑 → (𝐶 < (𝑄‘(𝐼 + 1)) ↔ ¬ (𝑄‘(𝐼 + 1)) ≤ 𝐶))
144	142, 143	mpbird 247	. . 3 ⊢ (𝜑 → 𝐶 < (𝑄‘(𝐼 + 1)))
145	63, 67, 27, 73, 144	eliood 39720	. 2 ⊢ (𝜑 → 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
146		fveq2 6191	. . . . 5 ⊢ (𝑗 = 𝐼 → (𝑄‘𝑗) = (𝑄‘𝐼))
147		oveq1 6657	. . . . . 6 ⊢ (𝑗 = 𝐼 → (𝑗 + 1) = (𝐼 + 1))
148	147	fveq2d 6195	. . . . 5 ⊢ (𝑗 = 𝐼 → (𝑄‘(𝑗 + 1)) = (𝑄‘(𝐼 + 1)))
149	146, 148	oveq12d 6668	. . . 4 ⊢ (𝑗 = 𝐼 → ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
150	149	eleq2d 2687	. . 3 ⊢ (𝑗 = 𝐼 → (𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))) ↔ 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
151	150	rspcev 3309	. 2 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐶 ∈ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))))
152	60, 145, 151	syl2anc 693	1 ⊢ (𝜑 → ∃𝑗 ∈ (0..^𝑀)𝐶 ∈ ((𝑄‘𝑗)(,)(𝑄‘(𝑗 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∨ wo 383 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 {crab 2916 ⊆ wss 3574 ∅c0 3915 class class class wbr 4653 Or wor 5034 ran crn 5115 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 supcsup 8346 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 ℕcn 11020 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 (,)cioo 12175 [,]cicc 12178 ...cfz 12326 ..^cfzo 12465

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-ioo 12179 df-icc 12182 df-fz 12327 df-fzo 12466

This theorem is referenced by: fourierdlem41 40365 fourierdlem48 40371 fourierdlem49 40372 fourierdlem70 40393 fourierdlem71 40394 fourierdlem103 40426 fourierdlem104 40427

W3C validator