Metamath Proof Explorer

Theorem incsequz

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

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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑝 = 1 → ( ℤ≥ ‘ 𝑝 ) = ( ℤ≥ ‘ 1 ) )
2 1 eleq2d ⊢ ( 𝑝 = 1 → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) ) )
3 2 rexbidv ⊢ ( 𝑝 = 1 → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) ) )
4 3 imbi2d ⊢ ( 𝑝 = 1 → ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ) ↔ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) ) ) )
5 fveq2 ⊢ ( 𝑝 = 𝑞 → ( ℤ≥ ‘ 𝑝 ) = ( ℤ≥ ‘ 𝑞 ) )
6 5 eleq2d ⊢ ( 𝑝 = 𝑞 → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ) )
7 6 rexbidv ⊢ ( 𝑝 = 𝑞 → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ) )
8 7 imbi2d ⊢ ( 𝑝 = 𝑞 → ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ) ↔ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ) ) )
9 fveq2 ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ℤ≥ ‘ 𝑝 ) = ( ℤ≥ ‘ ( 𝑞 + 1 ) ) )
10 9 eleq2d ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
11 10 rexbidv ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
12 11 imbi2d ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ) ↔ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) ) )
13 fveq2 ⊢ ( 𝑝 = 𝐴 → ( ℤ≥ ‘ 𝑝 ) = ( ℤ≥ ‘ 𝐴 ) )
14 13 eleq2d ⊢ ( 𝑝 = 𝐴 → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
15 14 rexbidv ⊢ ( 𝑝 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
16 15 imbi2d ⊢ ( 𝑝 = 𝐴 → ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑝 ) ) ↔ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) ) )
17 1nn ⊢ 1 ∈ ℕ
18 17 ne0ii ⊢ ℕ ≠ ∅
19 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℕ )
20 elnnuz ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ℕ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
21 19 20 sylib ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
22 21 ralrimiva ⊢ ( 𝐹 : ℕ ⟶ ℕ → ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
23 r19.2z ⊢ ( ( ℕ ≠ ∅ ∧ ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
24 18 22 23 sylancr ⊢ ( 𝐹 : ℕ ⟶ ℕ → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
25 24 adantr ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 1 ) )
26 peano2nn ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
27 26 adantl ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
28 nnre ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℝ )
29 28 ad2antrr ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → 𝑞 ∈ ℝ )
30 19 nnred ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
31 30 adantlr ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
32 31 adantll ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
33 1red ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℝ )
34 29 32 33 leadd1d ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑞 + 1 ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ) )
35 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
36 fvoveq1 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ ( 𝑚 + 1 ) ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
37 35 36 breq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
38 37 rspcv ⊢ ( 𝑛 ∈ ℕ → ( ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) → ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
39 38 imdistani ⊢ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
40 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℕ )
41 26 40 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℕ )
42 nnltp1le ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∈ ℕ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
43 19 41 42 syl2anc ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
44 43 biimpa ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
45 44 anasss ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐹 ‘ 𝑛 ) < ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
46 39 45 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
47 46 anass1rs ⊢ ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
48 47 adantll ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
49 peano2re ⊢ ( 𝑞 ∈ ℝ → ( 𝑞 + 1 ) ∈ ℝ )
50 28 49 syl ⊢ ( 𝑞 ∈ ℕ → ( 𝑞 + 1 ) ∈ ℝ )
51 50 ad2antrr ⊢ ( ( ( 𝑞 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝑞 + 1 ) ∈ ℝ )
52 peano2nn ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ℕ → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℕ )
53 19 52 syl ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℕ )
54 53 nnred ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℝ )
55 54 adantll ⊢ ( ( ( 𝑞 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℝ )
56 40 nnred ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
57 26 56 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
58 57 adantll ⊢ ( ( ( 𝑞 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
59 letr ⊢ ( ( ( 𝑞 + 1 ) ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℝ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ ) → ( ( ( 𝑞 + 1 ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∧ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
60 51 55 58 59 syl3anc ⊢ ( ( ( 𝑞 ∈ ℕ ∧ 𝐹 : ℕ ⟶ ℕ ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑞 + 1 ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∧ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
61 60 adantlrr ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑞 + 1 ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∧ ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) → ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
62 48 61 mpan2d ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑞 + 1 ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) → ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
63 34 62 sylbid ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) → ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
64 nnz ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℤ )
65 19 nnzd ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℤ )
66 eluz ⊢ ( ( 𝑞 ∈ ℤ ∧ ( 𝐹 ‘ 𝑛 ) ∈ ℤ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ↔ 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) ) )
67 64 65 66 syl2an ⊢ ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ↔ 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) ) )
68 67 adantrlr ⊢ ( ( 𝑞 ∈ ℕ ∧ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ↔ 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) ) )
69 68 anassrs ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ↔ 𝑞 ≤ ( 𝐹 ‘ 𝑛 ) ) )
70 64 peano2zd ⊢ ( 𝑞 ∈ ℕ → ( 𝑞 + 1 ) ∈ ℤ )
71 40 nnzd ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℤ )
72 26 71 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℤ )
73 eluz ⊢ ( ( ( 𝑞 + 1 ) ∈ ℤ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℤ ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
74 70 72 73 syl2an ⊢ ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
75 74 adantrlr ⊢ ( ( 𝑞 ∈ ℕ ∧ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ∧ 𝑛 ∈ ℕ ) ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
76 75 anassrs ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝑞 + 1 ) ≤ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ) )
77 63 69 76 3imtr4d ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
78 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
79 78 eleq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
80 79 rspcev ⊢ ( ( ( 𝑛 + 1 ) ∈ ℕ ∧ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) → ∃ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) )
81 27 77 80 syl6an ⊢ ( ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) → ∃ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
82 81 rexlimdva ⊢ ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) → ∃ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
83 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
84 83 eleq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
85 84 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℕ ( 𝐹 ‘ 𝑘 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ↔ ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) )
86 82 85 imbitrdi ⊢ ( ( 𝑞 ∈ ℕ ∧ ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) )
87 86 ex ⊢ ( 𝑞 ∈ ℕ → ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ( ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) ) )
88 87 a2d ⊢ ( 𝑞 ∈ ℕ → ( ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝑞 ) ) → ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ ( 𝑞 + 1 ) ) ) ) )
89 4 8 12 16 25 88 nnind ⊢ ( 𝐴 ∈ ℕ → ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
90 89 com12 ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) → ( 𝐴 ∈ ℕ → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) ) )
91 90 3impia ⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ∀ 𝑚 ∈ ℕ ( 𝐹 ‘ 𝑚 ) < ( 𝐹 ‘ ( 𝑚 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ∃ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ∈ ( ℤ≥ ‘ 𝐴 ) )