| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1nn 12278 | . . . 4
⊢ 1 ∈
ℕ | 
| 2 |  | rzal 4508 | . . . . 5
⊢ (𝐴 = ∅ → ∀𝑖 ∈ 𝐴 𝜒) | 
| 3 | 2 | ralrimivw 3149 | . . . 4
⊢ (𝐴 = ∅ → ∀𝑟 ∈
(1(,)+∞)∀𝑖
∈ 𝐴 𝜒) | 
| 4 |  | oveq1 7439 | . . . . . 6
⊢ (𝑛 = 1 → (𝑛(,)+∞) =
(1(,)+∞)) | 
| 5 | 4 | raleqdv 3325 | . . . . 5
⊢ (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) | 
| 6 | 5 | rspcev 3621 | . . . 4
⊢ ((1
∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 7 | 1, 3, 6 | sylancr 587 | . . 3
⊢ (𝐴 = ∅ → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 8 | 7 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 9 |  | fourierdlem31.n | . . . 4
⊢ 𝑁 = sup(ran 𝑉, ℝ, < ) | 
| 10 |  | fourierdlem31.i | . . . . . . 7
⊢
Ⅎ𝑖𝜑 | 
| 11 |  | fourierdlem31.v | . . . . . . 7
⊢ 𝑉 = (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) | 
| 12 |  | fourierdlem31.m | . . . . . . . . . 10
⊢ 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} | 
| 13 | 12 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) | 
| 14 | 13 | infeq1d 9518 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < )) | 
| 15 |  | ssrab2 4079 | . . . . . . . . 9
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ | 
| 16 |  | nnuz 12922 | . . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) | 
| 17 | 15, 16 | sseqtri 4031 | . . . . . . . . . 10
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆
(ℤ≥‘1) | 
| 18 |  | fourierdlem31.exm | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) | 
| 19 | 18 | r19.21bi 3250 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) | 
| 20 |  | rabn0 4388 | . . . . . . . . . . 11
⊢ ({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) | 
| 21 | 19, 20 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) | 
| 22 |  | infssuzcl 12975 | . . . . . . . . . 10
⊢ (({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ≥‘1)
∧ {𝑚 ∈ ℕ
∣ ∀𝑟 ∈
(𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) | 
| 23 | 17, 21, 22 | sylancr 587 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) | 
| 24 | 15, 23 | sselid 3980 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈
ℕ) | 
| 25 | 14, 24 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℕ) | 
| 26 | 10, 11, 25 | rnmptssd 45206 | . . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ ℕ) | 
| 27 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ) | 
| 28 |  | ltso 11342 | . . . . . . 7
⊢  < Or
ℝ | 
| 29 | 28 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or
ℝ) | 
| 30 |  | fourierdlem31.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 31 |  | mptfi 9392 | . . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) | 
| 33 | 11, 32 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ Fin) | 
| 34 |  | rnfi 9381 | . . . . . . . 8
⊢ (𝑉 ∈ Fin → ran 𝑉 ∈ Fin) | 
| 35 | 33, 34 | syl 17 | . . . . . . 7
⊢ (𝜑 → ran 𝑉 ∈ Fin) | 
| 36 | 35 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin) | 
| 37 |  | neqne 2947 | . . . . . . . . 9
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) | 
| 38 |  | n0 4352 | . . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔
∃𝑖 𝑖 ∈ 𝐴) | 
| 39 | 37, 38 | sylib 218 | . . . . . . . 8
⊢ (¬
𝐴 = ∅ →
∃𝑖 𝑖 ∈ 𝐴) | 
| 40 | 39 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖 ∈ 𝐴) | 
| 41 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑖 ¬ 𝐴 = ∅ | 
| 42 | 10, 41 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ ¬ 𝐴 = ∅) | 
| 43 |  | fourierdlem31.iv | . . . . . . . . . 10
⊢
Ⅎ𝑖𝑉 | 
| 44 | 43 | nfrn 5962 | . . . . . . . . 9
⊢
Ⅎ𝑖ran
𝑉 | 
| 45 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑖∅ | 
| 46 | 44, 45 | nfne 3042 | . . . . . . . 8
⊢
Ⅎ𝑖ran 𝑉 ≠ ∅ | 
| 47 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴) | 
| 48 | 11 | elrnmpt1 5970 | . . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
inf(𝑀, ℝ, < )
∈ ran 𝑉) | 
| 49 | 47, 25, 48 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉) | 
| 50 | 49 | ne0d 4341 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ≠ ∅) | 
| 51 | 50 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) | 
| 52 | 51 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) | 
| 53 | 42, 46, 52 | exlimd 2217 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) | 
| 54 | 40, 53 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅) | 
| 55 |  | nnssre 12271 | . . . . . . 7
⊢ ℕ
⊆ ℝ | 
| 56 | 27, 55 | sstrdi 3995 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ) | 
| 57 |  | fisupcl 9510 | . . . . . 6
⊢ (( <
Or ℝ ∧ (ran 𝑉
∈ Fin ∧ ran 𝑉 ≠
∅ ∧ ran 𝑉 ⊆
ℝ)) → sup(ran 𝑉,
ℝ, < ) ∈ ran 𝑉) | 
| 58 | 29, 36, 54, 56, 57 | syl13anc 1373 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉) | 
| 59 | 27, 58 | sseldd 3983 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈
ℕ) | 
| 60 | 9, 59 | eqeltrid 2844 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ) | 
| 61 |  | fourierdlem31.r | . . . . 5
⊢
Ⅎ𝑟𝜑 | 
| 62 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑖ℝ | 
| 63 |  | nfcv 2904 | . . . . . . . . . . . 12
⊢
Ⅎ𝑖
< | 
| 64 | 44, 62, 63 | nfsup 9492 | . . . . . . . . . . 11
⊢
Ⅎ𝑖sup(ran 𝑉, ℝ, < ) | 
| 65 | 9, 64 | nfcxfr 2902 | . . . . . . . . . 10
⊢
Ⅎ𝑖𝑁 | 
| 66 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑖(,) | 
| 67 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑖+∞ | 
| 68 | 65, 66, 67 | nfov 7462 | . . . . . . . . 9
⊢
Ⅎ𝑖(𝑁(,)+∞) | 
| 69 | 68 | nfcri 2896 | . . . . . . . 8
⊢
Ⅎ𝑖 𝑟 ∈ (𝑁(,)+∞) | 
| 70 | 10, 69 | nfan 1898 | . . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) | 
| 71 | 11 | fvmpt2 7026 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
(𝑉‘𝑖) = inf(𝑀, ℝ, < )) | 
| 72 | 47, 25, 71 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) = inf(𝑀, ℝ, < )) | 
| 73 | 25 | nnxrd 45290 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℝ*) | 
| 74 | 72, 73 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈
ℝ*) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈
ℝ*) | 
| 76 |  | pnfxr 11316 | . . . . . . . . . . . 12
⊢ +∞
∈ ℝ* | 
| 77 | 76 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈
ℝ*) | 
| 78 |  | elioore 13418 | . . . . . . . . . . . 12
⊢ (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ) | 
| 79 | 78 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ) | 
| 80 | 72, 25 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℕ) | 
| 81 | 80 | nnred 12282 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℝ) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈ ℝ) | 
| 83 |  | ne0i 4340 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝐴 → 𝐴 ≠ ∅) | 
| 84 | 83 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐴 ≠ ∅) | 
| 85 | 84 | neneqd 2944 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ¬ 𝐴 = ∅) | 
| 86 | 85, 60 | syldan 591 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℕ) | 
| 87 | 86 | nnred 12282 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℝ) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ) | 
| 89 | 85, 56 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ⊆ ℝ) | 
| 90 | 26, 55 | sstrdi 3995 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝑉 ⊆ ℝ) | 
| 91 |  | fimaxre2 12214 | . . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) | 
| 92 | 90, 35, 91 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) | 
| 94 | 72, 49 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ran 𝑉) | 
| 95 |  | suprub 12230 | . . . . . . . . . . . . . . 15
⊢ (((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) ∧ (𝑉‘𝑖) ∈ ran 𝑉) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) | 
| 96 | 89, 50, 93, 94, 95 | syl31anc 1374 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) | 
| 97 | 96, 9 | breqtrrdi 5184 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ 𝑁) | 
| 98 | 97 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ≤ 𝑁) | 
| 99 | 88 | rexrd 11312 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈
ℝ*) | 
| 100 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞)) | 
| 101 |  | ioogtlb 45513 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) | 
| 102 | 99, 77, 100, 101 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) | 
| 103 | 82, 88, 79, 98, 102 | lelttrd 11420 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) < 𝑟) | 
| 104 | 79 | ltpnfd 13164 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞) | 
| 105 | 75, 77, 79, 103, 104 | eliood 45516 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) | 
| 106 | 14, 23 | eqeltrd 2840 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) | 
| 107 | 72, 106 | eqeltrd 2840 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) | 
| 108 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝐴 | 
| 109 |  | nfrab1 3456 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} | 
| 110 | 12, 109 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝑀 | 
| 111 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚ℝ | 
| 112 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚
< | 
| 113 | 110, 111,
112 | nfinf 9523 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚inf(𝑀, ℝ, < ) | 
| 114 | 108, 113 | nfmpt 5248 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) | 
| 115 | 11, 114 | nfcxfr 2902 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑉 | 
| 116 |  | nfcv 2904 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑖 | 
| 117 | 115, 116 | nffv 6915 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑉‘𝑖) | 
| 118 | 117, 109 | nfel 2919 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} | 
| 119 | 117 | nfel1 2921 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ ℕ | 
| 120 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚(,) | 
| 121 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚+∞ | 
| 122 | 117, 120,
121 | nfov 7462 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚((𝑉‘𝑖)(,)+∞) | 
| 123 |  | nfv 1913 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝜒 | 
| 124 | 122, 123 | nfralw 3310 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒 | 
| 125 | 119, 124 | nfan 1898 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) | 
| 126 | 118, 125 | nfbi 1902 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) | 
| 127 |  | eleq1 2828 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})) | 
| 128 |  | eleq1 2828 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ ℕ ↔ (𝑉‘𝑖) ∈ ℕ)) | 
| 129 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞)) | 
| 130 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟(𝑚(,)+∞) | 
| 131 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟𝐴 | 
| 132 |  | nfra1 3283 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟∀𝑟 ∈ (𝑚(,)+∞)𝜒 | 
| 133 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟ℕ | 
| 134 | 132, 133 | nfrabw 3474 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} | 
| 135 | 12, 134 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟𝑀 | 
| 136 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟ℝ | 
| 137 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟
< | 
| 138 | 135, 136,
137 | nfinf 9523 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟inf(𝑀, ℝ, < ) | 
| 139 | 131, 138 | nfmpt 5248 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑟(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) | 
| 140 | 11, 139 | nfcxfr 2902 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑉 | 
| 141 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑖 | 
| 142 | 140, 141 | nffv 6915 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(𝑉‘𝑖) | 
| 143 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(,) | 
| 144 |  | nfcv 2904 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟+∞ | 
| 145 | 142, 143,
144 | nfov 7462 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟((𝑉‘𝑖)(,)+∞) | 
| 146 | 130, 145 | raleqf 3352 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) | 
| 147 | 129, 146 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) | 
| 148 | 128, 147 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) | 
| 149 | 127, 148 | bibi12d 345 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)))) | 
| 150 |  | rabid 3457 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) | 
| 151 | 117, 126,
149, 150 | vtoclgf 3568 | . . . . . . . . . . . . . 14
⊢ ((𝑉‘𝑖) ∈ ℕ → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) | 
| 152 | 80, 151 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) | 
| 153 | 107, 152 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) | 
| 154 | 153 | simprd 495 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) | 
| 155 | 154 | r19.21bi 3250 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) → 𝜒) | 
| 156 | 105, 155 | syldan 591 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒) | 
| 157 | 156 | an32s 652 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖 ∈ 𝐴) → 𝜒) | 
| 158 | 157 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑖 ∈ 𝐴 → 𝜒)) | 
| 159 | 70, 158 | ralrimi 3256 | . . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖 ∈ 𝐴 𝜒) | 
| 160 | 159 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖 ∈ 𝐴 𝜒)) | 
| 161 | 61, 160 | ralrimi 3256 | . . . 4
⊢ (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 162 | 161 | adantr 480 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 163 |  | oveq1 7439 | . . . . 5
⊢ (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞)) | 
| 164 |  | nfcv 2904 | . . . . . 6
⊢
Ⅎ𝑟(𝑛(,)+∞) | 
| 165 | 140 | nfrn 5962 | . . . . . . . . 9
⊢
Ⅎ𝑟ran
𝑉 | 
| 166 | 165, 136,
137 | nfsup 9492 | . . . . . . . 8
⊢
Ⅎ𝑟sup(ran 𝑉, ℝ, < ) | 
| 167 | 9, 166 | nfcxfr 2902 | . . . . . . 7
⊢
Ⅎ𝑟𝑁 | 
| 168 | 167, 143,
144 | nfov 7462 | . . . . . 6
⊢
Ⅎ𝑟(𝑁(,)+∞) | 
| 169 | 164, 168 | raleqf 3352 | . . . . 5
⊢ ((𝑛(,)+∞) = (𝑁(,)+∞) →
(∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) | 
| 170 | 163, 169 | syl 17 | . . . 4
⊢ (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) | 
| 171 | 170 | rspcev 3621 | . . 3
⊢ ((𝑁 ∈ ℕ ∧
∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 172 | 60, 162, 171 | syl2anc 584 | . 2
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) | 
| 173 | 8, 172 | pm2.61dan 812 | 1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |