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 42419

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 4058	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13059	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 12912	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3978	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3978	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ)
8		0z 11995	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
9		0le0 11741	. . . . . . . . . 10 ⊢ 0 ≤ 0
10		eluz2 12252	. . . . . . . . . 10 ⊢ (0 ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0))
11	8, 8, 9, 10	mpbir3an 1337	. . . . . . . . 9 ⊢ 0 ∈ (ℤ_≥‘0)
12	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘0))
13		fourierdlem20.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14	13	nnzd 12089	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
15	13	nngt0d 11689	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
16		elfzo2 13044	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
17	12, 14, 15, 16	syl3anbrc 1339	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
18		fourierdlem20.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
19	3, 17	sseldi 3967	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
20	18, 19	ffvelrnd 6854	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
21		fourierdlem20.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
22		fourierdlem20.t	. . . . . . . . . . 11 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
23	21	rexrd 10693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
24		fourierdlem20.b	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
25	24	rexrd 10693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		fourierdlem20.aleb	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
27		lbicc2 12855	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
28	23, 25, 26, 27	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
29		ubicc2 12856	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
30	23, 25, 26, 29	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
31	28, 30	jca 514	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)))
32		prssg 4754	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
33	23, 25, 32	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
34	31, 33	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
35		inss2 4208	. . . . . . . . . . . . . 14 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossicc 12825	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
37	35, 36	sstri 3978	. . . . . . . . . . . . 13 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
39	34, 38	unssd 4164	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
40	22, 39	eqsstrid 4017	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
41	21, 24	iccssred 41787	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
42	40, 41	sstrd 3979	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
43		fourierdlem20.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44		isof1o 7078	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
45		f1of 6617	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
46	43, 44, 45	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
47		fourierdlem20.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
48		elfzofz 13056	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
50	46, 49	ffvelrnd 6854	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇)
51	42, 50	sseldd 3970	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
52		fourierdlem20.q0	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
53	40, 50	sseldd 3970	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵))
54		iccgelb 12796	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽))
55	23, 25, 53, 54	syl3anc 1367	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽))
56	20, 21, 51, 52, 55	letrd 10799	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽))
57		fveq2 6672	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
58	57	breq1d 5078	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽)))
59	58	elrab 3682	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽)))
60	17, 56, 59	sylanbrc 585	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
61	60	ne0d 4303	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
62	13	nnred 11655	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	2	sseli 3965	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀))
64		elfzo0le 13084	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀)
66	65	adantl 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀)
67	66	ralrimiva 3184	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)
68		breq2 5072	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀))
69	68	ralbidv 3199	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀))
70	69	rspcev 3625	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
71	62, 67, 70	syl2anc 586	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
72		suprzcl 12065	. . . . 5 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
73	7, 61, 71, 72	syl3anc 1367	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
74	2, 73	sseldi 3967	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
75	1, 74	eqeltrid 2919	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
76	3, 75	sseldi 3967	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
77	18, 76	ffvelrnd 6854	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
78	77	rexrd 10693	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
79		fzofzp1 13137	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
80	75, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
81	18, 80	ffvelrnd 6854	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
82	81	rexrd 10693	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
83	1, 73	eqeltrid 2919	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
84		nfrab1 3386	. . . . . . . 8 ⊢ Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}
85		nfcv 2979	. . . . . . . 8 ⊢ Ⅎ𝑘ℝ
86		nfcv 2979	. . . . . . . 8 ⊢ Ⅎ𝑘 <
87	84, 85, 86	nfsup 8917	. . . . . . 7 ⊢ Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
88	1, 87	nfcxfr 2977	. . . . . 6 ⊢ Ⅎ𝑘𝐼
89		nfcv 2979	. . . . . 6 ⊢ Ⅎ𝑘(0..^𝑀)
90		nfcv 2979	. . . . . . . 8 ⊢ Ⅎ𝑘𝑄
91	90, 88	nffv 6682	. . . . . . 7 ⊢ Ⅎ𝑘(𝑄‘𝐼)
92		nfcv 2979	. . . . . . 7 ⊢ Ⅎ𝑘 ≤
93		nfcv 2979	. . . . . . 7 ⊢ Ⅎ𝑘(𝑆‘𝐽)
94	91, 92, 93	nfbr 5115	. . . . . 6 ⊢ Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽)
95		fveq2 6672	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
96	95	breq1d 5078	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
97	88, 89, 94, 96	elrabf 3678	. . . . 5 ⊢ (𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
98	83, 97	sylib 220	. . . 4 ⊢ (𝜑 → (𝐼 ∈ (0..^𝑀) ∧ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
99	98	simprd 498	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ≤ (𝑆‘𝐽))
100		simpr 487	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
101	82	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
102		iccssxr 12822	. . . . . . . . . 10 ⊢ (𝐴[,]𝐵) ⊆ ℝ^*
103	40, 102	sstrdi 3981	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
104		fzofzp1 13137	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
105	47, 104	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
106	46, 105	ffvelrnd 6854	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
107	103, 106	sseldd 3970	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
108	107	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
109		xrltnle 10710	. . . . . . 7 ⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
110	101, 108, 109	syl2anc 586	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
111	100, 110	mpbird 259	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
112		fzssz 12912	. . . . . 6 ⊢ (0...𝑁) ⊆ ℤ
113		f1ofo 6624	. . . . . . . . . 10 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)–onto→𝑇)
114	43, 44, 113	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝑇)
115	114	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝑆:(0...𝑁)–onto→𝑇)
116		ffun 6519	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
117	18, 116	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝑄)
118	18	fdmd 6525	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
119	118	eqcomd 2829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
120	80, 119	eleqtrd 2917	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄)
121		fvelrn 6846	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑄 ∧ (𝐼 + 1) ∈ dom 𝑄) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
122	117, 120, 121	syl2anc 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
123	122	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
124	23	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 ∈ ℝ^*)
125	25	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ^*)
126	81	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
127	41, 53	sseldd 3970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
128	4	sseli 3965	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ)
129		zre 11988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
130	76, 128, 129	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ ℝ)
131	130	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ)
132	131	ltp1d 11572	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
133	132	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
134		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
135	127	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ)
136		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
137	134, 135, 136	nltled 10792	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
138	130	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ)
139		1red 10644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ)
140	138, 139	readdcld 10672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ)
141		elfzoelz 13041	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
142	141	zred 12090	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
143	142	ssriv 3973	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0..^𝑀) ⊆ ℝ
144	2, 143	sstri 3978	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ)
146	61	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
147	71	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
148	81	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
149	127	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) ∈ ℝ)
150	24	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐵 ∈ ℝ)
151		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
152	42, 106	sseldd 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
153	152	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
154		elfzoelz 13041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155		zre 11988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ ℤ → 𝐽 ∈ ℝ)
156	47, 154, 155	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℝ)
157	156	ltp1d 11572	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 < (𝐽 + 1))
158		isorel 7081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
159	43, 49, 105, 158	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
160	157, 159	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
161	160	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
162	40, 106	sseldd 3970	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵))
163		iccleub 12795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
164	23, 25, 162, 163	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
165	164	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
166	149, 153, 150, 161, 165	ltletrd 10802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵)
167	148, 149, 150, 151, 166	lelttrd 10800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑄‘(𝐼 + 1)) < 𝐵)
168	167	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) < 𝐵)
169	24	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ∈ ℝ)
170	81	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
171		fourierdlem20.qm	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀))
172	171	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘𝑀))
173	14	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 ∈ ℤ)
174	80	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0...𝑀))
175		fzval3 13109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑀 ∈ ℤ → (0...𝑀) = (0..^(𝑀 + 1)))
176	14, 175	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (0...𝑀) = (0..^(𝑀 + 1)))
177	176	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (0...𝑀) = (0..^(𝑀 + 1)))
178	174, 177	eleqtrd 2917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0..^(𝑀 + 1)))
179		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝐼 + 1) ∈ (0..^𝑀))
180	178, 179	jca 514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)))
181		elfzonelfzo 13142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))))
182	173, 180, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))
183		fzval3 13109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
184	14, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
185	184	eqcomd 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
186	185	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
187	182, 186	eleqtrd 2917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀))
188		elfz1eq 12921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀)
190	189	eqcomd 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1))
191	190	fveq2d 6676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
192	172, 191	breqtrd 5094	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1)))
193	169, 170, 192	lensymd 10793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
194	193	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
195	168, 194	condan 816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀))
196		nfcv 2979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘 +
197		nfcv 2979	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘1
198	88, 196, 197	nfov 7188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝐼 + 1)
199	90, 198	nffv 6682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1))
200	199, 92, 93	nfbr 5115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)
201		fveq2 6672	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
202	201	breq1d 5078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
203	198, 89, 200, 202	elrabf 3678	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
204	195, 151, 203	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
205		suprub 11604	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
206	145, 146, 147, 204, 205	syl31anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
207	206, 1	breqtrrdi 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
208	140, 138, 207	lensymd 10793	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
209	208	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
210	137, 209	syldan 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1))
211	133, 210	condan 816	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
212	81, 211	mpdan 685	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
213	21, 127, 81, 55, 212	lelttrd 10800	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 < (𝑄‘(𝐼 + 1)))
214	213	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐴 < (𝑄‘(𝐼 + 1)))
215	152	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
216	24	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → 𝐵 ∈ ℝ)
217		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
218	164	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
219	126, 215, 216, 217, 218	ltletrd 10802	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵)
220	124, 125, 126, 214, 219	eliood 41780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵))
221	123, 220	elind 4173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)))
222		elun2 4155	. . . . . . . . . 10 ⊢ ((𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
223	221, 222	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
224	223, 22	eleqtrrdi 2926	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ 𝑇)
225		foelrn 6874	. . . . . . . 8 ⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ (𝑄‘(𝐼 + 1)) ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
226	115, 224, 225	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
227	212	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
228		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
229	227, 228	breqtrd 5094	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
230	229	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
231	43	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
232	49	anim1i 616	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
233	232	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
234		isorel 7081	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
235	231, 233, 234	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
236	230, 235	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
237	236	adantllr 717	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
238		eqcom 2830	. . . . . . . . . . . . . . . 16 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
239	238	biimpi 218	. . . . . . . . . . . . . . 15 ⊢ ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
240	239	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) = (𝑄‘(𝐼 + 1)))
241		simpl 485	. . . . . . . . . . . . . 14 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
242	240, 241	eqbrtrd 5090	. . . . . . . . . . . . 13 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
243	242	adantll 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
244	243	adantlr 713	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	43	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
246		simpr 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
247	105	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁))
248		isorel 7081	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
249	245, 246, 247, 248	syl12anc 834	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
250	249	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
251	244, 250	mpbird 259	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑗 < (𝐽 + 1))
252	237, 251	jca 514	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
253	252	ex 415	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
254	253	reximdva 3276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
255	226, 254	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
256		ssrexv 4036	. . . . . 6 ⊢ ((0...𝑁) ⊆ ℤ → (∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
257	112, 255, 256	mpsyl 68	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
258	111, 257	syldan 593	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
259		simplr 767	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
260	47, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
261	260	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
262		simprl 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
263		simprr 771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
264		btwnnz 12061	. . . . . . . 8 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
265	261, 262, 263, 264	syl3anc 1367	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
266	259, 265	pm2.65da 815	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
267	266	nrexdv 3272	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
268	267	adantr 483	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
269	258, 268	condan 816	. . 3 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
270		ioossioo 12832	. . 3 ⊢ ((((𝑄‘𝐼) ∈ ℝ^* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ^*) ∧ ((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
271	78, 82, 99, 269, 270	syl22anc 836	. 2 ⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
272		fveq2 6672	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
273		oveq1 7165	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
274	273	fveq2d 6676	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
275	272, 274	oveq12d 7176	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
276	275	sseq2d 4001	. . 3 ⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
277	276	rspcev 3625	. 2 ⊢ ((𝐼 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))) → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
278	75, 271, 277	syl2anc 586	1 ⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 ∃wrex 3141 {crab 3144 ∪ cun 3936 ∩ cin 3937 ⊆ wss 3938 ∅c0 4293 {cpr 4571 class class class wbr 5068 dom cdm 5557 ran crn 5558 Fun wfun 6351 ⟶wf 6353 –onto→wfo 6355 –1-1-onto→wf1o 6356 ‘cfv 6357 Isom wiso 6358 (class class class)co 7158 supcsup 8906 ℝcr 10538 0cc0 10539 1c1 10540 + caddc 10542 ℝ^*cxr 10676 < clt 10677 ≤ cle 10678 ℕcn 11640 ℤcz 11984 ℤ_≥cuz 12246 (,)cioo 12741 [,]cicc 12744 ...cfz 12895 ..^cfzo 13036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-isom 6366 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-sup 8908 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-nn 11641 df-n0 11901 df-z 11985 df-uz 12247 df-ioo 12745 df-icc 12748 df-fz 12896 df-fzo 13037

This theorem is referenced by: fourierdlem50 42448

W3C validator