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 46142

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 4080	. . . 4 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ (0..^𝑀)
3		fzossfz 13718	. . . . . . . 8 ⊢ (0..^𝑀) ⊆ (0...𝑀)
4		fzssz 13566	. . . . . . . 8 ⊢ (0...𝑀) ⊆ ℤ
5	3, 4	sstri 3993	. . . . . . 7 ⊢ (0..^𝑀) ⊆ ℤ
6	2, 5	sstri 3993	. . . . . 6 ⊢ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ
7	6	a1i 11	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ)
8		0z 12624	. . . . . . . . . 10 ⊢ 0 ∈ ℤ
9		0le0 12367	. . . . . . . . . 10 ⊢ 0 ≤ 0
10		eluz2 12884	. . . . . . . . . 10 ⊢ (0 ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ≤ 0))
11	8, 8, 9, 10	mpbir3an 1342	. . . . . . . . 9 ⊢ 0 ∈ (ℤ_≥‘0)
12	11	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ (ℤ_≥‘0))
13		fourierdlem20.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
14	13	nnzd 12640	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ ℤ)
15	13	nngt0d 12315	. . . . . . . 8 ⊢ (𝜑 → 0 < 𝑀)
16		elfzo2 13702	. . . . . . . 8 ⊢ (0 ∈ (0..^𝑀) ↔ (0 ∈ (ℤ_≥‘0) ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀))
17	12, 14, 15, 16	syl3anbrc 1344	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0..^𝑀))
18		fourierdlem20.q	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
19	3, 17	sselid 3981	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0...𝑀))
20	18, 19	ffvelcdmd 7105	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
21		fourierdlem20.a	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℝ)
22		fourierdlem20.t	. . . . . . . . . . 11 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
23	21	rexrd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
24		fourierdlem20.b	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ)
25	24	rexrd 11311	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		fourierdlem20.aleb	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
27		lbicc2 13504	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
28	23, 25, 26, 27	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
29		ubicc2 13505	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
30	23, 25, 26, 29	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
31	28, 30	jca 511	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)))
32		prssg 4819	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
33	23, 25, 32	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∈ (𝐴[,]𝐵) ∧ 𝐵 ∈ (𝐴[,]𝐵)) ↔ {𝐴, 𝐵} ⊆ (𝐴[,]𝐵)))
34	31, 33	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ (𝐴[,]𝐵))
35		inss2 4238	. . . . . . . . . . . . . 14 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵)
36		ioossicc 13473	. . . . . . . . . . . . . 14 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
37	35, 36	sstri 3993	. . . . . . . . . . . . 13 ⊢ (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)
38	37	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
39	34, 38	unssd 4192	. . . . . . . . . . 11 ⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ (𝐴[,]𝐵))
40	22, 39	eqsstrid 4022	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ⊆ (𝐴[,]𝐵))
41	21, 24	iccssred 13474	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
42	40, 41	sstrd 3994	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ)
43		fourierdlem20.s	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇))
44		isof1o 7343	. . . . . . . . . . 11 ⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇)
45		f1of 6848	. . . . . . . . . . 11 ⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇)
46	43, 44, 45	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇)
47		fourierdlem20.j	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
48		elfzofz 13715	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
50	46, 49	ffvelcdmd 7105	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇)
51	42, 50	sseldd 3984	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
52		fourierdlem20.q0	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ≤ 𝐴)
53	40, 50	sseldd 3984	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐴[,]𝐵))
54		iccgelb 13443	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘𝐽) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑆‘𝐽))
55	23, 25, 53, 54	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≤ (𝑆‘𝐽))
56	20, 21, 51, 52, 55	letrd 11418	. . . . . . 7 ⊢ (𝜑 → (𝑄‘0) ≤ (𝑆‘𝐽))
57		fveq2 6906	. . . . . . . . 9 ⊢ (𝑘 = 0 → (𝑄‘𝑘) = (𝑄‘0))
58	57	breq1d 5153	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘0) ≤ (𝑆‘𝐽)))
59	58	elrab 3692	. . . . . . 7 ⊢ (0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ (0 ∈ (0..^𝑀) ∧ (𝑄‘0) ≤ (𝑆‘𝐽)))
60	17, 56, 59	sylanbrc 583	. . . . . 6 ⊢ (𝜑 → 0 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
61	60	ne0d 4342	. . . . 5 ⊢ (𝜑 → {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅)
62	13	nnred 12281	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℝ)
63	2	sseli 3979	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ∈ (0..^𝑀))
64		elfzo0le 13743	. . . . . . . . 9 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ≤ 𝑀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ (𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} → 𝑗 ≤ 𝑀)
66	65	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → 𝑗 ≤ 𝑀)
67	66	ralrimiva 3146	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀)
68		breq2 5147	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → (𝑗 ≤ 𝑥 ↔ 𝑗 ≤ 𝑀))
69	68	ralbidv 3178	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥 ↔ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀))
70	69	rspcev 3622	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑀) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
71	62, 67, 70	syl2anc 584	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥)
72		suprzcl 12698	. . . . 5 ⊢ (({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℤ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
73	7, 61, 71, 72	syl3anc 1373	. . . 4 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
74	2, 73	sselid 3981	. . 3 ⊢ (𝜑 → sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ) ∈ (0..^𝑀))
75	1, 74	eqeltrid 2845	. 2 ⊢ (𝜑 → 𝐼 ∈ (0..^𝑀))
76	3, 75	sselid 3981	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))
77	18, 76	ffvelcdmd 7105	. . . 4 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ)
78	77	rexrd 11311	. . 3 ⊢ (𝜑 → (𝑄‘𝐼) ∈ ℝ^*)
79		fzofzp1 13803	. . . . . 6 ⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀))
80	75, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐼 + 1) ∈ (0...𝑀))
81	18, 80	ffvelcdmd 7105	. . . 4 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ)
82	81	rexrd 11311	. . 3 ⊢ (𝜑 → (𝑄‘(𝐼 + 1)) ∈ ℝ^*)
83	1, 73	eqeltrid 2845	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
84		nfrab1 3457	. . . . . . . 8 ⊢ Ⅎ𝑘{𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}
85		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑘ℝ
86		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑘 <
87	84, 85, 86	nfsup 9491	. . . . . . 7 ⊢ Ⅎ𝑘sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < )
88	1, 87	nfcxfr 2903	. . . . . 6 ⊢ Ⅎ𝑘𝐼
89		nfcv 2905	. . . . . 6 ⊢ Ⅎ𝑘(0..^𝑀)
90		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑘𝑄
91	90, 88	nffv 6916	. . . . . . 7 ⊢ Ⅎ𝑘(𝑄‘𝐼)
92		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑘 ≤
93		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑘(𝑆‘𝐽)
94	91, 92, 93	nfbr 5190	. . . . . 6 ⊢ Ⅎ𝑘(𝑄‘𝐼) ≤ (𝑆‘𝐽)
95		fveq2 6906	. . . . . . 7 ⊢ (𝑘 = 𝐼 → (𝑄‘𝑘) = (𝑄‘𝐼))
96	95	breq1d 5153	. . . . . 6 ⊢ (𝑘 = 𝐼 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘𝐼) ≤ (𝑆‘𝐽)))
97	88, 89, 94, 96	elrabf 3688	. . . . 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 13470	. . . . . . . . . 10 ⊢ (𝐴[,]𝐵) ⊆ ℝ^*
103	40, 102	sstrdi 3996	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ⊆ ℝ^*)
104		fzofzp1 13803	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
105	47, 104	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
106	46, 105	ffvelcdmd 7105	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇)
107	103, 106	sseldd 3984	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
108	107	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑆‘(𝐽 + 1)) ∈ ℝ^*)
109		xrltnle 11328	. . . . . . 7 ⊢ (((𝑄‘(𝐼 + 1)) ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ^*) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
110	101, 108, 109	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ↔ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))))
111	100, 110	mpbird 257	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)))
112		fzssz 13566	. . . . . 6 ⊢ (0...𝑁) ⊆ ℤ
113		f1ofo 6855	. . . . . . . . . 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 6739	. . . . . . . . . . . . . 14 ⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
117	18, 116	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun 𝑄)
118	18	fdmd 6746	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝑄 = (0...𝑀))
119	118	eqcomd 2743	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0...𝑀) = dom 𝑄)
120	80, 119	eleqtrd 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐼 + 1) ∈ dom 𝑄)
121		fvelrn 7096	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑄 ∧ (𝐼 + 1) ∈ dom 𝑄) → (𝑄‘(𝐼 + 1)) ∈ ran 𝑄)
122	117, 120, 121	syl2anc 584	. . . . . . . . . . . 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 3984	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
128	4	sseli 3979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ (0...𝑀) → 𝐼 ∈ ℤ)
129		zre 12617	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
130	76, 128, 129	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐼 ∈ ℝ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 ∈ ℝ)
132	131	ltp1d 12198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
133	132	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → 𝐼 < (𝐼 + 1))
134		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ℝ)
135	127	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑆‘𝐽) ∈ ℝ)
136		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
137	134, 135, 136	nltled 11411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽))
138	130	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 𝐼 ∈ ℝ)
139		1red 11262	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → 1 ∈ ℝ)
140	138, 139	readdcld 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ ℝ)
141		elfzoelz 13699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
142	141	zred 12722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
143	142	ssriv 3987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0..^𝑀) ⊆ ℝ
144	2, 143	sstri 3993	. . . . . . . . . . . . . . . . . . . . . 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 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
153	152	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
154		elfzoelz 13699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
155		zre 12617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝐽 ∈ ℤ → 𝐽 ∈ ℝ)
156	47, 154, 155	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐽 ∈ ℝ)
157	156	ltp1d 12198	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐽 < (𝐽 + 1))
158		isorel 7346	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
159	43, 49, 105, 158	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
160	157, 159	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
161	160	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
162	40, 106	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵))
163		iccleub 13442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ (𝑆‘(𝐽 + 1)) ∈ (𝐴[,]𝐵)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
164	23, 25, 162, 163	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
165	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘(𝐽 + 1)) ≤ 𝐵)
166	149, 153, 150, 161, 165	ltletrd 11421	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝑆‘𝐽) < 𝐵)
167	148, 149, 150, 151, 166	lelttrd 11419	. . . . . . . . . . . . . . . . . . . . . . . 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 13773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑀 ∈ ℤ → (((𝐼 + 1) ∈ (0..^(𝑀 + 1)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1))))
182	173, 180, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀..^(𝑀 + 1)))
183		fzval3 13773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
184	14, 183	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝑀...𝑀) = (𝑀..^(𝑀 + 1)))
185	184	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
186	185	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑀..^(𝑀 + 1)) = (𝑀...𝑀))
187	182, 186	eleqtrd 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (𝑀...𝑀))
188		elfz1eq 13575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐼 + 1) ∈ (𝑀...𝑀) → (𝐼 + 1) = 𝑀)
189	187, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝐼 + 1) = 𝑀)
190	189	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝑀 = (𝐼 + 1))
191	190	fveq2d 6910	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → (𝑄‘𝑀) = (𝑄‘(𝐼 + 1)))
192	172, 191	breqtrd 5169	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → 𝐵 ≤ (𝑄‘(𝐼 + 1)))
193	169, 170, 192	lensymd 11412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
194	193	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) ∧ ¬ (𝐼 + 1) ∈ (0..^𝑀)) → ¬ (𝑄‘(𝐼 + 1)) < 𝐵)
195	168, 194	condan 818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ (0..^𝑀))
196		nfcv 2905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘 +
197		nfcv 2905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘1
198	88, 196, 197	nfov 7461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝐼 + 1)
199	90, 198	nffv 6916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1))
200	199, 92, 93	nfbr 5190	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑘(𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)
201		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = (𝐼 + 1) → (𝑄‘𝑘) = (𝑄‘(𝐼 + 1)))
202	201	breq1d 5153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = (𝐼 + 1) → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ↔ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
203	198, 89, 200, 202	elrabf 3688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ↔ ((𝐼 + 1) ∈ (0..^𝑀) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)))
204	195, 151, 203	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)})
205		suprub 12229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ⊆ ℝ ∧ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑗 ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}𝑗 ≤ 𝑥) ∧ (𝐼 + 1) ∈ {𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
206	145, 146, 147, 204, 205	syl31anc 1375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ sup({𝑘 ∈ (0..^𝑀) ∣ (𝑄‘𝑘) ≤ (𝑆‘𝐽)}, ℝ, < ))
207	206, 1	breqtrrdi 5185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → (𝐼 + 1) ≤ 𝐼)
208	140, 138, 207	lensymd 11412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
209	208	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ (𝑄‘(𝐼 + 1)) ≤ (𝑆‘𝐽)) → ¬ 𝐼 < (𝐼 + 1))
210	137, 209	syldan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) ∧ ¬ (𝑆‘𝐽) < (𝑄‘(𝐼 + 1))) → ¬ 𝐼 < (𝐼 + 1))
211	133, 210	condan 818	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
212	81, 211	mpdan 687	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
213	21, 127, 81, 55, 212	lelttrd 11419	. . . . . . . . . . . . 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 11421	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) < 𝐵)
220	124, 125, 126, 214, 219	eliood 45511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (𝐴(,)𝐵))
221	123, 220	elind 4200	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)))
222		elun2 4183	. . . . . . . . . 10 ⊢ ((𝑄‘(𝐼 + 1)) ∈ (ran 𝑄 ∩ (𝐴(,)𝐵)) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
223	221, 222	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))
224	223, 22	eleqtrrdi 2852	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (𝑄‘(𝐼 + 1)) ∈ 𝑇)
225		foelrn 7127	. . . . . . . 8 ⊢ ((𝑆:(0...𝑁)–onto→𝑇 ∧ (𝑄‘(𝐼 + 1)) ∈ 𝑇) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
226	115, 224, 225	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
227	212	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑄‘(𝐼 + 1)))
228		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗))
229	227, 228	breqtrd 5169	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
230	229	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗))
231	43	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
232	49	anim1i 615	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
233	232	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)))
234		isorel 7346	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
235	231, 233, 234	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗)))
236	230, 235	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
237	236	adantllr 719	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → 𝐽 < 𝑗)
238		eqcom 2744	. . . . . . . . . . . . . . . 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 5165	. . . . . . . . . . . . 13 ⊢ (((𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
243	242	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
244	243	adantlr 715	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑄‘(𝐼 + 1)) = (𝑆‘𝑗)) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))
245	43	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑆 Isom < , < ((0...𝑁), 𝑇))
246		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
247	105	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐽 + 1) ∈ (0...𝑁))
248		isorel 7346	. . . . . . . . . . . . 13 ⊢ ((𝑆 Isom < , < ((0...𝑁), 𝑇) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))))
249	245, 246, 247, 248	syl12anc 837	. . . . . . . . . . . 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 3168	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → (∃𝑗 ∈ (0...𝑁)(𝑄‘(𝐼 + 1)) = (𝑆‘𝑗) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))))
255	226, 254	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑄‘(𝐼 + 1)) < (𝑆‘(𝐽 + 1))) → ∃𝑗 ∈ (0...𝑁)(𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
256		ssrexv 4053	. . . . . 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 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 ∈ ℤ)
260	47, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ∈ ℤ)
261	260	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 ∈ ℤ)
262		simprl 771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝐽 < 𝑗)
263		simprr 773	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → 𝑗 < (𝐽 + 1))
264		btwnnz 12694	. . . . . . . 8 ⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
265	261, 262, 263, 264	syl3anc 1373	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1))) → ¬ 𝑗 ∈ ℤ)
266	259, 265	pm2.65da 817	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ ℤ) → ¬ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
267	266	nrexdv 3149	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
268	267	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1))) → ¬ ∃𝑗 ∈ ℤ (𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)))
269	258, 268	condan 818	. . 3 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))
270		ioossioo 13481	. . 3 ⊢ ((((𝑄‘𝐼) ∈ ℝ^* ∧ (𝑄‘(𝐼 + 1)) ∈ ℝ^*) ∧ ((𝑄‘𝐼) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝐼 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
271	78, 82, 99, 269, 270	syl22anc 839	. 2 ⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
272		fveq2 6906	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘𝑖) = (𝑄‘𝐼))
273		oveq1 7438	. . . . . 6 ⊢ (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
274	273	fveq2d 6910	. . . . 5 ⊢ (𝑖 = 𝐼 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝐼 + 1)))
275	272, 274	oveq12d 7449	. . . 4 ⊢ (𝑖 = 𝐼 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1))))
276	275	sseq2d 4016	. . 3 ⊢ (𝑖 = 𝐼 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝐼)(,)(𝑄‘(𝐼 + 1)))))
277	276	rspcev 3622	. 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 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 {cpr 4628 class class class wbr 5143 dom cdm 5685 ran crn 5686 Fun wfun 6555 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 supcsup 9480 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 ℕcn 12266 ℤcz 12613 ℤ_≥cuz 12878 (,)cioo 13387 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-sup 9482 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-ioo 13391 df-icc 13394 df-fz 13548 df-fzo 13695

This theorem is referenced by: fourierdlem50 46171

W3C validator