Step | Hyp | Ref
| Expression |
1 | | incsequz 33544 |
. 2
⊢ ((𝐹:ℕ⟶ℕ ∧
∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴)) |
2 | | nnssre 11024 |
. . . . . . . 8
⊢ ℕ
⊆ ℝ |
3 | | ltso 10118 |
. . . . . . . . 9
⊢ < Or
ℝ |
4 | | sopo 5052 |
. . . . . . . . 9
⊢ ( < Or
ℝ → < Po ℝ) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
⊢ < Po
ℝ |
6 | | poss 5037 |
. . . . . . . 8
⊢ (ℕ
⊆ ℝ → ( < Po ℝ → < Po
ℕ)) |
7 | 2, 5, 6 | mp2 9 |
. . . . . . 7
⊢ < Po
ℕ |
8 | | seqpo 33543 |
. . . . . . 7
⊢ (( <
Po ℕ ∧ 𝐹:ℕ⟶ℕ) →
(∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ↔ ∀𝑝 ∈ ℕ ∀𝑞 ∈ (ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞))) |
9 | 7, 8 | mpan 706 |
. . . . . 6
⊢ (𝐹:ℕ⟶ℕ →
(∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ↔ ∀𝑝 ∈ ℕ ∀𝑞 ∈ (ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞))) |
10 | 9 | biimpd 219 |
. . . . 5
⊢ (𝐹:ℕ⟶ℕ →
(∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) → ∀𝑝 ∈ ℕ ∀𝑞 ∈ (ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞))) |
11 | 10 | imdistani 726 |
. . . 4
⊢ ((𝐹:ℕ⟶ℕ ∧
∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → (𝐹:ℕ⟶ℕ ∧ ∀𝑝 ∈ ℕ ∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞))) |
12 | | uzp1 11721 |
. . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘𝑛) → (𝑘 = 𝑛 ∨ 𝑘 ∈ (ℤ≥‘(𝑛 + 1)))) |
13 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
14 | 13 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 = 𝑛) → (𝐹‘𝑘) = (𝐹‘𝑛)) |
15 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ∈ ℕ) |
16 | 15 | nnzd 11481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ∈ ℤ) |
17 | | uzid 11702 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑛) ∈ ℤ → (𝐹‘𝑛) ∈ (ℤ≥‘(𝐹‘𝑛))) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) →
(𝐹‘𝑛) ∈ (ℤ≥‘(𝐹‘𝑛))) |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 = 𝑛) → (𝐹‘𝑛) ∈ (ℤ≥‘(𝐹‘𝑛))) |
20 | 14, 19 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 = 𝑛) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛))) |
21 | 20 | adantllr 755 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛))) |
22 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑛 → (𝑝 + 1) = (𝑛 + 1)) |
23 | 22 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑛 → (ℤ≥‘(𝑝 + 1)) =
(ℤ≥‘(𝑛 + 1))) |
24 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑛 → (𝐹‘𝑝) = (𝐹‘𝑛)) |
25 | 24 | breq1d 4663 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑛 → ((𝐹‘𝑝) < (𝐹‘𝑞) ↔ (𝐹‘𝑛) < (𝐹‘𝑞))) |
26 | 23, 25 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑛 → (∀𝑞 ∈ (ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞) ↔ ∀𝑞 ∈ (ℤ≥‘(𝑛 + 1))(𝐹‘𝑛) < (𝐹‘𝑞))) |
27 | 26 | rspccva 3308 |
. . . . . . . . . . . . 13
⊢
((∀𝑝 ∈
ℕ ∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞) ∧ 𝑛 ∈ ℕ) → ∀𝑞 ∈
(ℤ≥‘(𝑛 + 1))(𝐹‘𝑛) < (𝐹‘𝑞)) |
28 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑘 → (𝐹‘𝑞) = (𝐹‘𝑘)) |
29 | 28 | breq2d 4665 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑘 → ((𝐹‘𝑛) < (𝐹‘𝑞) ↔ (𝐹‘𝑛) < (𝐹‘𝑘))) |
30 | 29 | rspccva 3308 |
. . . . . . . . . . . . 13
⊢
((∀𝑞 ∈
(ℤ≥‘(𝑛 + 1))(𝐹‘𝑛) < (𝐹‘𝑞) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑛) < (𝐹‘𝑘)) |
31 | 27, 30 | sylan 488 |
. . . . . . . . . . . 12
⊢
(((∀𝑝 ∈
ℕ ∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑛) < (𝐹‘𝑘)) |
32 | 31 | adantlll 754 |
. . . . . . . . . . 11
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑛) < (𝐹‘𝑘)) |
33 | 16 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑛) ∈ ℤ) |
34 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
ℕ) |
35 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 + 1) ∈ ℕ ↔
(𝑛 + 1) ∈
(ℤ≥‘1)) |
36 | 34, 35 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈
(ℤ≥‘1)) |
37 | | uztrn 11704 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈
(ℤ≥‘(𝑛 + 1)) ∧ (𝑛 + 1) ∈
(ℤ≥‘1)) → 𝑘 ∈
(ℤ≥‘1)) |
38 | 37 | ancoms 469 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑛 + 1) ∈
(ℤ≥‘1) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈
(ℤ≥‘1)) |
39 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 + 1) ∈
(ℤ≥‘1) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈
ℕ) |
41 | 36, 40 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ) |
42 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ℕ⟶ℕ ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ ℕ) |
43 | 42 | nnzd 11481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ℕ⟶ℕ ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ ℤ) |
44 | 41, 43 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶ℕ ∧
(𝑛 ∈ ℕ ∧
𝑘 ∈
(ℤ≥‘(𝑛 + 1)))) → (𝐹‘𝑘) ∈ ℤ) |
45 | 44 | anassrs 680 |
. . . . . . . . . . . . 13
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑘) ∈ ℤ) |
46 | | zre 11381 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑛) ∈ ℤ → (𝐹‘𝑛) ∈ ℝ) |
47 | | zre 11381 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑘) ∈ ℤ → (𝐹‘𝑘) ∈ ℝ) |
48 | | ltle 10126 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑛) ∈ ℝ ∧ (𝐹‘𝑘) ∈ ℝ) → ((𝐹‘𝑛) < (𝐹‘𝑘) → (𝐹‘𝑛) ≤ (𝐹‘𝑘))) |
49 | 46, 47, 48 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛) ∈ ℤ ∧ (𝐹‘𝑘) ∈ ℤ) → ((𝐹‘𝑛) < (𝐹‘𝑘) → (𝐹‘𝑛) ≤ (𝐹‘𝑘))) |
50 | | eluz 11701 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑛) ∈ ℤ ∧ (𝐹‘𝑘) ∈ ℤ) → ((𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)) ↔ (𝐹‘𝑛) ≤ (𝐹‘𝑘))) |
51 | 49, 50 | sylibrd 249 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑛) ∈ ℤ ∧ (𝐹‘𝑘) ∈ ℤ) → ((𝐹‘𝑛) < (𝐹‘𝑘) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)))) |
52 | 33, 45, 51 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐹:ℕ⟶ℕ ∧
𝑛 ∈ ℕ) ∧
𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → ((𝐹‘𝑛) < (𝐹‘𝑘) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)))) |
53 | 52 | adantllr 755 |
. . . . . . . . . . 11
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → ((𝐹‘𝑛) < (𝐹‘𝑘) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)))) |
54 | 32, 53 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛))) |
55 | 21, 54 | jaodan 826 |
. . . . . . . . 9
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ (𝑘 = 𝑛 ∨ 𝑘 ∈ (ℤ≥‘(𝑛 + 1)))) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛))) |
56 | 12, 55 | sylan2 491 |
. . . . . . . 8
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛))) |
57 | | uztrn 11704 |
. . . . . . . . 9
⊢ (((𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)) ∧ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴)) → (𝐹‘𝑘) ∈ (ℤ≥‘𝐴)) |
58 | 57 | ex 450 |
. . . . . . . 8
⊢ ((𝐹‘𝑘) ∈ (ℤ≥‘(𝐹‘𝑛)) → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → (𝐹‘𝑘) ∈ (ℤ≥‘𝐴))) |
59 | 56, 58 | syl 17 |
. . . . . . 7
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → (𝐹‘𝑘) ∈ (ℤ≥‘𝐴))) |
60 | 59 | adantllr 755 |
. . . . . 6
⊢
(((((𝐹:ℕ⟶ℕ ∧ ∀𝑝 ∈ ℕ ∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝐴 ∈ ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → (𝐹‘𝑘) ∈ (ℤ≥‘𝐴))) |
61 | 60 | ralrimdva 2969 |
. . . . 5
⊢ ((((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝐴 ∈ ℕ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴))) |
62 | 61 | ex 450 |
. . . 4
⊢ (((𝐹:ℕ⟶ℕ ∧
∀𝑝 ∈ ℕ
∀𝑞 ∈
(ℤ≥‘(𝑝 + 1))(𝐹‘𝑝) < (𝐹‘𝑞)) ∧ 𝐴 ∈ ℕ) → (𝑛 ∈ ℕ → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)))) |
63 | 11, 62 | stoic3 1701 |
. . 3
⊢ ((𝐹:ℕ⟶ℕ ∧
∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → (𝑛 ∈ ℕ → ((𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)))) |
64 | 63 | reximdvai 3015 |
. 2
⊢ ((𝐹:ℕ⟶ℕ ∧
∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ≥‘𝐴) → ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴))) |
65 | 1, 64 | mpd 15 |
1
⊢ ((𝐹:ℕ⟶ℕ ∧
∀𝑚 ∈ ℕ
(𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(𝐹‘𝑘) ∈ (ℤ≥‘𝐴)) |