Step | Hyp | Ref
| Expression |
1 | | 1nn 11486 |
. . . 4
⊢ 1 ∈
ℕ |
2 | | rzal 4361 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑖 ∈ 𝐴 𝜒) |
3 | 2 | ralrimivw 3148 |
. . . 4
⊢ (𝐴 = ∅ → ∀𝑟 ∈
(1(,)+∞)∀𝑖
∈ 𝐴 𝜒) |
4 | | oveq1 7014 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛(,)+∞) =
(1(,)+∞)) |
5 | 4 | raleqdv 3372 |
. . . . 5
⊢ (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
6 | 5 | rspcev 3554 |
. . . 4
⊢ ((1
∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
7 | 1, 3, 6 | sylancr 587 |
. . 3
⊢ (𝐴 = ∅ → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
8 | 7 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
9 | | fourierdlem31.n |
. . . 4
⊢ 𝑁 = sup(ran 𝑉, ℝ, < ) |
10 | | fourierdlem31.i |
. . . . . . . 8
⊢
Ⅎ𝑖𝜑 |
11 | | fourierdlem31.m |
. . . . . . . . . . . 12
⊢ 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑀 = {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
13 | 12 | infeq1d 8777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < )) |
14 | | ssrab2 3972 |
. . . . . . . . . . 11
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ |
15 | | nnuz 12119 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
16 | 14, 15 | sseqtri 3919 |
. . . . . . . . . . . 12
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆
(ℤ≥‘1) |
17 | | fourierdlem31.exm |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
18 | 17 | r19.21bi 3173 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
19 | | rabn0 4253 |
. . . . . . . . . . . . 13
⊢ ({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
20 | 18, 19 | sylibr 235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) |
21 | | infssuzcl 12170 |
. . . . . . . . . . . 12
⊢ (({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ≥‘1)
∧ {𝑚 ∈ ℕ
∣ ∀𝑟 ∈
(𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
22 | 16, 20, 21 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
23 | 14, 22 | sseldi 3882 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈
ℕ) |
24 | 13, 23 | eqeltrd 2881 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℕ) |
25 | 24 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ 𝐴 → inf(𝑀, ℝ, < ) ∈
ℕ)) |
26 | 10, 25 | ralrimi 3181 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 inf(𝑀, ℝ, < ) ∈
ℕ) |
27 | | fourierdlem31.v |
. . . . . . . 8
⊢ 𝑉 = (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
28 | 27 | rnmptss 6740 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐴 inf(𝑀, ℝ, < ) ∈ ℕ → ran
𝑉 ⊆
ℕ) |
29 | 26, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ ℕ) |
30 | 29 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ) |
31 | | ltso 10557 |
. . . . . . 7
⊢ < Or
ℝ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or
ℝ) |
33 | | fourierdlem31.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ Fin) |
34 | | mptfi 8659 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) |
36 | 27, 35 | syl5eqel 2885 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ Fin) |
37 | | rnfi 8643 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → ran 𝑉 ∈ Fin) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑉 ∈ Fin) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin) |
40 | | neqne 2990 |
. . . . . . . . 9
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) |
41 | | n0 4224 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔
∃𝑖 𝑖 ∈ 𝐴) |
42 | 40, 41 | sylib 219 |
. . . . . . . 8
⊢ (¬
𝐴 = ∅ →
∃𝑖 𝑖 ∈ 𝐴) |
43 | 42 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖 ∈ 𝐴) |
44 | | nfv 1890 |
. . . . . . . . 9
⊢
Ⅎ𝑖 ¬ 𝐴 = ∅ |
45 | 10, 44 | nfan 1879 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ ¬ 𝐴 = ∅) |
46 | | fourierdlem31.iv |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝑉 |
47 | 46 | nfrn 5698 |
. . . . . . . . 9
⊢
Ⅎ𝑖ran
𝑉 |
48 | | nfcv 2947 |
. . . . . . . . 9
⊢
Ⅎ𝑖∅ |
49 | 47, 48 | nfne 3085 |
. . . . . . . 8
⊢
Ⅎ𝑖ran 𝑉 ≠ ∅ |
50 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴) |
51 | 27 | elrnmpt1 5704 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
inf(𝑀, ℝ, < )
∈ ran 𝑉) |
52 | 50, 24, 51 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉) |
53 | 52 | ne0d 4215 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ≠ ∅) |
54 | 53 | ex 413 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
55 | 54 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
56 | 45, 49, 55 | exlimd 2181 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
57 | 43, 56 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅) |
58 | | nnssre 11479 |
. . . . . . 7
⊢ ℕ
⊆ ℝ |
59 | 30, 58 | syl6ss 3896 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ) |
60 | | fisupcl 8769 |
. . . . . 6
⊢ (( <
Or ℝ ∧ (ran 𝑉
∈ Fin ∧ ran 𝑉 ≠
∅ ∧ ran 𝑉 ⊆
ℝ)) → sup(ran 𝑉,
ℝ, < ) ∈ ran 𝑉) |
61 | 32, 39, 57, 59, 60 | syl13anc 1363 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉) |
62 | 30, 61 | sseldd 3885 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈
ℕ) |
63 | 9, 62 | syl5eqel 2885 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ) |
64 | | fourierdlem31.r |
. . . . 5
⊢
Ⅎ𝑟𝜑 |
65 | | nfcv 2947 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖ℝ |
66 | | nfcv 2947 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖
< |
67 | 47, 65, 66 | nfsup 8751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖sup(ran 𝑉, ℝ, < ) |
68 | 9, 67 | nfcxfr 2945 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝑁 |
69 | | nfcv 2947 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(,) |
70 | | nfcv 2947 |
. . . . . . . . . 10
⊢
Ⅎ𝑖+∞ |
71 | 68, 69, 70 | nfov 7037 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝑁(,)+∞) |
72 | 71 | nfcri 2941 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝑟 ∈ (𝑁(,)+∞) |
73 | 10, 72 | nfan 1879 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) |
74 | 27 | fvmpt2 6636 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
(𝑉‘𝑖) = inf(𝑀, ℝ, < )) |
75 | 50, 24, 74 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) = inf(𝑀, ℝ, < )) |
76 | 24 | nnxrd 40790 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℝ*) |
77 | 75, 76 | eqeltrd 2881 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈
ℝ*) |
78 | 77 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈
ℝ*) |
79 | | pnfxr 10530 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
80 | 79 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈
ℝ*) |
81 | | elioore 12607 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ) |
82 | 81 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ) |
83 | 75, 24 | eqeltrd 2881 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℕ) |
84 | 83 | nnred 11490 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℝ) |
85 | 84 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈ ℝ) |
86 | | ne0i 4214 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝐴 → 𝐴 ≠ ∅) |
87 | 86 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐴 ≠ ∅) |
88 | 87 | neneqd 2987 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ¬ 𝐴 = ∅) |
89 | 88, 63 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℕ) |
90 | 89 | nnred 11490 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℝ) |
91 | 90 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ) |
92 | 88, 59 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ⊆ ℝ) |
93 | 29, 58 | syl6ss 3896 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝑉 ⊆ ℝ) |
94 | | fimaxre2 11423 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
95 | 93, 38, 94 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
97 | 75, 52 | eqeltrd 2881 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ran 𝑉) |
98 | | suprub 11439 |
. . . . . . . . . . . . . . 15
⊢ (((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) ∧ (𝑉‘𝑖) ∈ ran 𝑉) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) |
99 | 92, 53, 96, 97, 98 | syl31anc 1364 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) |
100 | 99, 9 | syl6breqr 4998 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ 𝑁) |
101 | 100 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ≤ 𝑁) |
102 | 91 | rexrd 10526 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈
ℝ*) |
103 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞)) |
104 | | ioogtlb 41266 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) |
105 | 102, 80, 103, 104 | syl3anc 1362 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) |
106 | 85, 91, 82, 101, 105 | lelttrd 10634 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) < 𝑟) |
107 | 82 | ltpnfd 12355 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞) |
108 | 78, 80, 82, 106, 107 | eliood 41269 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) |
109 | 13, 22 | eqeltrd 2881 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
110 | 75, 109 | eqeltrd 2881 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
111 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝐴 |
112 | | nfrab1 3341 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
113 | 11, 112 | nfcxfr 2945 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝑀 |
114 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚ℝ |
115 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚
< |
116 | 113, 114,
115 | nfinf 8782 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚inf(𝑀, ℝ, < ) |
117 | 111, 116 | nfmpt 5051 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
118 | 27, 117 | nfcxfr 2945 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑉 |
119 | | nfcv 2947 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑖 |
120 | 118, 119 | nffv 6540 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑉‘𝑖) |
121 | 120, 112 | nfel 2959 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
122 | 120 | nfel1 2961 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ ℕ |
123 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚(,) |
124 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚+∞ |
125 | 120, 123,
124 | nfov 7037 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚((𝑉‘𝑖)(,)+∞) |
126 | | nfv 1890 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝜒 |
127 | 125, 126 | nfral 3189 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒 |
128 | 122, 127 | nfan 1879 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) |
129 | 121, 128 | nfbi 1883 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
130 | | eleq1 2868 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})) |
131 | | eleq1 2868 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ ℕ ↔ (𝑉‘𝑖) ∈ ℕ)) |
132 | | oveq1 7014 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞)) |
133 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟(𝑚(,)+∞) |
134 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟𝐴 |
135 | | nfra1 3184 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟∀𝑟 ∈ (𝑚(,)+∞)𝜒 |
136 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟ℕ |
137 | 135, 136 | nfrab 3342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
138 | 11, 137 | nfcxfr 2945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟𝑀 |
139 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟ℝ |
140 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟
< |
141 | 138, 139,
140 | nfinf 8782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟inf(𝑀, ℝ, < ) |
142 | 134, 141 | nfmpt 5051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑟(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
143 | 27, 142 | nfcxfr 2945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑉 |
144 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑖 |
145 | 143, 144 | nffv 6540 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(𝑉‘𝑖) |
146 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(,) |
147 | | nfcv 2947 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟+∞ |
148 | 145, 146,
147 | nfov 7037 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟((𝑉‘𝑖)(,)+∞) |
149 | 133, 148 | raleqf 3354 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
150 | 132, 149 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
151 | 131, 150 | anbi12d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
152 | 130, 151 | bibi12d 347 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)))) |
153 | | rabid 3334 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) |
154 | 120, 129,
152, 153 | vtoclgf 3503 |
. . . . . . . . . . . . . 14
⊢ ((𝑉‘𝑖) ∈ ℕ → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
155 | 83, 154 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
156 | 110, 155 | mpbid 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
157 | 156 | simprd 496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) |
158 | 157 | r19.21bi 3173 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) → 𝜒) |
159 | 108, 158 | syldan 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒) |
160 | 159 | an32s 648 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖 ∈ 𝐴) → 𝜒) |
161 | 160 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑖 ∈ 𝐴 → 𝜒)) |
162 | 73, 161 | ralrimi 3181 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖 ∈ 𝐴 𝜒) |
163 | 162 | ex 413 |
. . . . 5
⊢ (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖 ∈ 𝐴 𝜒)) |
164 | 64, 163 | ralrimi 3181 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
165 | 164 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
166 | | oveq1 7014 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞)) |
167 | | nfcv 2947 |
. . . . . 6
⊢
Ⅎ𝑟(𝑛(,)+∞) |
168 | 143 | nfrn 5698 |
. . . . . . . . 9
⊢
Ⅎ𝑟ran
𝑉 |
169 | 168, 139,
140 | nfsup 8751 |
. . . . . . . 8
⊢
Ⅎ𝑟sup(ran 𝑉, ℝ, < ) |
170 | 9, 169 | nfcxfr 2945 |
. . . . . . 7
⊢
Ⅎ𝑟𝑁 |
171 | 170, 146,
147 | nfov 7037 |
. . . . . 6
⊢
Ⅎ𝑟(𝑁(,)+∞) |
172 | 167, 171 | raleqf 3354 |
. . . . 5
⊢ ((𝑛(,)+∞) = (𝑁(,)+∞) →
(∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
173 | 166, 172 | syl 17 |
. . . 4
⊢ (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
174 | 173 | rspcev 3554 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧
∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
175 | 63, 165, 174 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
176 | 8, 175 | pm2.61dan 809 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |