fourierdlem20 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem20 46048

Description: Every interval in the partition 𝑆 is included in an interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem20.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem20.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem20.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem20.aleb	⊢ (𝜑 → 𝐴 ≤ 𝐵)
fourierdlem20.q	⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
fourierdlem20.q0	⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
fourierdlem20.qm	⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀))
fourierdlem20.j	⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
fourierdlem20.t	⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
fourierdlem20.s	⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
fourierdlem20.i	⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )

**Assertion**
Ref	Expression
fourierdlem20	⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Distinct variable groups: 𝑖,𝐼 𝑖,𝐽 𝑘,𝐽 𝑖,𝑀 𝑘,𝑀 𝑄,𝑖 𝑄,𝑘 𝑆,𝑖 𝑆,𝑘 Allowed substitution hints: 𝜑(𝑖,𝑘) 𝐴(𝑖,𝑘) 𝐵(𝑖,𝑘) 𝑇(𝑖,𝑘) 𝐼(𝑘) 𝑁(𝑖,𝑘)

Proof of Theorem fourierdlem20 Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem20.i	. . 3 ⊢ 𝐼 = sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
2		ssrab2 4103	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13735	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13586	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 4018	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 4018	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ)
8		0z 12650	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
9		0le0 12394	. . . . . . . . . 10 ⊢ 0 ≤ 0
10		eluz2 12909	. . . . . . . . . 10 ⊢ (0 ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0))
11	8, 8, 9, 10	mpbir3an 1341	. . . . . . . . 9 ⊢ 0 ∈ (ℤ_≥‘0)
12	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘0))
13		fourierdlem20.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14	13	nnzd 12666	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
15	13	nngt0d 12342	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
16		elfzo2 13719	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
17	12, 14, 15, 16	syl3anbrc 1343	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
18		fourierdlem20.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
19	3, 17	sselid 4006	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
20	18, 19	ffvelcdmd 7119	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
21		fourierdlem20.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
22		fourierdlem20.t	. . . . . . . . . . 11 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
23	21	rexrd 11340	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
24		fourierdlem20.b	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
25	24	rexrd 11340	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		fourierdlem20.aleb	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
27		lbicc2 13524	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
28	23, 25, 26, 27	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
29		ubicc2 13525	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
30	23, 25, 26, 29	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
31	28, 30	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)))
32		prssg 4844	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
33	23, 25, 32	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
34	31, 33	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
35		inss2 4259	. . . . . . . . . . . . . 14 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossicc 13493	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
37	35, 36	sstri 4018	. . . . . . . . . . . . 13 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
39	34, 38	unssd 4215	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
40	22, 39	eqsstrid 4057	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
41	21, 24	iccssred 13494	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
42	40, 41	sstrd 4019	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
43		fourierdlem20.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44		isof1o 7359	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
45		f1of 6862	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
46	43, 44, 45	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
47		fourierdlem20.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
48		elfzofz 13732	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
50	46, 49	ffvelcdmd 7119	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇)
51	42, 50	sseldd 4009	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
52		fourierdlem20.q0	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
53	40, 50	sseldd 4009	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵))
54		iccgelb 13463	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽))
55	23, 25, 53, 54	syl3anc 1371	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽))
56	20, 21, 51, 52, 55	letrd 11447	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽))
57		fveq2 6920	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
58	57	breq1d 5176	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽)))
59	58	elrab 3708	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽)))
60	17, 56, 59	sylanbrc 582	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
61	60	ne0d 4365	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
62	13	nnred 12308	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	2	sseli 4004	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀))
64		elfzo0le 13760	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀)
66	65	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀)
67	66	ralrimiva 3152	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)
68		breq2 5170	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀))
69	68	ralbidv 3184	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀))
70	69	rspcev 3635	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
71	62, 67, 70	syl2anc 583	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
72		suprzcl 12723	. . . . 5 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
73	7, 61, 71, 72	syl3anc 1371	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
74	2, 73	sselid 4006	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
75	1, 74	eqeltrid 2848	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
76	3, 75	sselid 4006	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
77	18, 76	ffvelcdmd 7119	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
78	77	rexrd 11340	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
79		fzofzp1 13814	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
80	75, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
81	18, 80	ffvelcdmd 7119	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
82	81	rexrd 11340	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
83	1, 73	eqeltrid 2848	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
84		nfrab1 3464	. . . . . . . 8 ⊢ Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}
85		nfcv 2908	. . . . . . . 8 ⊢ Ⅎ𝑘ℝ
86		nfcv 2908	. . . . . . . 8 ⊢ Ⅎ𝑘 <
87	84, 85, 86	nfsup 9520	. . . . . . 7 ⊢ Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
88	1, 87	nfcxfr 2906	. . . . . 6 ⊢ Ⅎ𝑘𝐼
89		nfcv 2908	. . . . . 6 ⊢ Ⅎ𝑘(0..^𝑀)
90		nfcv 2908	. . . . . . . 8 ⊢ Ⅎ𝑘𝑄
91	90, 88	nffv 6930	. . . . . . 7 ⊢ Ⅎ𝑘(𝑄‘𝐼)
92		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑘 ≤
93		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑘(𝑆‘𝐽)
94	91, 92, 93	nfbr 5213	. . . . . 6 ⊢ Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽)
95		fveq2 6920	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
96	95	breq1d 5176	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
97	88, 89, 94, 96	elrabf 3704	. . . . 5 ⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
98	83, 97	sylib 218	. . . 4 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
99	98	simprd 495	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑆‘𝐽))
100		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
101	82	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
102		iccssxr 13490	. . . . . . . . . 10 ⊢ (𝐴[,]𝐵) ⊆ ℝ^*
103	40, 102	sstrdi 4021	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
104		fzofzp1 13814	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
105	47, 104	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
106	46, 105	ffvelcdmd 7119	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
107	103, 106	sseldd 4009	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
108	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
109		xrltnle 11357	. . . . . . 7 ⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
110	101, 108, 109	syl2anc 583	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
111	100, 110	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
112		fzssz 13586	. . . . . 6 ⊢ (0...𝑁) ⊆ ℤ
113		f1ofo 6869	. . . . . . . . . 10 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇)
114	43, 44, 113	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇)
115	114	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝑆:(0...𝑁)–onto→𝑇)
116		ffun 6750	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
117	18, 116	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝑄)
118	18	fdmd 6757	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
119	118	eqcomd 2746	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
120	80, 119	eleqtrd 2846	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄)
121		fvelrn 7110	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑄 ∧ (𝐼 + 1) ∈ dom 𝑄) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
122	117, 120, 121	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
123	122	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
124	23	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 ∈ ℝ^*)
125	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ^*)
126	81	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
127	41, 53	sseldd 4009	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
128	4	sseli 4004	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ)
129		zre 12643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
130	76, 128, 129	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ ℝ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ)
132	131	ltp1d 12225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
133	132	adantlr 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
134		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
135	127	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
137	134, 135, 136	nltled 11440	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
138	130	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ)
139		1red 11291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ)
140	138, 139	readdcld 11319	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ)
141		elfzoelz 13716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
142	141	zred 12747	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
143	142	ssriv 4012	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0..^𝑀) ⊆ ℝ
144	2, 143	sstri 4018	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ)
146	61	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
147	71	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
148	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
149	127	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) ∈ ℝ)
150	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐵 ∈ ℝ)
151		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
152	42, 106	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
153	152	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
154		elfzoelz 13716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155		zre 12643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ ℤ → 𝐽 ∈ ℝ)
156	47, 154, 155	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℝ)
157	156	ltp1d 12225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 < (𝐽 + 1))
158		isorel 7362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
159	43, 49, 105, 158	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
160	157, 159	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
162	40, 106	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵))
163		iccleub 13462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
164	23, 25, 162, 163	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
165	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
166	149, 153, 150, 161, 165	ltletrd 11450	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵)
167	148, 149, 150, 151, 166	lelttrd 11448	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) < 𝐵)
168	167	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) < 𝐵)
169	24	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ∈ ℝ)
170	81	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
171		fourierdlem20.qm	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀))
172	171	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘𝑀))
173	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
174	80	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0...𝑀))
175		fzval3 13785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀 ∈ ℤ → (0...𝑀) = (0..^(𝑀 + 1)))
176	14, 175	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0...𝑀) = (0..^(𝑀 + 1)))
177	176	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (0...𝑀) = (0..^(𝑀 + 1)))
178	174, 177	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0..^(𝑀 + 1)))
179		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝐼 + 1) ∈ (0..^𝑀))
180	178, 179	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)))
181		elfzonelfzo 13819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))))
182	173, 180, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))
183		fzval3 13785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
184	14, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
185	184	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
186	185	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
187	182, 186	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀))
188		elfz1eq 13595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀)
190	189	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1))
191	190	fveq2d 6924	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
192	172, 191	breqtrd 5192	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1)))
193	169, 170, 192	lensymd 11441	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
194	193	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
195	168, 194	condan 817	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀))
196		nfcv 2908	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘 +
197		nfcv 2908	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘1
198	88, 196, 197	nfov 7478	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝐼 + 1)
199	90, 198	nffv 6930	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1))
200	199, 92, 93	nfbr 5213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)
201		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
202	201	breq1d 5176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
203	198, 89, 200, 202	elrabf 3704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
204	195, 151, 203	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
205		suprub 12256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
206	145, 146, 147, 204, 205	syl31anc 1373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
207	206, 1	breqtrrdi 5208	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
208	140, 138, 207	lensymd 11441	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
209	208	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
210	137, 209	syldan 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1))
211	133, 210	condan 817	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
212	81, 211	mpdan 686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
213	21, 127, 81, 55, 212	lelttrd 11448	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < (𝑄‘(𝐼 + 1)))
214	213	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 < (𝑄‘(𝐼 + 1)))
215	152	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
216	24	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ)
217		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
218	164	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
219	126, 215, 216, 217, 218	ltletrd 11450	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵)
220	124, 125, 126, 214, 219	eliood 45416	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵))
221	123, 220	elind 4223	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)))
222		elun2 4206	. . . . . . . . . 10 ⊢ ((𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
223	221, 222	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
224	223, 22	eleqtrrdi 2855	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ 𝑇)
225		foelrn 7141	. . . . . . . 8 ⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ (𝑄‘(𝐼 + 1)) ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
226	115, 224, 225	syl2anc 583	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
227	212	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
228		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
229	227, 228	breqtrd 5192	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
230	229	adantlr 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
231	43	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
232	49	anim1i 614	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
233	232	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
234		isorel 7362	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
235	231, 233, 234	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
236	230, 235	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
237	236	adantllr 718	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
238		eqcom 2747	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
239	238	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
240	239	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
241		simpl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
242	240, 241	eqbrtrd 5188	. . . . . . . . . . . . 13 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
243	242	adantll 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
244	243	adantlr 714	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	43	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
246		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
247	105	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁))
248		isorel 7362	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
249	245, 246, 247, 248	syl12anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
250	249	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
251	244, 250	mpbird 257	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑗 < (𝐽 + 1))
252	237, 251	jca 511	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
253	252	ex 412	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
254	253	reximdva 3174	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
255	226, 254	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
256		ssrexv 4078	. . . . . 6 ⊢ ((0...𝑁) ⊆ ℤ → (∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
257	112, 255, 256	mpsyl 68	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
258	111, 257	syldan 590	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
259		simplr 768	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
260	47, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
261	260	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
262		simprl 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
263		simprr 772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
264		btwnnz 12719	. . . . . . . 8 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
265	261, 262, 263, 264	syl3anc 1371	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
266	259, 265	pm2.65da 816	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
267	266	nrexdv 3155	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
268	267	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
269	258, 268	condan 817	. . 3 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
270		ioossioo 13501	. . 3 ⊢ ((((𝑄‘𝐼) ∈ ℝ^* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ^*) ∧ ((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
271	78, 82, 99, 269, 270	syl22anc 838	. 2 ⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
272		fveq2 6920	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
273		oveq1 7455	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
274	273	fveq2d 6924	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
275	272, 274	oveq12d 7466	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
276	275	sseq2d 4041	. . 3 ⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
277	276	rspcev 3635	. 2 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	75, 271, 277	syl2anc 583	1 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∀wral 3067 ∃wrex 3076 {crab 3443 ∪ cun 3974 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 {cpr 4650 class class class wbr 5166 dom cdm 5700 ran crn 5701 Fun wfun 6567 ⟶wf 6569 –onto→wfo 6571 –1-1-onto→wf1o 6572 ‘cfv 6573 Isom wiso 6574 (class class class)co 7448 supcsup 9509 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 ℕcn 12293 ℤcz 12639 ℤ_≥cuz 12903 (,)cioo 13407 [,]cicc 13410 ...cfz 13567 ..^cfzo 13711

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-nn 12294 df-n0 12554 df-z 12640 df-uz 12904 df-ioo 13411 df-icc 13414 df-fz 13568 df-fzo 13712

This theorem is referenced by: fourierdlem50 46077

W3C validator