Step | Hyp | Ref
| Expression |
1 | | nninfdclemf.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
2 | | nninfdclemf.dc |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) |
3 | | nninfdclemf.nb |
. . . . . 6
⊢ (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) |
4 | | nninfdclemf.j |
. . . . . 6
⊢ (𝜑 → (𝐽 ∈ 𝐴 ∧ 1 < 𝐽)) |
5 | | nninfdclemf.f |
. . . . . 6
⊢ 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽)) |
6 | 1, 2, 3, 4, 5 | nninfdclemf 12376 |
. . . . 5
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
7 | | nninfdclemp1.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ ℕ) |
8 | 6, 7 | ffvelrnd 5618 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑈) ∈ 𝐴) |
9 | 1, 8 | sseldd 3141 |
. . 3
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℕ) |
10 | 9 | nnred 8864 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℝ) |
11 | 9 | nnzd 9306 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑈) ∈ ℤ) |
12 | 11 | peano2zd 9310 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) + 1) ∈ ℤ) |
13 | 12 | zred 9307 |
. 2
⊢ (𝜑 → ((𝐹‘𝑈) + 1) ∈ ℝ) |
14 | 7 | peano2nnd 8866 |
. . . . 5
⊢ (𝜑 → (𝑈 + 1) ∈ ℕ) |
15 | 6, 14 | ffvelrnd 5618 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑈 + 1)) ∈ 𝐴) |
16 | 1, 15 | sseldd 3141 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℕ) |
17 | 16 | nnred 8864 |
. 2
⊢ (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℝ) |
18 | 10 | ltp1d 8819 |
. 2
⊢ (𝜑 → (𝐹‘𝑈) < ((𝐹‘𝑈) + 1)) |
19 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) → 𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
20 | 19 | elin2d 3310 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) → 𝑟 ∈ (ℤ≥‘((𝐹‘𝑈) + 1))) |
21 | | eluzle 9472 |
. . . . . 6
⊢ (𝑟 ∈
(ℤ≥‘((𝐹‘𝑈) + 1)) → ((𝐹‘𝑈) + 1) ≤ 𝑟) |
22 | 20, 21 | syl 14 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) → ((𝐹‘𝑈) + 1) ≤ 𝑟) |
23 | 22 | ralrimiva 2537 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))((𝐹‘𝑈) + 1) ≤ 𝑟) |
24 | | inss1 3340 |
. . . . . . 7
⊢ (𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1))) ⊆ 𝐴 |
25 | 24, 1 | sstrid 3151 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ⊆ ℕ) |
26 | | eleq1w 2225 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
27 | 26 | dcbid 828 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑎 ∈ 𝐴)) |
28 | 2 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) |
29 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℕ) |
30 | 27, 28, 29 | rspcdva 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → DECID
𝑎 ∈ 𝐴) |
31 | 29 | nnzd 9306 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℤ) |
32 | | eluzdc 9542 |
. . . . . . . . . 10
⊢ ((((𝐹‘𝑈) + 1) ∈ ℤ ∧ 𝑎 ∈ ℤ) →
DECID 𝑎
∈ (ℤ≥‘((𝐹‘𝑈) + 1))) |
33 | 12, 31, 32 | syl2an2r 585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → DECID
𝑎 ∈
(ℤ≥‘((𝐹‘𝑈) + 1))) |
34 | | dcan 923 |
. . . . . . . . 9
⊢
(DECID 𝑎 ∈ 𝐴 → (DECID 𝑎 ∈
(ℤ≥‘((𝐹‘𝑈) + 1)) → DECID (𝑎 ∈ 𝐴 ∧ 𝑎 ∈ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
35 | 30, 33, 34 | sylc 62 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → DECID
(𝑎 ∈ 𝐴 ∧ 𝑎 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
36 | | elin 3303 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ (𝑎 ∈ 𝐴 ∧ 𝑎 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
37 | 36 | dcbii 830 |
. . . . . . . 8
⊢
(DECID 𝑎 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ DECID (𝑎 ∈ 𝐴 ∧ 𝑎 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
38 | 35, 37 | sylibr 133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → DECID
𝑎 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
39 | 38 | ralrimiva 2537 |
. . . . . 6
⊢ (𝜑 → ∀𝑎 ∈ ℕ DECID 𝑎 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
40 | | breq1 3982 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝐹‘𝑈) → (𝑚 < 𝑛 ↔ (𝐹‘𝑈) < 𝑛)) |
41 | 40 | rexbidv 2465 |
. . . . . . . . . 10
⊢ (𝑚 = (𝐹‘𝑈) → (∃𝑛 ∈ 𝐴 𝑚 < 𝑛 ↔ ∃𝑛 ∈ 𝐴 (𝐹‘𝑈) < 𝑛)) |
42 | 41, 3, 9 | rspcdva 2833 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑛 ∈ 𝐴 (𝐹‘𝑈) < 𝑛) |
43 | | breq2 3983 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑏 → ((𝐹‘𝑈) < 𝑛 ↔ (𝐹‘𝑈) < 𝑏)) |
44 | 43 | cbvrexv 2691 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
𝐴 (𝐹‘𝑈) < 𝑛 ↔ ∃𝑏 ∈ 𝐴 (𝐹‘𝑈) < 𝑏) |
45 | 42, 44 | sylib 121 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑏 ∈ 𝐴 (𝐹‘𝑈) < 𝑏) |
46 | | df-rex 2448 |
. . . . . . . 8
⊢
(∃𝑏 ∈
𝐴 (𝐹‘𝑈) < 𝑏 ↔ ∃𝑏(𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) |
47 | 45, 46 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → ∃𝑏(𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) |
48 | | simprl 521 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝑏 ∈ 𝐴) |
49 | 12 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → ((𝐹‘𝑈) + 1) ∈ ℤ) |
50 | 1 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝐴 ⊆ ℕ) |
51 | 50, 48 | sseldd 3141 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝑏 ∈ ℕ) |
52 | 51 | nnzd 9306 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝑏 ∈ ℤ) |
53 | | simprr 522 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → (𝐹‘𝑈) < 𝑏) |
54 | | nnltp1le 9245 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑈) ∈ ℕ ∧ 𝑏 ∈ ℕ) → ((𝐹‘𝑈) < 𝑏 ↔ ((𝐹‘𝑈) + 1) ≤ 𝑏)) |
55 | 9, 51, 54 | syl2an2r 585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → ((𝐹‘𝑈) < 𝑏 ↔ ((𝐹‘𝑈) + 1) ≤ 𝑏)) |
56 | 53, 55 | mpbid 146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → ((𝐹‘𝑈) + 1) ≤ 𝑏) |
57 | | eluz2 9466 |
. . . . . . . . . . 11
⊢ (𝑏 ∈
(ℤ≥‘((𝐹‘𝑈) + 1)) ↔ (((𝐹‘𝑈) + 1) ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ ((𝐹‘𝑈) + 1) ≤ 𝑏)) |
58 | 49, 52, 56, 57 | syl3anbrc 1170 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝑏 ∈ (ℤ≥‘((𝐹‘𝑈) + 1))) |
59 | 48, 58 | elind 3305 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏)) → 𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
60 | 59 | ex 114 |
. . . . . . . 8
⊢ (𝜑 → ((𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏) → 𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
61 | 60 | eximdv 1867 |
. . . . . . 7
⊢ (𝜑 → (∃𝑏(𝑏 ∈ 𝐴 ∧ (𝐹‘𝑈) < 𝑏) → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
62 | 47, 61 | mpd 13 |
. . . . . 6
⊢ (𝜑 → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
63 | 25, 39, 62 | nninfdcex 11880 |
. . . . 5
⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑟 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))𝑟 < 𝑏))) |
64 | | nnssre 8855 |
. . . . . 6
⊢ ℕ
⊆ ℝ |
65 | 25, 64 | sstrdi 3152 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ⊆ ℝ) |
66 | 63, 65, 13 | infregelbex 9530 |
. . . 4
⊢ (𝜑 → (((𝐹‘𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) ↔
∀𝑟 ∈ (𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1)))((𝐹‘𝑈) + 1) ≤ 𝑟)) |
67 | 23, 66 | mpbird 166 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
68 | 5 | fveq1i 5484 |
. . . . 5
⊢ (𝐹‘(𝑈 + 1)) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1)) |
69 | | nnuz 9495 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
70 | 7, 69 | eleqtrdi 2257 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈
(ℤ≥‘1)) |
71 | | eqid 2164 |
. . . . . . . 8
⊢ (𝑖 ∈ ℕ ↦ 𝐽) = (𝑖 ∈ ℕ ↦ 𝐽) |
72 | | eqidd 2165 |
. . . . . . . 8
⊢ (𝑖 = 𝑝 → 𝐽 = 𝐽) |
73 | | elnnuz 9496 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℕ ↔ 𝑝 ∈
(ℤ≥‘1)) |
74 | 73 | biimpri 132 |
. . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘1) → 𝑝 ∈ ℕ) |
75 | 74 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘1))
→ 𝑝 ∈
ℕ) |
76 | 4 | simpld 111 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ 𝐴) |
77 | 76 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘1))
→ 𝐽 ∈ 𝐴) |
78 | 71, 72, 75, 77 | fvmptd3 5576 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑖 ∈ ℕ
↦ 𝐽)‘𝑝) = 𝐽) |
79 | 78, 77 | eqeltrd 2241 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (ℤ≥‘1))
→ ((𝑖 ∈ ℕ
↦ 𝐽)‘𝑝) ∈ 𝐴) |
80 | 1 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → 𝐴 ⊆ ℕ) |
81 | 2 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) |
82 | 3 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) |
83 | | simprl 521 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → 𝑝 ∈ 𝐴) |
84 | | simprr 522 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → 𝑞 ∈ 𝐴) |
85 | 80, 81, 82, 83, 84 | nninfdclemcl 12375 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴)) → (𝑝(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))𝑞) ∈ 𝐴) |
86 | 70, 79, 85 | seq3p1 10391 |
. . . . 5
⊢ (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1)))) |
87 | 68, 86 | syl5eq 2209 |
. . . 4
⊢ (𝜑 → (𝐹‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1)))) |
88 | 5 | fveq1i 5484 |
. . . . . . 7
⊢ (𝐹‘𝑈) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) |
89 | 88 | eqcomi 2168 |
. . . . . 6
⊢
(seq1((𝑦 ∈
ℕ, 𝑧 ∈ ℕ
↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹‘𝑈) |
90 | 89 | a1i 9 |
. . . . 5
⊢ (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹‘𝑈)) |
91 | | eqidd 2165 |
. . . . . 6
⊢ (𝑖 = (𝑈 + 1) → 𝐽 = 𝐽) |
92 | 71, 91, 14, 76 | fvmptd3 5576 |
. . . . 5
⊢ (𝜑 → ((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1)) = 𝐽) |
93 | 90, 92 | oveq12d 5857 |
. . . 4
⊢ (𝜑 → ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))) = ((𝐹‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))𝐽)) |
94 | 1, 76 | sseldd 3141 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ ℕ) |
95 | | eleq1w 2225 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑠 → (𝑥 ∈ 𝐴 ↔ 𝑠 ∈ 𝐴)) |
96 | 95 | dcbid 828 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑠 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑠 ∈ 𝐴)) |
97 | 2 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → ∀𝑥 ∈ ℕ
DECID 𝑥
∈ 𝐴) |
98 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → 𝑠 ∈ ℕ) |
99 | 96, 97, 98 | rspcdva 2833 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → DECID
𝑠 ∈ 𝐴) |
100 | 98 | nnzd 9306 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → 𝑠 ∈ ℤ) |
101 | | eluzdc 9542 |
. . . . . . . . . . . 12
⊢ ((((𝐹‘𝑈) + 1) ∈ ℤ ∧ 𝑠 ∈ ℤ) →
DECID 𝑠
∈ (ℤ≥‘((𝐹‘𝑈) + 1))) |
102 | 12, 100, 101 | syl2an2r 585 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → DECID
𝑠 ∈
(ℤ≥‘((𝐹‘𝑈) + 1))) |
103 | | dcan 923 |
. . . . . . . . . . 11
⊢
(DECID 𝑠 ∈ 𝐴 → (DECID 𝑠 ∈
(ℤ≥‘((𝐹‘𝑈) + 1)) → DECID (𝑠 ∈ 𝐴 ∧ 𝑠 ∈ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
104 | 99, 102, 103 | sylc 62 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → DECID
(𝑠 ∈ 𝐴 ∧ 𝑠 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
105 | | elin 3303 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ (𝑠 ∈ 𝐴 ∧ 𝑠 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
106 | 105 | dcbii 830 |
. . . . . . . . . 10
⊢
(DECID 𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ DECID (𝑠 ∈ 𝐴 ∧ 𝑠 ∈ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
107 | 104, 106 | sylibr 133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → DECID
𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
108 | 107 | ralrimiva 2537 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑠 ∈ ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
109 | | eleq1w 2225 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑥 → (𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ 𝑥 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
110 | 109 | dcbid 828 |
. . . . . . . . 9
⊢ (𝑠 = 𝑥 → (DECID 𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ DECID 𝑥 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))))) |
111 | 110 | cbvralv 2690 |
. . . . . . . 8
⊢
(∀𝑠 ∈
ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))) ↔ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
112 | 108, 111 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
113 | | nnmindc 11961 |
. . . . . . 7
⊢ (((𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1))) ⊆ ℕ ∧ ∀𝑥 ∈ ℕ
DECID 𝑥
∈ (𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1))) ∧ ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) → inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1)))) |
114 | 25, 112, 62, 113 | syl3anc 1227 |
. . . . . 6
⊢ (𝜑 → inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1)))) |
115 | 114 | elin1d 3309 |
. . . . 5
⊢ (𝜑 → inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) ∈ 𝐴) |
116 | | fvoveq1 5862 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑈) →
(ℤ≥‘(𝑦 + 1)) =
(ℤ≥‘((𝐹‘𝑈) + 1))) |
117 | 116 | ineq2d 3321 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑈) → (𝐴 ∩ (ℤ≥‘(𝑦 + 1))) = (𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1)))) |
118 | 117 | infeq1d 6971 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝑈) → inf((𝐴 ∩ (ℤ≥‘(𝑦 + 1))), ℝ, < ) =
inf((𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
119 | | eqidd 2165 |
. . . . . 6
⊢ (𝑧 = 𝐽 → inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) = inf((𝐴 ∩
(ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
120 | | eqid 2164 |
. . . . . 6
⊢ (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦
inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )) = (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦
inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < )) |
121 | 118, 119,
120 | ovmpog 5970 |
. . . . 5
⊢ (((𝐹‘𝑈) ∈ ℕ ∧ 𝐽 ∈ ℕ ∧ inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < ) ∈ 𝐴) → ((𝐹‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
122 | 9, 94, 115, 121 | syl3anc 1227 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩
(ℤ≥‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
123 | 87, 93, 122 | 3eqtrd 2201 |
. . 3
⊢ (𝜑 → (𝐹‘(𝑈 + 1)) = inf((𝐴 ∩ (ℤ≥‘((𝐹‘𝑈) + 1))), ℝ, < )) |
124 | 67, 123 | breqtrrd 4007 |
. 2
⊢ (𝜑 → ((𝐹‘𝑈) + 1) ≤ (𝐹‘(𝑈 + 1))) |
125 | 10, 13, 17, 18, 124 | ltletrd 8315 |
1
⊢ (𝜑 → (𝐹‘𝑈) < (𝐹‘(𝑈 + 1))) |