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 43668

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 4013	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13406	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13258	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3930	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3930	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ)
8		0z 12330	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
9		0le0 12074	. . . . . . . . . 10 ⊢ 0 ≤ 0
10		eluz2 12588	. . . . . . . . . 10 ⊢ (0 ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0))
11	8, 8, 9, 10	mpbir3an 1340	. . . . . . . . 9 ⊢ 0 ∈ (ℤ_≥‘0)
12	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘0))
13		fourierdlem20.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14	13	nnzd 12425	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
15	13	nngt0d 12022	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
16		elfzo2 13390	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
17	12, 14, 15, 16	syl3anbrc 1342	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
18		fourierdlem20.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
19	3, 17	sselid 3919	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
20	18, 19	ffvelrnd 6962	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
21		fourierdlem20.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
22		fourierdlem20.t	. . . . . . . . . . 11 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
23	21	rexrd 11025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
24		fourierdlem20.b	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
25	24	rexrd 11025	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		fourierdlem20.aleb	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
27		lbicc2 13196	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
28	23, 25, 26, 27	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
29		ubicc2 13197	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
30	23, 25, 26, 29	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
31	28, 30	jca 512	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)))
32		prssg 4752	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
33	23, 25, 32	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
34	31, 33	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
35		inss2 4163	. . . . . . . . . . . . . 14 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossicc 13165	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
37	35, 36	sstri 3930	. . . . . . . . . . . . 13 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
39	34, 38	unssd 4120	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
40	22, 39	eqsstrid 3969	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
41	21, 24	iccssred 13166	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
42	40, 41	sstrd 3931	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
43		fourierdlem20.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44		isof1o 7194	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
45		f1of 6716	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
46	43, 44, 45	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
47		fourierdlem20.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
48		elfzofz 13403	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
50	46, 49	ffvelrnd 6962	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇)
51	42, 50	sseldd 3922	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
52		fourierdlem20.q0	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
53	40, 50	sseldd 3922	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵))
54		iccgelb 13135	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽))
55	23, 25, 53, 54	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽))
56	20, 21, 51, 52, 55	letrd 11132	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽))
57		fveq2 6774	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
58	57	breq1d 5084	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽)))
59	58	elrab 3624	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽)))
60	17, 56, 59	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
61	60	ne0d 4269	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
62	13	nnred 11988	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	2	sseli 3917	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀))
64		elfzo0le 13431	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀)
66	65	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀)
67	66	ralrimiva 3103	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)
68		breq2 5078	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀))
69	68	ralbidv 3112	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀))
70	69	rspcev 3561	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
71	62, 67, 70	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
72		suprzcl 12400	. . . . 5 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
73	7, 61, 71, 72	syl3anc 1370	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
74	2, 73	sselid 3919	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
75	1, 74	eqeltrid 2843	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
76	3, 75	sselid 3919	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
77	18, 76	ffvelrnd 6962	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
78	77	rexrd 11025	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
79		fzofzp1 13484	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
80	75, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
81	18, 80	ffvelrnd 6962	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
82	81	rexrd 11025	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
83	1, 73	eqeltrid 2843	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
84		nfrab1 3317	. . . . . . . 8 ⊢ Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}
85		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑘ℝ
86		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑘 <
87	84, 85, 86	nfsup 9210	. . . . . . 7 ⊢ Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
88	1, 87	nfcxfr 2905	. . . . . 6 ⊢ Ⅎ𝑘𝐼
89		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑘(0..^𝑀)
90		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑘𝑄
91	90, 88	nffv 6784	. . . . . . 7 ⊢ Ⅎ𝑘(𝑄‘𝐼)
92		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑘 ≤
93		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑘(𝑆‘𝐽)
94	91, 92, 93	nfbr 5121	. . . . . 6 ⊢ Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽)
95		fveq2 6774	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
96	95	breq1d 5084	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
97	88, 89, 94, 96	elrabf 3620	. . . . 5 ⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
98	83, 97	sylib 217	. . . 4 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
99	98	simprd 496	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑆‘𝐽))
100		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
101	82	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
102		iccssxr 13162	. . . . . . . . . 10 ⊢ (𝐴[,]𝐵) ⊆ ℝ^*
103	40, 102	sstrdi 3933	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
104		fzofzp1 13484	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
105	47, 104	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
106	46, 105	ffvelrnd 6962	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
107	103, 106	sseldd 3922	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
108	107	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
109		xrltnle 11042	. . . . . . 7 ⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
110	101, 108, 109	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
111	100, 110	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
112		fzssz 13258	. . . . . 6 ⊢ (0...𝑁) ⊆ ℤ
113		f1ofo 6723	. . . . . . . . . 10 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇)
114	43, 44, 113	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇)
115	114	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝑆:(0...𝑁)–onto→𝑇)
116		ffun 6603	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
117	18, 116	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝑄)
118	18	fdmd 6611	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
119	118	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
120	80, 119	eleqtrd 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄)
121		fvelrn 6954	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑄 ∧ (𝐼 + 1) ∈ dom 𝑄) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
122	117, 120, 121	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
123	122	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
124	23	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 ∈ ℝ^*)
125	25	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ^*)
126	81	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
127	41, 53	sseldd 3922	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
128	4	sseli 3917	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ)
129		zre 12323	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
130	76, 128, 129	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ ℝ)
131	130	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ)
132	131	ltp1d 11905	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
133	132	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
134		simplr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
135	127	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ)
136		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
137	134, 135, 136	nltled 11125	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
138	130	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ)
139		1red 10976	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ)
140	138, 139	readdcld 11004	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ)
141		elfzoelz 13387	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
142	141	zred 12426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
143	142	ssriv 3925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0..^𝑀) ⊆ ℝ
144	2, 143	sstri 3930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ)
146	61	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
147	71	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
148	81	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
149	127	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) ∈ ℝ)
150	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐵 ∈ ℝ)
151		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
152	42, 106	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
153	152	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
154		elfzoelz 13387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155		zre 12323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ ℤ → 𝐽 ∈ ℝ)
156	47, 154, 155	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℝ)
157	156	ltp1d 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 < (𝐽 + 1))
158		isorel 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
159	43, 49, 105, 158	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
160	157, 159	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
161	160	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
162	40, 106	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵))
163		iccleub 13134	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
164	23, 25, 162, 163	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
165	164	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
166	149, 153, 150, 161, 165	ltletrd 11135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵)
167	148, 149, 150, 151, 166	lelttrd 11133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) < 𝐵)
168	167	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) < 𝐵)
169	24	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ∈ ℝ)
170	81	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
171		fourierdlem20.qm	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀))
172	171	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘𝑀))
173	14	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
174	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0...𝑀))
175		fzval3 13456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀 ∈ ℤ → (0...𝑀) = (0..^(𝑀 + 1)))
176	14, 175	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0...𝑀) = (0..^(𝑀 + 1)))
177	176	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (0...𝑀) = (0..^(𝑀 + 1)))
178	174, 177	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0..^(𝑀 + 1)))
179		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝐼 + 1) ∈ (0..^𝑀))
180	178, 179	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)))
181		elfzonelfzo 13489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))))
182	173, 180, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))
183		fzval3 13456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
184	14, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
185	184	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
186	185	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
187	182, 186	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀))
188		elfz1eq 13267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀)
190	189	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1))
191	190	fveq2d 6778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
192	172, 191	breqtrd 5100	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1)))
193	169, 170, 192	lensymd 11126	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
194	193	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
195	168, 194	condan 815	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀))
196		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘 +
197		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘1
198	88, 196, 197	nfov 7305	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝐼 + 1)
199	90, 198	nffv 6784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1))
200	199, 92, 93	nfbr 5121	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)
201		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
202	201	breq1d 5084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
203	198, 89, 200, 202	elrabf 3620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
204	195, 151, 203	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
205		suprub 11936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
206	145, 146, 147, 204, 205	syl31anc 1372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
207	206, 1	breqtrrdi 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
208	140, 138, 207	lensymd 11126	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
209	208	adantlr 712	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
210	137, 209	syldan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1))
211	133, 210	condan 815	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
212	81, 211	mpdan 684	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
213	21, 127, 81, 55, 212	lelttrd 11133	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < (𝑄‘(𝐼 + 1)))
214	213	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 < (𝑄‘(𝐼 + 1)))
215	152	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
216	24	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ)
217		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
218	164	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
219	126, 215, 216, 217, 218	ltletrd 11135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵)
220	124, 125, 126, 214, 219	eliood 43036	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵))
221	123, 220	elind 4128	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)))
222		elun2 4111	. . . . . . . . . 10 ⊢ ((𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
223	221, 222	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
224	223, 22	eleqtrrdi 2850	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ 𝑇)
225		foelrn 6982	. . . . . . . 8 ⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ (𝑄‘(𝐼 + 1)) ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
226	115, 224, 225	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
227	212	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
228		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
229	227, 228	breqtrd 5100	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
230	229	adantlr 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
231	43	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
232	49	anim1i 615	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
233	232	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
234		isorel 7197	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
235	231, 233, 234	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
236	230, 235	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
237	236	adantllr 716	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
238		eqcom 2745	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
239	238	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
240	239	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
241		simpl 483	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
242	240, 241	eqbrtrd 5096	. . . . . . . . . . . . 13 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
243	242	adantll 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
244	243	adantlr 712	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	43	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
246		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
247	105	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁))
248		isorel 7197	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
249	245, 246, 247, 248	syl12anc 834	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
250	249	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
251	244, 250	mpbird 256	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑗 < (𝐽 + 1))
252	237, 251	jca 512	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
253	252	ex 413	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
254	253	reximdva 3203	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
255	226, 254	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
256		ssrexv 3988	. . . . . 6 ⊢ ((0...𝑁) ⊆ ℤ → (∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
257	112, 255, 256	mpsyl 68	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
258	111, 257	syldan 591	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
259		simplr 766	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
260	47, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
261	260	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
262		simprl 768	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
263		simprr 770	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
264		btwnnz 12396	. . . . . . . 8 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
265	261, 262, 263, 264	syl3anc 1370	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
266	259, 265	pm2.65da 814	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
267	266	nrexdv 3198	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
268	267	adantr 481	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
269	258, 268	condan 815	. . 3 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
270		ioossioo 13173	. . 3 ⊢ ((((𝑄‘𝐼) ∈ ℝ^* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ^*) ∧ ((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
271	78, 82, 99, 269, 270	syl22anc 836	. 2 ⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
272		fveq2 6774	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
273		oveq1 7282	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
274	273	fveq2d 6778	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
275	272, 274	oveq12d 7293	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
276	275	sseq2d 3953	. . 3 ⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
277	276	rspcev 3561	. 2 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	75, 271, 277	syl2anc 584	1 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 ∪ cun 3885 ∩ cin 3886 ⊆ wss 3887 ∅c0 4256 {cpr 4563 class class class wbr 5074 dom cdm 5589 ran crn 5590 Fun wfun 6427 ⟶wf 6429 –onto→wfo 6431 –1-1-onto→wf1o 6432 ‘cfv 6433 Isom wiso 6434 (class class class)co 7275 supcsup 9199 ℝcr 10870 0cc0 10871 1c1 10872 + caddc 10874 ℝ^*cxr 11008 < clt 11009 ≤ cle 11010 ℕcn 11973 ℤcz 12319 ℤ_≥cuz 12582 (,)cioo 13079 [,]cicc 13082 ...cfz 13239 ..^cfzo 13382

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-n0 12234 df-z 12320 df-uz 12583 df-ioo 13083 df-icc 13086 df-fz 13240 df-fzo 13383

This theorem is referenced by: fourierdlem50 43697

W3C validator