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 44369
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 12164 . . . 4 1 ∈ ℕ
2 rzal 4466 . . . . 5 (𝐴 = ∅ → ∀𝑖𝐴 𝜒)
32ralrimivw 3147 . . . 4 (𝐴 = ∅ → ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒)
4 oveq1 7364 . . . . . 6 (𝑛 = 1 → (𝑛(,)+∞) = (1(,)+∞))
54raleqdv 3313 . . . . 5 (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒))
65rspcev 3581 . . . 4 ((1 ∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
71, 3, 6sylancr 587 . . 3 (𝐴 = ∅ → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
87adantl 482 . 2 ((𝜑𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
9 fourierdlem31.n . . . 4 𝑁 = sup(ran 𝑉, ℝ, < )
10 fourierdlem31.i . . . . . . 7 𝑖𝜑
11 fourierdlem31.v . . . . . . 7 𝑉 = (𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
12 fourierdlem31.m . . . . . . . . . 10 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
1312a1i 11 . . . . . . . . 9 ((𝜑𝑖𝐴) → 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
1413infeq1d 9413 . . . . . . . 8 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ))
15 ssrab2 4037 . . . . . . . . 9 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ
16 nnuz 12806 . . . . . . . . . . 11 ℕ = (ℤ‘1)
1715, 16sseqtri 3980 . . . . . . . . . 10 {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1)
18 fourierdlem31.exm . . . . . . . . . . . 12 (𝜑 → ∀𝑖𝐴𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
1918r19.21bi 3234 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
20 rabn0 4345 . . . . . . . . . . 11 ({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)
2119, 20sylibr 233 . . . . . . . . . 10 ((𝜑𝑖𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅)
22 infssuzcl 12857 . . . . . . . . . 10 (({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ‘1) ∧ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2317, 21, 22sylancr 587 . . . . . . . . 9 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
2415, 23sselid 3942 . . . . . . . 8 ((𝜑𝑖𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ ℕ)
2514, 24eqeltrd 2838 . . . . . . 7 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℕ)
2610, 11, 25rnmptssd 43406 . . . . . 6 (𝜑 → ran 𝑉 ⊆ ℕ)
2726adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ)
28 ltso 11235 . . . . . . 7 < Or ℝ
2928a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or ℝ)
30 fourierdlem31.a . . . . . . . . . 10 (𝜑𝐴 ∈ Fin)
31 mptfi 9295 . . . . . . . . . 10 (𝐴 ∈ Fin → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3230, 31syl 17 . . . . . . . . 9 (𝜑 → (𝑖𝐴 ↦ inf(𝑀, ℝ, < )) ∈ Fin)
3311, 32eqeltrid 2842 . . . . . . . 8 (𝜑𝑉 ∈ Fin)
34 rnfi 9279 . . . . . . . 8 (𝑉 ∈ Fin → ran 𝑉 ∈ Fin)
3533, 34syl 17 . . . . . . 7 (𝜑 → ran 𝑉 ∈ Fin)
3635adantr 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin)
37 neqne 2951 . . . . . . . . 9 𝐴 = ∅ → 𝐴 ≠ ∅)
38 n0 4306 . . . . . . . . 9 (𝐴 ≠ ∅ ↔ ∃𝑖 𝑖𝐴)
3937, 38sylib 217 . . . . . . . 8 𝐴 = ∅ → ∃𝑖 𝑖𝐴)
4039adantl 482 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖𝐴)
41 nfv 1917 . . . . . . . . 9 𝑖 ¬ 𝐴 = ∅
4210, 41nfan 1902 . . . . . . . 8 𝑖(𝜑 ∧ ¬ 𝐴 = ∅)
43 fourierdlem31.iv . . . . . . . . . 10 𝑖𝑉
4443nfrn 5907 . . . . . . . . 9 𝑖ran 𝑉
45 nfcv 2907 . . . . . . . . 9 𝑖
4644, 45nfne 3045 . . . . . . . 8 𝑖ran 𝑉 ≠ ∅
47 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → 𝑖𝐴)
4811elrnmpt1 5913 . . . . . . . . . . . 12 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
4947, 25, 48syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉)
5049ne0d 4295 . . . . . . . . . 10 ((𝜑𝑖𝐴) → ran 𝑉 ≠ ∅)
5150ex 413 . . . . . . . . 9 (𝜑 → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5251adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖𝐴 → ran 𝑉 ≠ ∅))
5342, 46, 52exlimd 2211 . . . . . . 7 ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖𝐴 → ran 𝑉 ≠ ∅))
5440, 53mpd 15 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅)
55 nnssre 12157 . . . . . . 7 ℕ ⊆ ℝ
5627, 55sstrdi 3956 . . . . . 6 ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ)
57 fisupcl 9405 . . . . . 6 (( < Or ℝ ∧ (ran 𝑉 ∈ Fin ∧ ran 𝑉 ≠ ∅ ∧ ran 𝑉 ⊆ ℝ)) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
5829, 36, 54, 56, 57syl13anc 1372 . . . . 5 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉)
5927, 58sseldd 3945 . . . 4 ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ℕ)
609, 59eqeltrid 2842 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ)
61 fourierdlem31.r . . . . 5 𝑟𝜑
62 nfcv 2907 . . . . . . . . . . . 12 𝑖
63 nfcv 2907 . . . . . . . . . . . 12 𝑖 <
6444, 62, 63nfsup 9387 . . . . . . . . . . 11 𝑖sup(ran 𝑉, ℝ, < )
659, 64nfcxfr 2905 . . . . . . . . . 10 𝑖𝑁
66 nfcv 2907 . . . . . . . . . 10 𝑖(,)
67 nfcv 2907 . . . . . . . . . 10 𝑖+∞
6865, 66, 67nfov 7387 . . . . . . . . 9 𝑖(𝑁(,)+∞)
6968nfcri 2894 . . . . . . . 8 𝑖 𝑟 ∈ (𝑁(,)+∞)
7010, 69nfan 1902 . . . . . . 7 𝑖(𝜑𝑟 ∈ (𝑁(,)+∞))
7111fvmpt2 6959 . . . . . . . . . . . . . 14 ((𝑖𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7247, 25, 71syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) = inf(𝑀, ℝ, < ))
7325nnxrd 43497 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ ℝ*)
7472, 73eqeltrd 2838 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ*)
7574adantr 481 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ*)
76 pnfxr 11209 . . . . . . . . . . . 12 +∞ ∈ ℝ*
7776a1i 11 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈ ℝ*)
78 elioore 13294 . . . . . . . . . . . 12 (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ)
7978adantl 482 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ)
8072, 25eqeltrd 2838 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℕ)
8180nnred 12168 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ℝ)
8281adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ∈ ℝ)
83 ne0i 4294 . . . . . . . . . . . . . . . . 17 (𝑖𝐴𝐴 ≠ ∅)
8483adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝐴) → 𝐴 ≠ ∅)
8584neneqd 2948 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ¬ 𝐴 = ∅)
8685, 60syldan 591 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → 𝑁 ∈ ℕ)
8786nnred 12168 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → 𝑁 ∈ ℝ)
8887adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ)
8985, 56syldan 591 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ran 𝑉 ⊆ ℝ)
9026, 55sstrdi 3956 . . . . . . . . . . . . . . . . 17 (𝜑 → ran 𝑉 ⊆ ℝ)
91 fimaxre2 12100 . . . . . . . . . . . . . . . . 17 ((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9290, 35, 91syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9392adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥)
9472, 49eqeltrd 2838 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ ran 𝑉)
95 suprub 12116 . . . . . . . . . . . . . . 15 (((ran 𝑉 ⊆ ℝ ∧ ran 𝑉 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦𝑥) ∧ (𝑉𝑖) ∈ ran 𝑉) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
9689, 50, 93, 94, 95syl31anc 1373 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ sup(ran 𝑉, ℝ, < ))
9796, 9breqtrrdi 5147 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ≤ 𝑁)
9897adantr 481 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) ≤ 𝑁)
9988rexrd 11205 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ*)
100 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞))
101 ioogtlb 43723 . . . . . . . . . . . . 13 ((𝑁 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
10299, 77, 100, 101syl3anc 1371 . . . . . . . . . . . 12 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟)
10382, 88, 79, 98, 102lelttrd 11313 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉𝑖) < 𝑟)
10479ltpnfd 13042 . . . . . . . . . . 11 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞)
10575, 77, 79, 103, 104eliood 43726 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉𝑖)(,)+∞))
10614, 23eqeltrd 2838 . . . . . . . . . . . . . 14 ((𝜑𝑖𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
10772, 106eqeltrd 2838 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})
108 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑚𝐴
109 nfrab1 3426 . . . . . . . . . . . . . . . . . . . 20 𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
11012, 109nfcxfr 2905 . . . . . . . . . . . . . . . . . . 19 𝑚𝑀
111 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑚
112 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑚 <
113110, 111, 112nfinf 9418 . . . . . . . . . . . . . . . . . 18 𝑚inf(𝑀, ℝ, < )
114108, 113nfmpt 5212 . . . . . . . . . . . . . . . . 17 𝑚(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
11511, 114nfcxfr 2905 . . . . . . . . . . . . . . . 16 𝑚𝑉
116 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑚𝑖
117115, 116nffv 6852 . . . . . . . . . . . . . . 15 𝑚(𝑉𝑖)
118117, 109nfel 2921 . . . . . . . . . . . . . . . 16 𝑚(𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
119117nfel1 2923 . . . . . . . . . . . . . . . . 17 𝑚(𝑉𝑖) ∈ ℕ
120 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑚(,)
121 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑚+∞
122117, 120, 121nfov 7387 . . . . . . . . . . . . . . . . . 18 𝑚((𝑉𝑖)(,)+∞)
123 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑚𝜒
124122, 123nfralw 3294 . . . . . . . . . . . . . . . . 17 𝑚𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒
125119, 124nfan 1902 . . . . . . . . . . . . . . . 16 𝑚((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
126118, 125nfbi 1906 . . . . . . . . . . . . . . 15 𝑚((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
127 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}))
128 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (𝑚 ∈ ℕ ↔ (𝑉𝑖) ∈ ℕ))
129 oveq1 7364 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑉𝑖) → (𝑚(,)+∞) = ((𝑉𝑖)(,)+∞))
130 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑟(𝑚(,)+∞)
131 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟𝐴
132 nfra1 3267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟𝑟 ∈ (𝑚(,)+∞)𝜒
133 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑟
134132, 133nfrabw 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}
13512, 134nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟𝑀
136 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟
137 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑟 <
138135, 136, 137nfinf 9418 . . . . . . . . . . . . . . . . . . . . . . 23 𝑟inf(𝑀, ℝ, < )
139131, 138nfmpt 5212 . . . . . . . . . . . . . . . . . . . . . 22 𝑟(𝑖𝐴 ↦ inf(𝑀, ℝ, < ))
14011, 139nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑉
141 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑟𝑖
142140, 141nffv 6852 . . . . . . . . . . . . . . . . . . . 20 𝑟(𝑉𝑖)
143 nfcv 2907 . . . . . . . . . . . . . . . . . . . 20 𝑟(,)
144 nfcv 2907 . . . . . . . . . . . . . . . . . . . 20 𝑟+∞
145142, 143, 144nfov 7387 . . . . . . . . . . . . . . . . . . 19 𝑟((𝑉𝑖)(,)+∞)
146130, 145raleqf 3328 . . . . . . . . . . . . . . . . . 18 ((𝑚(,)+∞) = ((𝑉𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
147129, 146syl 17 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑉𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
148128, 147anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
149127, 148bibi12d 345 . . . . . . . . . . . . . . 15 (𝑚 = (𝑉𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))))
150 rabid 3427 . . . . . . . . . . . . . . 15 (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒))
151117, 126, 149, 150vtoclgf 3523 . . . . . . . . . . . . . 14 ((𝑉𝑖) ∈ ℕ → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
15280, 151syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)))
153107, 152mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑖𝐴) → ((𝑉𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒))
154153simprd 496 . . . . . . . . . . 11 ((𝜑𝑖𝐴) → ∀𝑟 ∈ ((𝑉𝑖)(,)+∞)𝜒)
155154r19.21bi 3234 . . . . . . . . . 10 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ ((𝑉𝑖)(,)+∞)) → 𝜒)
156105, 155syldan 591 . . . . . . . . 9 (((𝜑𝑖𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒)
157156an32s 650 . . . . . . . 8 (((𝜑𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖𝐴) → 𝜒)
158157ex 413 . . . . . . 7 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → (𝑖𝐴𝜒))
15970, 158ralrimi 3240 . . . . . 6 ((𝜑𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖𝐴 𝜒)
160159ex 413 . . . . 5 (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖𝐴 𝜒))
16161, 160ralrimi 3240 . . . 4 (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
162161adantr 481 . . 3 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒)
163 oveq1 7364 . . . . 5 (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞))
164 nfcv 2907 . . . . . 6 𝑟(𝑛(,)+∞)
165140nfrn 5907 . . . . . . . . 9 𝑟ran 𝑉
166165, 136, 137nfsup 9387 . . . . . . . 8 𝑟sup(ran 𝑉, ℝ, < )
1679, 166nfcxfr 2905 . . . . . . 7 𝑟𝑁
168167, 143, 144nfov 7387 . . . . . 6 𝑟(𝑁(,)+∞)
169164, 168raleqf 3328 . . . . 5 ((𝑛(,)+∞) = (𝑁(,)+∞) → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
170163, 169syl 17 . . . 4 (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒))
171170rspcev 3581 . . 3 ((𝑁 ∈ ℕ ∧ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
17260, 162, 171syl2anc 584 . 2 ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
1738, 172pm2.61dan 811 1 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖𝐴 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2887  wne 2943  wral 3064  wrex 3073  {crab 3407  wss 3910  c0 4282   class class class wbr 5105  cmpt 5188   Or wor 5544  ran crn 5634  cfv 6496  (class class class)co 7357  Fincfn 8883  supcsup 9376  infcinf 9377  cr 11050  1c1 11052  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cn 12153  cuz 12763  (,)cioo 13264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-ioo 13268
This theorem is referenced by:  fourierdlem73  44410
  Copyright terms: Public domain W3C validator