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 42300
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 11637 . . . 4 1 ∈ ℕ
2 rzal 4449 . . . . 5 (𝐴 = ∅ → ∀𝑖𝐴 𝜒)
32ralrimivw 3180 . . . 4 (𝐴 = ∅ → ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒)
4 oveq1 7152 . . . . . 6 (𝑛 = 1 → (𝑛(,)+∞) = (1(,)+∞))
54raleqdv 3413 . . . . 5 (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒))
65rspcev 3620 . . . 4 ((1 ∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
71, 3, 6sylancr 587 . . 3 (𝐴 = ∅ → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
87adantl 482 . 2 ((𝜑𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
9 fourierdlem31.n . . . 4 𝑁 = sup(ran 𝑉, ℝ, < )
10 fourierdlem31.i . . . . . . . 8 𝑖𝜑
11 fourierdlem31.m . . . . . . . . . . . 12 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
1211a1i 11 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
1312infeq1d 8929 . . . . . . . . . 10 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ))
14 ssrab2 4053 . . . . . . . . . . 11 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ
15 nnuz 12269 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
1614, 15sseqtri 4000 . . . . . . . . . . . 12 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1)
17 fourierdlem31.exm . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖𝐴𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
1817r19.21bi 3205 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
19 rabn0 4336 . . . . . . . . . . . . 13 ({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
2018, 19sylibr 235 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅)
21 infssuzcl 12320 . . . . . . . . . . . 12 (({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1) ∧ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2216, 20, 21sylancr 587 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2314, 22sseldi 3962 . . . . . . . . . 10 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ ℕ)
2413, 23eqeltrd 2910 . . . . . . . . 9 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℕ)
2524ex 413 . . . . . . . 8 (𝜑 → (𝑖𝐴 → inf(𝑀, ℝ, < ) ∈ ℕ))
2610, 25ralrimi 3213 . . . . . . 7 (𝜑 → ∀𝑖𝐴 inf(𝑀, ℝ, < ) ∈ ℕ)
27 fourierdlem31.v . . . . . . . 8 𝑉 = (𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
2827rnmptss 6878 . . . . . . 7 (∀𝑖𝐴 inf(𝑀, ℝ, < ) ∈ ℕ → ran 𝑉 ⊆ ℕ)
2926, 28syl 17 . . . . . 6 (𝜑 → ran 𝑉 ⊆ ℕ)
3029adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ)
31 ltso 10709 . . . . . . 7 < Or ℝ
3231a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or ℝ)
33 fourierdlem31.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
34 mptfi 8811 . . . . . . . . . 10 (𝐴 ∈ Fin → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3533, 34syl 17 . . . . . . . . 9 (𝜑 → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3627, 35eqeltrid 2914 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
37 rnfi 8795 . . . . . . . 8 (𝑉 ∈ Fin → ran 𝑉 ∈ Fin)
3836, 37syl 17 . . . . . . 7 (𝜑 → ran 𝑉 ∈ Fin)
3938adantr 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin)
40 neqne 3021 . . . . . . . . 9 𝐴 = ∅ → 𝐴 ≠ ∅)
41 n0 4307 . . . . . . . . 9 (𝐴 ≠ ∅ ↔ ∃𝑖 𝑖𝐴)
4240, 41sylib 219 . . . . . . . 8 𝐴 = ∅ → ∃𝑖 𝑖𝐴)
4342adantl 482 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖𝐴)
44 nfv 1906 . . . . . . . . 9 𝑖 ¬ 𝐴 = ∅
4510, 44nfan 1891 . . . . . . . 8 𝑖(𝜑 ∧ ¬ 𝐴 = ∅)
46 fourierdlem31.iv . . . . . . . . . 10 𝑖𝑉
4746nfrn 5817 . . . . . . . . 9 𝑖ran 𝑉
48 nfcv 2974 . . . . . . . . 9 𝑖
4947, 48nfne 3116 . . . . . . . 8 𝑖ran 𝑉 ≠ ∅
50 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → 𝑖𝐴)
5127elrnmpt1 5823 . . . . . . . . . . . 12 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
5250, 24, 51syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
5352ne0d 4298 . . . . . . . . . 10 ((𝜑𝑖𝐴) → ran 𝑉 ≠ ∅)
5453ex 413 . . . . . . . . 9 (𝜑 → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5554adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5645, 49, 55exlimd 2208 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖𝐴 → ran 𝑉 ≠ ∅))
5743, 56mpd 15 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅)
58 nnssre 11630 . . . . . . 7 ℕ ⊆ ℝ
5930, 58sstrdi 3976 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ)
60 fisupcl 8921 . . . . . 6 (( < Or ℝ ∧ (ran 𝑉 ∈ Fin ∧ ran 𝑉 ≠ ∅ ∧ ran 𝑉 ⊆ ℝ)) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
6132, 39, 57, 59, 60syl13anc 1364 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
6230, 61sseldd 3965 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ℕ)
639, 62eqeltrid 2914 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ)
64 fourierdlem31.r . . . . 5 𝑟𝜑
65 nfcv 2974 . . . . . . . . . . . 12 𝑖
66 nfcv 2974 . . . . . . . . . . . 12 𝑖 <
6747, 65, 66nfsup 8903 . . . . . . . . . . 11 𝑖sup(ran 𝑉, ℝ, < )
689, 67nfcxfr 2972 . . . . . . . . . 10 𝑖𝑁
69 nfcv 2974 . . . . . . . . . 10 𝑖(,)
70 nfcv 2974 . . . . . . . . . 10 𝑖+∞
7168, 69, 70nfov 7175 . . . . . . . . 9 𝑖(𝑁(,)+∞)
7271nfcri 2968 . . . . . . . 8 𝑖 𝑟 ∈ (𝑁(,)+∞)
7310, 72nfan 1891 . . . . . . 7 𝑖(𝜑𝑟 ∈ (𝑁(,)+∞))
7427fvmpt2 6771 . . . . . . . . . . . . . 14 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7550, 24, 74syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7624nnxrd 41176 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℝ*)
7775, 76eqeltrd 2910 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ*)
7877adantr 481 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ*)
79 pnfxr 10683 . . . . . . . . . . . 12 +∞ ∈ ℝ*
8079a1i 11 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈ ℝ*)
81 elioore 12756 . . . . . . . . . . . 12 (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ)
8281adantl 482 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ)
8375, 24eqeltrd 2910 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℕ)
8483nnred 11641 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ)
8584adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ)
86 ne0i 4297 . . . . . . . . . . . . . . . . 17 (𝑖𝐴𝐴 ≠ ∅)
8786adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐴) → 𝐴 ≠ ∅)
8887neneqd 3018 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ¬ 𝐴 = ∅)
8988, 63syldan 591 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → 𝑁 ∈ ℕ)
9089nnred 11641 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → 𝑁 ∈ ℝ)
9190adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ)
9288, 59syldan 591 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ran 𝑉 ⊆ ℝ)
9329, 58sstrdi 3976 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑉 ⊆ ℝ)
94 fimaxre2 11574 . . . . . . . . . . . . . . . . 17 ((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9593, 38, 94syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9695adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9775, 52eqeltrd 2910 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ran 𝑉)
98 suprub 11590 . . . . . . . . . . . . . . 15 (((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥) ∧ (𝑉𝑖) ∈ ran 𝑉) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
9992, 53, 96, 97, 98syl31anc 1365 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
10099, 9breqtrrdi 5099 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ 𝑁)
101100adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ≤ 𝑁)
10291rexrd 10679 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ*)
103 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞))
104 ioogtlb 41646 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
105102, 80, 103, 104syl3anc 1363 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
10685, 91, 82, 101, 105lelttrd 10786 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) < 𝑟)
10782ltpnfd 12504 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞)
10878, 80, 82, 106, 107eliood 41649 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉𝑖)(,)+∞))
10913, 22eqeltrd 2910 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
11075, 109eqeltrd 2910 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
111 nfcv 2974 . . . . . . . . . . . . . . . . . 18 𝑚𝐴
112 nfrab1 3382 . . . . . . . . . . . . . . . . . . . 20 𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
11311, 112nfcxfr 2972 . . . . . . . . . . . . . . . . . . 19 𝑚𝑀
114 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑚
115 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑚 <
116113, 114, 115nfinf 8934 . . . . . . . . . . . . . . . . . 18 𝑚inf(𝑀, ℝ, < )
117111, 116nfmpt 5154 . . . . . . . . . . . . . . . . 17 𝑚(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
11827, 117nfcxfr 2972 . . . . . . . . . . . . . . . 16 𝑚𝑉
119 nfcv 2974 . . . . . . . . . . . . . . . 16 𝑚𝑖
120118, 119nffv 6673 . . . . . . . . . . . . . . 15 𝑚(𝑉𝑖)
121120, 112nfel 2989 . . . . . . . . . . . . . . . 16 𝑚(𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
122120nfel1 2991 . . . . . . . . . . . . . . . . 17 𝑚(𝑉𝑖) ∈ ℕ
123 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑚(,)
124 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑚+∞
125120, 123, 124nfov 7175 . . . . . . . . . . . . . . . . . 18 𝑚((𝑉𝑖)(,)+∞)
126 nfv 1906 . . . . . . . . . . . . . . . . . 18 𝑚𝜒
127125, 126nfralw 3222 . . . . . . . . . . . . . . . . 17 𝑚𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒
128122, 127nfan 1891 . . . . . . . . . . . . . . . 16 𝑚((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
129121, 128nfbi 1895 . . . . . . . . . . . . . . 15 𝑚((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
130 eleq1 2897 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}))
131 eleq1 2897 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (𝑚 ∈ ℕ ↔ (𝑉𝑖) ∈ ℕ))
132 oveq1 7152 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑉𝑖) → (𝑚(,)+∞) = ((𝑉𝑖)(,)+∞))
133 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑟(𝑚(,)+∞)
134 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟𝐴
135 nfra1 3216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟𝑟 ∈ (𝑚(,)+∞)𝜒
136 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟
137135, 136nfrabw 3383 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
13811, 137nfcxfr 2972 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟𝑀
139 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟
140 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟 <
141138, 139, 140nfinf 8934 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟inf(𝑀, ℝ, < )
142134, 141nfmpt 5154 . . . . . . . . . . . . . . . . . . . . . 22 𝑟(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
14327, 142nfcxfr 2972 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑉
144 nfcv 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑖
145143, 144nffv 6673 . . . . . . . . . . . . . . . . . . . 20 𝑟(𝑉𝑖)
146 nfcv 2974 . . . . . . . . . . . . . . . . . . . 20 𝑟(,)
147 nfcv 2974 . . . . . . . . . . . . . . . . . . . 20 𝑟+∞
148145, 146, 147nfov 7175 . . . . . . . . . . . . . . . . . . 19 𝑟((𝑉𝑖)(,)+∞)
149133, 148raleqf 3395 . . . . . . . . . . . . . . . . . 18 ((𝑚(,)+∞) = ((𝑉𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
150132, 149syl 17 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
151131, 150anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
152130, 151bibi12d 347 . . . . . . . . . . . . . . 15 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))))
153 rabid 3376 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒))
154120, 129, 152, 153vtoclgf 3563 . . . . . . . . . . . . . 14 ((𝑉𝑖) ∈ ℕ → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
15583, 154syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
156110, 155mpbid 233 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
157156simprd 496 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
158157r19.21bi 3205 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ ((𝑉𝑖)(,)+∞)) → 𝜒)
159108, 158syldan 591 . . . . . . . . 9 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒)
160159an32s 648 . . . . . . . 8 (((𝜑𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖𝐴) → 𝜒)
161160ex 413 . . . . . . 7 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → (𝑖𝐴𝜒))
16273, 161ralrimi 3213 . . . . . 6 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖𝐴 𝜒)
163162ex 413 . . . . 5 (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖𝐴 𝜒))
16464, 163ralrimi 3213 . . . 4 (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
165164adantr 481 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
166 oveq1 7152 . . . . 5 (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞))
167 nfcv 2974 . . . . . 6 𝑟(𝑛(,)+∞)
168143nfrn 5817 . . . . . . . . 9 𝑟ran 𝑉
169168, 139, 140nfsup 8903 . . . . . . . 8 𝑟sup(ran 𝑉, ℝ, < )
1709, 169nfcxfr 2972 . . . . . . 7 𝑟𝑁
171170, 146, 147nfov 7175 . . . . . 6 𝑟(𝑁(,)+∞)
172167, 171raleqf 3395 . . . . 5 ((𝑛(,)+∞) = (𝑁(,)+∞) → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
173166, 172syl 17 . . . 4 (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
174173rspcev 3620 . . 3 ((𝑁 ∈ ℕ ∧ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
17563, 165, 174syl2anc 584 . 2 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
1768, 175pm2.61dan 809 1 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wex 1771  wnf 1775  wcel 2105  wnfc 2958  wne 3013  wral 3135  wrex 3136  {crab 3139  wss 3933  c0 4288   class class class wbr 5057  cmpt 5137   Or wor 5466  ran crn 5549  cfv 6348  (class class class)co 7145  Fincfn 8497  supcsup 8892  infcinf 8893  cr 10524  1c1 10526  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664  cn 11626  cuz 12231  (,)cioo 12726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970  df-uz 12232  df-ioo 12730
This theorem is referenced by:  fourierdlem73  42341
  Copyright terms: Public domain W3C validator