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 43558

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 4009	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13334	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13187	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3926	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3926	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ)
8		0z 12260	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
9		0le0 12004	. . . . . . . . . 10 ⊢ 0 ≤ 0
10		eluz2 12517	. . . . . . . . . 10 ⊢ (0 ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0))
11	8, 8, 9, 10	mpbir3an 1339	. . . . . . . . 9 ⊢ 0 ∈ (ℤ_≥‘0)
12	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘0))
13		fourierdlem20.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14	13	nnzd 12354	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
15	13	nngt0d 11952	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
16		elfzo2 13319	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
17	12, 14, 15, 16	syl3anbrc 1341	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
18		fourierdlem20.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
19	3, 17	sselid 3915	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
20	18, 19	ffvelrnd 6944	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
21		fourierdlem20.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
22		fourierdlem20.t	. . . . . . . . . . 11 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
23	21	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
24		fourierdlem20.b	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
25	24	rexrd 10956	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		fourierdlem20.aleb	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
27		lbicc2 13125	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
28	23, 25, 26, 27	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
29		ubicc2 13126	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
30	23, 25, 26, 29	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
31	28, 30	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)))
32		prssg 4749	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
33	23, 25, 32	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
34	31, 33	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
35		inss2 4160	. . . . . . . . . . . . . 14 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossicc 13094	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
37	35, 36	sstri 3926	. . . . . . . . . . . . 13 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
39	34, 38	unssd 4116	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
40	22, 39	eqsstrid 3965	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
41	21, 24	iccssred 13095	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
42	40, 41	sstrd 3927	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
43		fourierdlem20.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44		isof1o 7174	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
45		f1of 6700	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
46	43, 44, 45	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
47		fourierdlem20.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
48		elfzofz 13331	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
50	46, 49	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇)
51	42, 50	sseldd 3918	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
52		fourierdlem20.q0	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
53	40, 50	sseldd 3918	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵))
54		iccgelb 13064	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽))
55	23, 25, 53, 54	syl3anc 1369	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽))
56	20, 21, 51, 52, 55	letrd 11062	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽))
57		fveq2 6756	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
58	57	breq1d 5080	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽)))
59	58	elrab 3617	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽)))
60	17, 56, 59	sylanbrc 582	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
61	60	ne0d 4266	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
62	13	nnred 11918	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	2	sseli 3913	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀))
64		elfzo0le 13359	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀)
66	65	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀)
67	66	ralrimiva 3107	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)
68		breq2 5074	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀))
69	68	ralbidv 3120	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀))
70	69	rspcev 3552	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
71	62, 67, 70	syl2anc 583	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
72		suprzcl 12330	. . . . 5 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
73	7, 61, 71, 72	syl3anc 1369	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
74	2, 73	sselid 3915	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
75	1, 74	eqeltrid 2843	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
76	3, 75	sselid 3915	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
77	18, 76	ffvelrnd 6944	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
78	77	rexrd 10956	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
79		fzofzp1 13412	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
80	75, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
81	18, 80	ffvelrnd 6944	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
82	81	rexrd 10956	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
83	1, 73	eqeltrid 2843	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
84		nfrab1 3310	. . . . . . . 8 ⊢ Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}
85		nfcv 2906	. . . . . . . 8 ⊢ Ⅎ𝑘ℝ
86		nfcv 2906	. . . . . . . 8 ⊢ Ⅎ𝑘 <
87	84, 85, 86	nfsup 9140	. . . . . . 7 ⊢ Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
88	1, 87	nfcxfr 2904	. . . . . 6 ⊢ Ⅎ𝑘𝐼
89		nfcv 2906	. . . . . 6 ⊢ Ⅎ𝑘(0..^𝑀)
90		nfcv 2906	. . . . . . . 8 ⊢ Ⅎ𝑘𝑄
91	90, 88	nffv 6766	. . . . . . 7 ⊢ Ⅎ𝑘(𝑄‘𝐼)
92		nfcv 2906	. . . . . . 7 ⊢ Ⅎ𝑘 ≤
93		nfcv 2906	. . . . . . 7 ⊢ Ⅎ𝑘(𝑆‘𝐽)
94	91, 92, 93	nfbr 5117	. . . . . 6 ⊢ Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽)
95		fveq2 6756	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
96	95	breq1d 5080	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
97	88, 89, 94, 96	elrabf 3613	. . . . 5 ⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
98	83, 97	sylib 217	. . . 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 13091	. . . . . . . . . 10 ⊢ (𝐴[,]𝐵) ⊆ ℝ^*
103	40, 102	sstrdi 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
104		fzofzp1 13412	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
105	47, 104	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
106	46, 105	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
107	103, 106	sseldd 3918	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
108	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
109		xrltnle 10973	. . . . . . 7 ⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
110	101, 108, 109	syl2anc 583	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
111	100, 110	mpbird 256	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
112		fzssz 13187	. . . . . 6 ⊢ (0...𝑁) ⊆ ℤ
113		f1ofo 6707	. . . . . . . . . 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 6587	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
117	18, 116	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝑄)
118	18	fdmd 6595	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
119	118	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
120	80, 119	eleqtrd 2841	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄)
121		fvelrn 6936	. . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
128	4	sseli 3913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ)
129		zre 12253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
130	76, 128, 129	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ ℝ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ)
132	131	ltp1d 11835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
133	132	adantlr 711	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
134		simplr 765	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
135	127	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
137	134, 135, 136	nltled 11055	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
138	130	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ)
139		1red 10907	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ)
140	138, 139	readdcld 10935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ)
141		elfzoelz 13316	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
142	141	zred 12355	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
143	142	ssriv 3921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0..^𝑀) ⊆ ℝ
144	2, 143	sstri 3926	. . . . . . . . . . . . . . . . . . . . . 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 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
153	152	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
154		elfzoelz 13316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155		zre 12253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ ℤ → 𝐽 ∈ ℝ)
156	47, 154, 155	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℝ)
157	156	ltp1d 11835	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 < (𝐽 + 1))
158		isorel 7177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
159	43, 49, 105, 158	syl12anc 833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
160	157, 159	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
162	40, 106	sseldd 3918	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵))
163		iccleub 13063	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
164	23, 25, 162, 163	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
165	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
166	149, 153, 150, 161, 165	ltletrd 11065	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵)
167	148, 149, 150, 151, 166	lelttrd 11063	. . . . . . . . . . . . . . . . . . . . . . . 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 13384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))))
182	173, 180, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))
183		fzval3 13384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
184	14, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
185	184	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
186	185	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
187	182, 186	eleqtrd 2841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀))
188		elfz1eq 13196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀)
190	189	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1))
191	190	fveq2d 6760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
192	172, 191	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1)))
193	169, 170, 192	lensymd 11056	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
194	193	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
195	168, 194	condan 814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀))
196		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘 +
197		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘1
198	88, 196, 197	nfov 7285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝐼 + 1)
199	90, 198	nffv 6766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1))
200	199, 92, 93	nfbr 5117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)
201		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
202	201	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
203	198, 89, 200, 202	elrabf 3613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
204	195, 151, 203	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
205		suprub 11866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
206	145, 146, 147, 204, 205	syl31anc 1371	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
207	206, 1	breqtrrdi 5112	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
208	140, 138, 207	lensymd 11056	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
209	208	adantlr 711	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
210	137, 209	syldan 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1))
211	133, 210	condan 814	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
212	81, 211	mpdan 683	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
213	21, 127, 81, 55, 212	lelttrd 11063	. . . . . . . . . . . . 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 11065	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵)
220	124, 125, 126, 214, 219	eliood 42926	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵))
221	123, 220	elind 4124	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)))
222		elun2 4107	. . . . . . . . . 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 6964	. . . . . . . 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 5096	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
230	229	adantlr 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
231	43	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
232	49	anim1i 614	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
233	232	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
234		isorel 7177	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
235	231, 233, 234	syl2anc 583	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
236	230, 235	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
237	236	adantllr 715	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
238		eqcom 2745	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
239	238	biimpi 215	. . . . . . . . . . . . . . 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 5092	. . . . . . . . . . . . 13 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
243	242	adantll 710	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
244	243	adantlr 711	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	43	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
246		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
247	105	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁))
248		isorel 7177	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
249	245, 246, 247, 248	syl12anc 833	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
250	249	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
251	244, 250	mpbird 256	. . . . . . . . . 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 3202	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
255	226, 254	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
256		ssrexv 3984	. . . . . 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 765	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
260	47, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
261	260	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
262		simprl 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
263		simprr 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
264		btwnnz 12326	. . . . . . . 8 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
265	261, 262, 263, 264	syl3anc 1369	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
266	259, 265	pm2.65da 813	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
267	266	nrexdv 3197	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
268	267	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
269	258, 268	condan 814	. . 3 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
270		ioossioo 13102	. . 3 ⊢ ((((𝑄‘𝐼) ∈ ℝ^* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ^*) ∧ ((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
271	78, 82, 99, 269, 270	syl22anc 835	. 2 ⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
272		fveq2 6756	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
273		oveq1 7262	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
274	273	fveq2d 6760	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
275	272, 274	oveq12d 7273	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
276	275	sseq2d 3949	. . 3 ⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
277	276	rspcev 3552	. 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 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 {cpr 4560 class class class wbr 5070 dom cdm 5580 ran crn 5581 Fun wfun 6412 ⟶wf 6414 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 Isom wiso 6419 (class class class)co 7255 supcsup 9129 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 ℕcn 11903 ℤcz 12249 ℤ_≥cuz 12511 (,)cioo 13008 [,]cicc 13011 ...cfz 13168 ..^cfzo 13311

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-ioo 13012 df-icc 13015 df-fz 13169 df-fzo 13312

This theorem is referenced by: fourierdlem50 43587

W3C validator