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

Theorem fourierdlem31 45154
Description: If 𝐴 is finite and for any element in 𝐴 there is a number 𝑚 such that a property holds for all numbers larger than 𝑚, then there is a number 𝑛 such that the property holds for all numbers larger than 𝑛 and for all elements in 𝐴. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 29-Sep-2020.)
Hypotheses
Ref Expression
fourierdlem31.i 𝑖𝜑
fourierdlem31.r 𝑟𝜑
fourierdlem31.iv 𝑖𝑉
fourierdlem31.a (𝜑𝐴 ∈ Fin)
fourierdlem31.exm (𝜑 → ∀𝑖𝐴𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
fourierdlem31.m 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
fourierdlem31.v 𝑉 = (𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
fourierdlem31.n 𝑁 = sup(ran 𝑉, ℝ, < )
Assertion
Ref Expression
fourierdlem31 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
Distinct variable groups:   𝐴,𝑖,𝑚,𝑟   𝐴,𝑛,𝑖,𝑟   𝑛,𝑁   𝜒,𝑚   𝜒,𝑛
Allowed substitution hints:   𝜑(𝑖,𝑚,𝑛,𝑟)   𝜒(𝑖,𝑟)   𝑀(𝑖,𝑚,𝑛,𝑟)   𝑁(𝑖,𝑚,𝑟)   𝑉(𝑖,𝑚,𝑛,𝑟)

Proof of Theorem fourierdlem31
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1nn 12228 . . . 4 1 ∈ ℕ
2 rzal 4509 . . . . 5 (𝐴 = ∅ → ∀𝑖𝐴 𝜒)
32ralrimivw 3149 . . . 4 (𝐴 = ∅ → ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒)
4 oveq1 7419 . . . . . 6 (𝑛 = 1 → (𝑛(,)+∞) = (1(,)+∞))
54raleqdv 3324 . . . . 5 (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒))
65rspcev 3613 . . . 4 ((1 ∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
71, 3, 6sylancr 586 . . 3 (𝐴 = ∅ → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
87adantl 481 . 2 ((𝜑𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
9 fourierdlem31.n . . . 4 𝑁 = sup(ran 𝑉, ℝ, < )
10 fourierdlem31.i . . . . . . 7 𝑖𝜑
11 fourierdlem31.v . . . . . . 7 𝑉 = (𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
12 fourierdlem31.m . . . . . . . . . 10 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
1312a1i 11 . . . . . . . . 9 ((𝜑𝑖𝐴) → 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
1413infeq1d 9475 . . . . . . . 8 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ))
15 ssrab2 4078 . . . . . . . . 9 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ
16 nnuz 12870 . . . . . . . . . . 11 ℕ = (ℤ‘1)
1715, 16sseqtri 4019 . . . . . . . . . 10 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1)
18 fourierdlem31.exm . . . . . . . . . . . 12 (𝜑 → ∀𝑖𝐴𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
1918r19.21bi 3247 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
20 rabn0 4386 . . . . . . . . . . 11 ({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
2119, 20sylibr 233 . . . . . . . . . 10 ((𝜑𝑖𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅)
22 infssuzcl 12921 . . . . . . . . . 10 (({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1) ∧ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2317, 21, 22sylancr 586 . . . . . . . . 9 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2415, 23sselid 3981 . . . . . . . 8 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ ℕ)
2514, 24eqeltrd 2832 . . . . . . 7 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℕ)
2610, 11, 25rnmptssd 44195 . . . . . 6 (𝜑 → ran 𝑉 ⊆ ℕ)
2726adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ)
28 ltso 11299 . . . . . . 7 < Or ℝ
2928a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or ℝ)
30 fourierdlem31.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
31 mptfi 9354 . . . . . . . . . 10 (𝐴 ∈ Fin → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3230, 31syl 17 . . . . . . . . 9 (𝜑 → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3311, 32eqeltrid 2836 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
34 rnfi 9338 . . . . . . . 8 (𝑉 ∈ Fin → ran 𝑉 ∈ Fin)
3533, 34syl 17 . . . . . . 7 (𝜑 → ran 𝑉 ∈ Fin)
3635adantr 480 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin)
37 neqne 2947 . . . . . . . . 9 𝐴 = ∅ → 𝐴 ≠ ∅)
38 n0 4347 . . . . . . . . 9 (𝐴 ≠ ∅ ↔ ∃𝑖 𝑖𝐴)
3937, 38sylib 217 . . . . . . . 8 𝐴 = ∅ → ∃𝑖 𝑖𝐴)
4039adantl 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖𝐴)
41 nfv 1916 . . . . . . . . 9 𝑖 ¬ 𝐴 = ∅
4210, 41nfan 1901 . . . . . . . 8 𝑖(𝜑 ∧ ¬ 𝐴 = ∅)
43 fourierdlem31.iv . . . . . . . . . 10 𝑖𝑉
4443nfrn 5952 . . . . . . . . 9 𝑖ran 𝑉
45 nfcv 2902 . . . . . . . . 9 𝑖
4644, 45nfne 3042 . . . . . . . 8 𝑖ran 𝑉 ≠ ∅
47 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → 𝑖𝐴)
4811elrnmpt1 5958 . . . . . . . . . . . 12 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
4947, 25, 48syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
5049ne0d 4336 . . . . . . . . . 10 ((𝜑𝑖𝐴) → ran 𝑉 ≠ ∅)
5150ex 412 . . . . . . . . 9 (𝜑 → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5251adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5342, 46, 52exlimd 2210 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖𝐴 → ran 𝑉 ≠ ∅))
5440, 53mpd 15 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅)
55 nnssre 12221 . . . . . . 7 ℕ ⊆ ℝ
5627, 55sstrdi 3995 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ)
57 fisupcl 9467 . . . . . 6 (( < Or ℝ ∧ (ran 𝑉 ∈ Fin ∧ ran 𝑉 ≠ ∅ ∧ ran 𝑉 ⊆ ℝ)) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
5829, 36, 54, 56, 57syl13anc 1371 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
5927, 58sseldd 3984 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ℕ)
609, 59eqeltrid 2836 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ)
61 fourierdlem31.r . . . . 5 𝑟𝜑
62 nfcv 2902 . . . . . . . . . . . 12 𝑖
63 nfcv 2902 . . . . . . . . . . . 12 𝑖 <
6444, 62, 63nfsup 9449 . . . . . . . . . . 11 𝑖sup(ran 𝑉, ℝ, < )
659, 64nfcxfr 2900 . . . . . . . . . 10 𝑖𝑁
66 nfcv 2902 . . . . . . . . . 10 𝑖(,)
67 nfcv 2902 . . . . . . . . . 10 𝑖+∞
6865, 66, 67nfov 7442 . . . . . . . . 9 𝑖(𝑁(,)+∞)
6968nfcri 2889 . . . . . . . 8 𝑖 𝑟 ∈ (𝑁(,)+∞)
7010, 69nfan 1901 . . . . . . 7 𝑖(𝜑𝑟 ∈ (𝑁(,)+∞))
7111fvmpt2 7010 . . . . . . . . . . . . . 14 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7247, 25, 71syl2anc 583 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7325nnxrd 44283 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℝ*)
7472, 73eqeltrd 2832 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ*)
7574adantr 480 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ*)
76 pnfxr 11273 . . . . . . . . . . . 12 +∞ ∈ ℝ*
7776a1i 11 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈ ℝ*)
78 elioore 13359 . . . . . . . . . . . 12 (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ)
7978adantl 481 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ)
8072, 25eqeltrd 2832 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℕ)
8180nnred 12232 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ)
8281adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ)
83 ne0i 4335 . . . . . . . . . . . . . . . . 17 (𝑖𝐴𝐴 ≠ ∅)
8483adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐴) → 𝐴 ≠ ∅)
8584neneqd 2944 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ¬ 𝐴 = ∅)
8685, 60syldan 590 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → 𝑁 ∈ ℕ)
8786nnred 12232 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → 𝑁 ∈ ℝ)
8887adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ)
8985, 56syldan 590 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ran 𝑉 ⊆ ℝ)
9026, 55sstrdi 3995 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑉 ⊆ ℝ)
91 fimaxre2 12164 . . . . . . . . . . . . . . . . 17 ((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9290, 35, 91syl2anc 583 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9392adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9472, 49eqeltrd 2832 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ran 𝑉)
95 suprub 12180 . . . . . . . . . . . . . . 15 (((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥) ∧ (𝑉𝑖) ∈ ran 𝑉) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
9689, 50, 93, 94, 95syl31anc 1372 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
9796, 9breqtrrdi 5191 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ 𝑁)
9897adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ≤ 𝑁)
9988rexrd 11269 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ*)
100 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞))
101 ioogtlb 44508 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
10299, 77, 100, 101syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
10382, 88, 79, 98, 102lelttrd 11377 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) < 𝑟)
10479ltpnfd 13106 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞)
10575, 77, 79, 103, 104eliood 44511 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉𝑖)(,)+∞))
10614, 23eqeltrd 2832 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
10772, 106eqeltrd 2832 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
108 nfcv 2902 . . . . . . . . . . . . . . . . . 18 𝑚𝐴
109 nfrab1 3450 . . . . . . . . . . . . . . . . . . . 20 𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
11012, 109nfcxfr 2900 . . . . . . . . . . . . . . . . . . 19 𝑚𝑀
111 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑚
112 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑚 <
113110, 111, 112nfinf 9480 . . . . . . . . . . . . . . . . . 18 𝑚inf(𝑀, ℝ, < )
114108, 113nfmpt 5256 . . . . . . . . . . . . . . . . 17 𝑚(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
11511, 114nfcxfr 2900 . . . . . . . . . . . . . . . 16 𝑚𝑉
116 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑚𝑖
117115, 116nffv 6902 . . . . . . . . . . . . . . 15 𝑚(𝑉𝑖)
118117, 109nfel 2916 . . . . . . . . . . . . . . . 16 𝑚(𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
119117nfel1 2918 . . . . . . . . . . . . . . . . 17 𝑚(𝑉𝑖) ∈ ℕ
120 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑚(,)
121 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑚+∞
122117, 120, 121nfov 7442 . . . . . . . . . . . . . . . . . 18 𝑚((𝑉𝑖)(,)+∞)
123 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑚𝜒
124122, 123nfralw 3307 . . . . . . . . . . . . . . . . 17 𝑚𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒
125119, 124nfan 1901 . . . . . . . . . . . . . . . 16 𝑚((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
126118, 125nfbi 1905 . . . . . . . . . . . . . . 15 𝑚((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
127 eleq1 2820 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}))
128 eleq1 2820 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (𝑚 ∈ ℕ ↔ (𝑉𝑖) ∈ ℕ))
129 oveq1 7419 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑉𝑖) → (𝑚(,)+∞) = ((𝑉𝑖)(,)+∞))
130 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑟(𝑚(,)+∞)
131 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟𝐴
132 nfra1 3280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟𝑟 ∈ (𝑚(,)+∞)𝜒
133 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟
134132, 133nfrabw 3467 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
13512, 134nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟𝑀
136 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟
137 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟 <
138135, 136, 137nfinf 9480 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟inf(𝑀, ℝ, < )
139131, 138nfmpt 5256 . . . . . . . . . . . . . . . . . . . . . 22 𝑟(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
14011, 139nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑉
141 nfcv 2902 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑖
142140, 141nffv 6902 . . . . . . . . . . . . . . . . . . . 20 𝑟(𝑉𝑖)
143 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑟(,)
144 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑟+∞
145142, 143, 144nfov 7442 . . . . . . . . . . . . . . . . . . 19 𝑟((𝑉𝑖)(,)+∞)
146130, 145raleqf 3348 . . . . . . . . . . . . . . . . . 18 ((𝑚(,)+∞) = ((𝑉𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
147129, 146syl 17 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
148128, 147anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
149127, 148bibi12d 344 . . . . . . . . . . . . . . 15 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))))
150 rabid 3451 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒))
151117, 126, 149, 150vtoclgf 3555 . . . . . . . . . . . . . 14 ((𝑉𝑖) ∈ ℕ → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
15280, 151syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
153107, 152mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
154153simprd 495 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
155154r19.21bi 3247 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ ((𝑉𝑖)(,)+∞)) → 𝜒)
156105, 155syldan 590 . . . . . . . . 9 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒)
157156an32s 649 . . . . . . . 8 (((𝜑𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖𝐴) → 𝜒)
158157ex 412 . . . . . . 7 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → (𝑖𝐴𝜒))
15970, 158ralrimi 3253 . . . . . 6 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖𝐴 𝜒)
160159ex 412 . . . . 5 (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖𝐴 𝜒))
16161, 160ralrimi 3253 . . . 4 (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
162161adantr 480 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
163 oveq1 7419 . . . . 5 (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞))
164 nfcv 2902 . . . . . 6 𝑟(𝑛(,)+∞)
165140nfrn 5952 . . . . . . . . 9 𝑟ran 𝑉
166165, 136, 137nfsup 9449 . . . . . . . 8 𝑟sup(ran 𝑉, ℝ, < )
1679, 166nfcxfr 2900 . . . . . . 7 𝑟𝑁
168167, 143, 144nfov 7442 . . . . . 6 𝑟(𝑁(,)+∞)
169164, 168raleqf 3348 . . . . 5 ((𝑛(,)+∞) = (𝑁(,)+∞) → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
170163, 169syl 17 . . . 4 (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
171170rspcev 3613 . . 3 ((𝑁 ∈ ℕ ∧ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
17260, 162, 171syl2anc 583 . 2 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
1738, 172pm2.61dan 810 1 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1540  wex 1780  wnf 1784  wcel 2105  wnfc 2882  wne 2939  wral 3060  wrex 3069  {crab 3431  wss 3949  c0 4323   class class class wbr 5149  cmpt 5232   Or wor 5588  ran crn 5678  cfv 6544  (class class class)co 7412  Fincfn 8942  supcsup 9438  infcinf 9439  cr 11112  1c1 11114  +∞cpnf 11250  *cxr 11252   < clt 11253  cle 11254  cn 12217  cuz 12827  (,)cioo 13329
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-er 8706  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-sup 9440  df-inf 9441  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-n0 12478  df-z 12564  df-uz 12828  df-ioo 13333
This theorem is referenced by:  fourierdlem73  45195
  Copyright terms: Public domain W3C validator