Metamath Proof Explorer

Theorem incsequz2

Description: An increasing sequence of positive integers takes on indefinitely large values. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion incsequz2 ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 incsequz ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
2 nnssre ⊢ ℕ ⊆ ℝ
3 ltso ⊢ < Or ℝ
4 sopo ⊢ ( < Or ℝ → < Po ℝ )
5 3 4 ax-mp ⊢ < Po ℝ
6 poss ⊢ ( ℕ ⊆ ℝ → ( < Po ℝ → < Po ℕ ) )
7 2 5 6 mp2 ⊢ < Po ℕ
8 seqpo ⊢ ( ( < Po ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) → ( ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ↔ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) )
9 7 8 mpan ⊢ ( 𝐹 : ℕ ⟶ ℕ → ( ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ↔ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) )
10 9 biimpd ⊢ ( 𝐹 : ℕ ⟶ ℕ → ( ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) → ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) )
11 10 imdistani ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) )
12 uzp1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) → ( 𝑘 = 𝑛 ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) )
13 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
14 13 adantl ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
15 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℕ )
16 15 nnzd ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℤ )
17 uzid ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ℤ → ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
18 16 17 syl ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
19 18 adantr ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
20 14 19 eqeltrd ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
21 20 adantllr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
22 fvoveq1 ⊢ ( 𝑝 = 𝑛 → ( ℤ≥ ‘ ( 𝑝 + 1 ) ) = ( ℤ≥ ‘ ( 𝑛 + 1 ) ) )
23 fveq2 ⊢ ( 𝑝 = 𝑛 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑛 ) )
24 23 breq1d ⊢ ( 𝑝 = 𝑛 → ( ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ↔ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑞 ) ) )
25 22 24 raleqbidv ⊢ ( 𝑝 = 𝑛 → ( ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ↔ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑞 ) ) )
26 25 rspccva ⊢ ( ( ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑞 ) )
27 fveq2 ⊢ ( 𝑞 = 𝑘 → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑘 ) )
28 27 breq2d ⊢ ( 𝑞 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑞 ) ↔ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) ) )
29 28 rspccva ⊢ ( ( ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑞 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) )
30 26 29 sylan ⊢ ( ( ( ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) )
31 30 adantlll ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) )
32 16 adantr ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℤ )
33 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
34 elnnuz ⊢ ( ( 𝑛 + 1 ) ∈ ℕ ↔ ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
35 33 34 sylib ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
36 uztrn ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ∧ ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
37 36 ancoms ⊢ ( ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
38 elnnuz ⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
39 37 38 sylibr ⊢ ( ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ )
40 35 39 sylan ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → 𝑘 ∈ ℕ )
41 ffvelrn ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℕ )
42 41 nnzd ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
43 40 42 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
44 43 anassrs ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℤ )
45 zre ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ℤ → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
46 zre ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ℤ → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
47 ltle ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
48 45 46 47 syl2an ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℤ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
49 eluz ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℤ ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( 𝐹 ‘ 𝑛 ) ≤ ( 𝐹 ‘ 𝑘 ) ) )
50 48 49 sylibrd ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℤ ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℤ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
51 32 44 50 syl2anc ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
52 51 adantllr ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) ) )
53 31 52 mpd ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
54 21 53 jaodan ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑘 = 𝑛 ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑛 + 1 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
55 12 54 sylan2 ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) )
56 uztrn ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) ∧ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) )
57 56 ex ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
58 55 57 syl ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
59 58 adantllr ⊢ ( ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝐴 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
60 59 ralrimdva ⊢ ( ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝐴 ∈ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
61 60 ex ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑝 ∈ ℕ ∀ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑝 + 1 ) ) ( 𝐹 ‘ 𝑝 ) < ( 𝐹 ‘ 𝑞 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝑛 ∈ ℕ → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) ) )
62 11 61 stoic3 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝑛 ∈ ℕ → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) ) )
63 62 reximdvai ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
64 1 63 mpd ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑛 ) ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ 𝐴 ) )