Step | Hyp | Ref
| Expression |
1 | | 1nn 11031 |
. . . 4
⊢ 1 ∈
ℕ |
2 | | rzal 4073 |
. . . . 5
⊢ (𝐴 = ∅ → ∀𝑖 ∈ 𝐴 𝜒) |
3 | 2 | ralrimivw 2967 |
. . . 4
⊢ (𝐴 = ∅ → ∀𝑟 ∈
(1(,)+∞)∀𝑖
∈ 𝐴 𝜒) |
4 | | oveq1 6657 |
. . . . . 6
⊢ (𝑛 = 1 → (𝑛(,)+∞) =
(1(,)+∞)) |
5 | 4 | raleqdv 3144 |
. . . . 5
⊢ (𝑛 = 1 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
6 | 5 | rspcev 3309 |
. . . 4
⊢ ((1
∈ ℕ ∧ ∀𝑟 ∈ (1(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
7 | 1, 3, 6 | sylancr 695 |
. . 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 8383 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) = inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < )) |
14 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ ℕ |
15 | | nnuz 11723 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
16 | 14, 15 | sseqtri 3637 |
. . . . . . . . . . . 12
⊢ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆
(ℤ≥‘1) |
17 | | fourierdlem31.exm |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
18 | 17 | r19.21bi 2932 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
19 | | rabn0 3958 |
. . . . . . . . . . . . 13
⊢ ({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅ ↔ ∃𝑚 ∈ ℕ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) |
20 | 18, 19 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ≠ ∅) |
21 | | infssuzcl 11772 |
. . . . . . . . . . . 12
⊢ (({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒} ⊆ (ℤ≥‘1)
∧ {𝑚 ∈ ℕ
∣ ∀𝑟 ∈
(𝑚(,)+∞)𝜒} ≠ ∅) → inf({𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
22 | 16, 20, 21 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣
∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
23 | 14, 22 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf({𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}, ℝ, < ) ∈
ℕ) |
24 | 13, 23 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℕ) |
25 | 24 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ 𝐴 → inf(𝑀, ℝ, < ) ∈
ℕ)) |
26 | 10, 25 | ralrimi 2957 |
. . . . . . 7
⊢ (𝜑 → ∀𝑖 ∈ 𝐴 inf(𝑀, ℝ, < ) ∈
ℕ) |
27 | | fourierdlem31.v |
. . . . . . . 8
⊢ 𝑉 = (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
28 | 27 | rnmptss 6392 |
. . . . . . 7
⊢
(∀𝑖 ∈
𝐴 inf(𝑀, ℝ, < ) ∈ ℕ → ran
𝑉 ⊆
ℕ) |
29 | 26, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑉 ⊆ ℕ) |
30 | 29 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℕ) |
31 | | ltso 10118 |
. . . . . . 7
⊢ < Or
ℝ |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → < Or
ℝ) |
33 | | fourierdlem31.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ Fin) |
34 | | mptfi 8265 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) ∈
Fin) |
36 | 27, 35 | syl5eqel 2705 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ Fin) |
37 | | rnfi 8249 |
. . . . . . . 8
⊢ (𝑉 ∈ Fin → ran 𝑉 ∈ Fin) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝑉 ∈ Fin) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ∈ Fin) |
40 | | neqne 2802 |
. . . . . . . . 9
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) |
41 | | n0 3931 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔
∃𝑖 𝑖 ∈ 𝐴) |
42 | 40, 41 | sylib 208 |
. . . . . . . 8
⊢ (¬
𝐴 = ∅ →
∃𝑖 𝑖 ∈ 𝐴) |
43 | 42 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑖 𝑖 ∈ 𝐴) |
44 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑖 ¬ 𝐴 = ∅ |
45 | 10, 44 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑖(𝜑 ∧ ¬ 𝐴 = ∅) |
46 | | fourierdlem31.iv |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝑉 |
47 | 46 | nfrn 5368 |
. . . . . . . . 9
⊢
Ⅎ𝑖ran
𝑉 |
48 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑖∅ |
49 | 47, 48 | nfne 2894 |
. . . . . . . 8
⊢
Ⅎ𝑖ran 𝑉 ≠ ∅ |
50 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑖 ∈ 𝐴) |
51 | 27 | elrnmpt1 5374 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
inf(𝑀, ℝ, < )
∈ ran 𝑉) |
52 | 50, 24, 51 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ ran 𝑉) |
53 | | ne0i 3921 |
. . . . . . . . . . 11
⊢
(inf(𝑀, ℝ,
< ) ∈ ran 𝑉 →
ran 𝑉 ≠
∅) |
54 | 52, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ≠ ∅) |
55 | 54 | ex 450 |
. . . . . . . . 9
⊢ (𝜑 → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
56 | 55 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
57 | 45, 49, 56 | exlimd 2087 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → (∃𝑖 𝑖 ∈ 𝐴 → ran 𝑉 ≠ ∅)) |
58 | 43, 57 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ≠ ∅) |
59 | | nnssre 11024 |
. . . . . . 7
⊢ ℕ
⊆ ℝ |
60 | 30, 59 | syl6ss 3615 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ran 𝑉 ⊆ ℝ) |
61 | | fisupcl 8375 |
. . . . . 6
⊢ (( <
Or ℝ ∧ (ran 𝑉
∈ Fin ∧ ran 𝑉 ≠
∅ ∧ ran 𝑉 ⊆
ℝ)) → sup(ran 𝑉,
ℝ, < ) ∈ ran 𝑉) |
62 | 32, 39, 58, 60, 61 | syl13anc 1328 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈ ran 𝑉) |
63 | 30, 62 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → sup(ran 𝑉, ℝ, < ) ∈
ℕ) |
64 | 9, 63 | syl5eqel 2705 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → 𝑁 ∈ ℕ) |
65 | | fourierdlem31.r |
. . . . 5
⊢
Ⅎ𝑟𝜑 |
66 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖ℝ |
67 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖
< |
68 | 47, 66, 67 | nfsup 8357 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖sup(ran 𝑉, ℝ, < ) |
69 | 9, 68 | nfcxfr 2762 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝑁 |
70 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(,) |
71 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑖+∞ |
72 | 69, 70, 71 | nfov 6676 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝑁(,)+∞) |
73 | 72 | nfcri 2758 |
. . . . . . . 8
⊢
Ⅎ𝑖 𝑟 ∈ (𝑁(,)+∞) |
74 | 10, 73 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑖(𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) |
75 | 27 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ 𝐴 ∧ inf(𝑀, ℝ, < ) ∈ ℕ) →
(𝑉‘𝑖) = inf(𝑀, ℝ, < )) |
76 | 50, 24, 75 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) = inf(𝑀, ℝ, < )) |
77 | 24 | nnxrd 39201 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈
ℝ*) |
78 | 76, 77 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈
ℝ*) |
79 | 78 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈
ℝ*) |
80 | | pnfxr 10092 |
. . . . . . . . . . . 12
⊢ +∞
∈ ℝ* |
81 | 80 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → +∞ ∈
ℝ*) |
82 | | elioore 12205 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (𝑁(,)+∞) → 𝑟 ∈ ℝ) |
83 | 82 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ℝ) |
84 | 76, 24 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℕ) |
85 | 84 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ℝ) |
86 | 85 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ∈ ℝ) |
87 | | ne0i 3921 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ 𝐴 → 𝐴 ≠ ∅) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝐴 ≠ ∅) |
89 | 88 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ¬ 𝐴 = ∅) |
90 | 89, 64 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℕ) |
91 | 90 | nnred 11035 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → 𝑁 ∈ ℝ) |
92 | 91 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈ ℝ) |
93 | 89, 60 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ran 𝑉 ⊆ ℝ) |
94 | 29, 59 | syl6ss 3615 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝑉 ⊆ ℝ) |
95 | | fimaxre2 10969 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
96 | 94, 38, 95 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
97 | 96 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) |
98 | 76, 52 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ ran 𝑉) |
99 | | suprub 10984 |
. . . . . . . . . . . . . . 15
⊢ (((ran
𝑉 ⊆ ℝ ∧ ran
𝑉 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran 𝑉 𝑦 ≤ 𝑥) ∧ (𝑉‘𝑖) ∈ ran 𝑉) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) |
100 | 93, 54, 97, 98, 99 | syl31anc 1329 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ sup(ran 𝑉, ℝ, < )) |
101 | 100, 9 | syl6breqr 4695 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ≤ 𝑁) |
102 | 101 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) ≤ 𝑁) |
103 | 92 | rexrd 10089 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 ∈
ℝ*) |
104 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ (𝑁(,)+∞)) |
105 | | ioogtlb 39717 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) |
106 | 103, 81, 104, 105 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑁 < 𝑟) |
107 | 86, 92, 83, 102, 106 | lelttrd 10195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑉‘𝑖) < 𝑟) |
108 | 83 | ltpnfd 11955 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 < +∞) |
109 | 79, 81, 83, 107, 108 | eliood 39720 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) |
110 | 13, 22 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → inf(𝑀, ℝ, < ) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
111 | 76, 110 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒}) |
112 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝐴 |
113 | | nfrab1 3122 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑚{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
114 | 11, 113 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚𝑀 |
115 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚ℝ |
116 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚
< |
117 | 114, 115,
116 | nfinf 8388 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚inf(𝑀, ℝ, < ) |
118 | 112, 117 | nfmpt 4746 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
119 | 27, 118 | nfcxfr 2762 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑉 |
120 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝑖 |
121 | 119, 120 | nffv 6198 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝑉‘𝑖) |
122 | 121, 113 | nfel 2777 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
123 | 121 | nfel1 2779 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚(𝑉‘𝑖) ∈ ℕ |
124 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚(,) |
125 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑚+∞ |
126 | 121, 124,
125 | nfov 6676 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚((𝑉‘𝑖)(,)+∞) |
127 | | nfv 1843 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝜒 |
128 | 126, 127 | nfral 2945 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒 |
129 | 123, 128 | nfan 1828 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) |
130 | 122, 129 | nfbi 1833 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
131 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒})) |
132 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚 ∈ ℕ ↔ (𝑉‘𝑖) ∈ ℕ)) |
133 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = (𝑉‘𝑖) → (𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞)) |
134 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟(𝑚(,)+∞) |
135 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟𝐴 |
136 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟∀𝑟 ∈ (𝑚(,)+∞)𝜒 |
137 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑟ℕ |
138 | 136, 137 | nfrab 3123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑟{𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} |
139 | 11, 138 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟𝑀 |
140 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟ℝ |
141 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑟
< |
142 | 139, 140,
141 | nfinf 8388 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑟inf(𝑀, ℝ, < ) |
143 | 135, 142 | nfmpt 4746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑟(𝑖 ∈ 𝐴 ↦ inf(𝑀, ℝ, < )) |
144 | 27, 143 | nfcxfr 2762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑉 |
145 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑟𝑖 |
146 | 144, 145 | nffv 6198 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(𝑉‘𝑖) |
147 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟(,) |
148 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑟+∞ |
149 | 146, 147,
148 | nfov 6676 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑟((𝑉‘𝑖)(,)+∞) |
150 | 134, 149 | raleqf 3134 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚(,)+∞) = ((𝑉‘𝑖)(,)+∞) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
151 | 133, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (𝑉‘𝑖) → (∀𝑟 ∈ (𝑚(,)+∞)𝜒 ↔ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
152 | 132, 151 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒) ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
153 | 131, 152 | bibi12d 335 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑉‘𝑖) → ((𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) ↔ ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)))) |
154 | | rabid 3116 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ (𝑚 ∈ ℕ ∧ ∀𝑟 ∈ (𝑚(,)+∞)𝜒)) |
155 | 121, 130,
153, 154 | vtoclgf 3264 |
. . . . . . . . . . . . . 14
⊢ ((𝑉‘𝑖) ∈ ℕ → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
156 | 84, 155 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ {𝑚 ∈ ℕ ∣ ∀𝑟 ∈ (𝑚(,)+∞)𝜒} ↔ ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒))) |
157 | 111, 156 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ((𝑉‘𝑖) ∈ ℕ ∧ ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒)) |
158 | 157 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐴) → ∀𝑟 ∈ ((𝑉‘𝑖)(,)+∞)𝜒) |
159 | 158 | r19.21bi 2932 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ ((𝑉‘𝑖)(,)+∞)) → 𝜒) |
160 | 109, 159 | syldan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐴) ∧ 𝑟 ∈ (𝑁(,)+∞)) → 𝜒) |
161 | 160 | an32s 846 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) ∧ 𝑖 ∈ 𝐴) → 𝜒) |
162 | 161 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → (𝑖 ∈ 𝐴 → 𝜒)) |
163 | 74, 162 | ralrimi 2957 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝑁(,)+∞)) → ∀𝑖 ∈ 𝐴 𝜒) |
164 | 163 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑟 ∈ (𝑁(,)+∞) → ∀𝑖 ∈ 𝐴 𝜒)) |
165 | 65, 164 | ralrimi 2957 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
166 | 165 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
167 | | oveq1 6657 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛(,)+∞) = (𝑁(,)+∞)) |
168 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑟(𝑛(,)+∞) |
169 | 144 | nfrn 5368 |
. . . . . . . . 9
⊢
Ⅎ𝑟ran
𝑉 |
170 | 169, 140,
141 | nfsup 8357 |
. . . . . . . 8
⊢
Ⅎ𝑟sup(ran 𝑉, ℝ, < ) |
171 | 9, 170 | nfcxfr 2762 |
. . . . . . 7
⊢
Ⅎ𝑟𝑁 |
172 | 171, 147,
148 | nfov 6676 |
. . . . . 6
⊢
Ⅎ𝑟(𝑁(,)+∞) |
173 | 168, 172 | raleqf 3134 |
. . . . 5
⊢ ((𝑛(,)+∞) = (𝑁(,)+∞) →
(∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
174 | 167, 173 | syl 17 |
. . . 4
⊢ (𝑛 = 𝑁 → (∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒 ↔ ∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒)) |
175 | 174 | rspcev 3309 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧
∀𝑟 ∈ (𝑁(,)+∞)∀𝑖 ∈ 𝐴 𝜒) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
176 | 64, 166, 175 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 = ∅) → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |
177 | 8, 176 | pm2.61dan 832 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑟 ∈ (𝑛(,)+∞)∀𝑖 ∈ 𝐴 𝜒) |