incsequz - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > incsequz		Structured version Visualization version GIF version

Theorem incsequz 36920

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

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

Distinct variable groups: 𝑚,𝐹,𝑛 𝐴,𝑚,𝑛

Proof of Theorem incsequz Dummy variables 𝑘 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6891	. . . . . . 7 ⊢ (𝑝 = 1 → (ℤ_≥‘𝑝) = (ℤ_≥‘1))
2	1	eleq2d 2818	. . . . . 6 ⊢ (𝑝 = 1 → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘1)))
3	2	rexbidv 3177	. . . . 5 ⊢ (𝑝 = 1 → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1)))
4	3	imbi2d 340	. . . 4 ⊢ (𝑝 = 1 → (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝)) ↔ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1))))
5		fveq2 6891	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (ℤ_≥‘𝑝) = (ℤ_≥‘𝑞))
6	5	eleq2d 2818	. . . . . 6 ⊢ (𝑝 = 𝑞 → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞)))
7	6	rexbidv 3177	. . . . 5 ⊢ (𝑝 = 𝑞 → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞)))
8	7	imbi2d 340	. . . 4 ⊢ (𝑝 = 𝑞 → (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝)) ↔ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞))))
9		fveq2 6891	. . . . . . 7 ⊢ (𝑝 = (𝑞 + 1) → (ℤ_≥‘𝑝) = (ℤ_≥‘(𝑞 + 1)))
10	9	eleq2d 2818	. . . . . 6 ⊢ (𝑝 = (𝑞 + 1) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1))))
11	10	rexbidv 3177	. . . . 5 ⊢ (𝑝 = (𝑞 + 1) → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1))))
12	11	imbi2d 340	. . . 4 ⊢ (𝑝 = (𝑞 + 1) → (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝)) ↔ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1)))))
13		fveq2 6891	. . . . . . 7 ⊢ (𝑝 = 𝐴 → (ℤ_≥‘𝑝) = (ℤ_≥‘𝐴))
14	13	eleq2d 2818	. . . . . 6 ⊢ (𝑝 = 𝐴 → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴)))
15	14	rexbidv 3177	. . . . 5 ⊢ (𝑝 = 𝐴 → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝) ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴)))
16	15	imbi2d 340	. . . 4 ⊢ (𝑝 = 𝐴 → (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑝)) ↔ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴))))
17		1nn 12228	. . . . . . 7 ⊢ 1 ∈ ℕ
18	17	ne0ii 4337	. . . . . 6 ⊢ ℕ ≠ ∅
19		ffvelcdm 7083	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℕ)
20		elnnuz 12871	. . . . . . . 8 ⊢ ((𝐹‘𝑛) ∈ ℕ ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘1))
21	19, 20	sylib 217	. . . . . . 7 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℤ_≥‘1))
22	21	ralrimiva 3145	. . . . . 6 ⊢ (𝐹:ℕ⟶ℕ → ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1))
23		r19.2z 4494	. . . . . 6 ⊢ ((ℕ ≠ ∅ ∧ ∀𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1)) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1))
24	18, 22, 23	sylancr 586	. . . . 5 ⊢ (𝐹:ℕ⟶ℕ → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1))
25	24	adantr 480	. . . 4 ⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘1))
26		peano2nn 12229	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
27	26	adantl 481	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
28		nnre 12224	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ ℕ → 𝑞 ∈ ℝ)
29	28	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → 𝑞 ∈ ℝ)
30	19	nnred 12232	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ)
31	30	adantlr 712	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ)
32	31	adantll 711	. . . . . . . . . . . 12 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℝ)
33		1red 11220	. . . . . . . . . . . 12 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → 1 ∈ ℝ)
34	29, 32, 33	leadd1d 11813	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → (𝑞 ≤ (𝐹‘𝑛) ↔ (𝑞 + 1) ≤ ((𝐹‘𝑛) + 1)))
35		fveq2 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛))
36		fvoveq1 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 = 𝑛 → (𝐹‘(𝑚 + 1)) = (𝐹‘(𝑛 + 1)))
37	35, 36	breq12d 5161	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ↔ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))))
38	37	rspcv 3608	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) → (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))))
39	38	imdistani 568	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → (𝑛 ∈ ℕ ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))))
40		ffvelcdm 7083	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹:ℕ⟶ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℕ)
41	26, 40	sylan2 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℕ)
42		nnltp1le 12623	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑛) ∈ ℕ ∧ (𝐹‘(𝑛 + 1)) ∈ ℕ) → ((𝐹‘𝑛) < (𝐹‘(𝑛 + 1)) ↔ ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1))))
43	19, 41, 42	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) < (𝐹‘(𝑛 + 1)) ↔ ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1))))
44	43	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1))) → ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1)))
45	44	anasss 466	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶ℕ ∧ (𝑛 ∈ ℕ ∧ (𝐹‘𝑛) < (𝐹‘(𝑛 + 1)))) → ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1)))
46	39, 45	sylan2 592	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶ℕ ∧ (𝑛 ∈ ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) → ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1)))
47	46	anass1rs 652	. . . . . . . . . . . . 13 ⊢ (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1)))
48	47	adantll 711	. . . . . . . . . . . 12 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1)))
49		peano2re 11392	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ ℝ → (𝑞 + 1) ∈ ℝ)
50	28, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℕ → (𝑞 + 1) ∈ ℝ)
51	50	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝑞 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) ∧ 𝑛 ∈ ℕ) → (𝑞 + 1) ∈ ℝ)
52		peano2nn 12229	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑛) ∈ ℕ → ((𝐹‘𝑛) + 1) ∈ ℕ)
53	19, 52	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) + 1) ∈ ℕ)
54	53	nnred 12232	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) + 1) ∈ ℝ)
55	54	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝑞 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) + 1) ∈ ℝ)
56	40	nnred 12232	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:ℕ⟶ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℝ)
57	26, 56	sylan2 592	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℝ)
58	57	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝑞 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℝ)
59		letr 11313	. . . . . . . . . . . . . 14 ⊢ (((𝑞 + 1) ∈ ℝ ∧ ((𝐹‘𝑛) + 1) ∈ ℝ ∧ (𝐹‘(𝑛 + 1)) ∈ ℝ) → (((𝑞 + 1) ≤ ((𝐹‘𝑛) + 1) ∧ ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1))) → (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
60	51, 55, 58, 59	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝑞 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) ∧ 𝑛 ∈ ℕ) → (((𝑞 + 1) ≤ ((𝐹‘𝑛) + 1) ∧ ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1))) → (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
61	60	adantlrr 718	. . . . . . . . . . . 12 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → (((𝑞 + 1) ≤ ((𝐹‘𝑛) + 1) ∧ ((𝐹‘𝑛) + 1) ≤ (𝐹‘(𝑛 + 1))) → (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
62	48, 61	mpan2d 691	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝑞 + 1) ≤ ((𝐹‘𝑛) + 1) → (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
63	34, 62	sylbid 239	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → (𝑞 ≤ (𝐹‘𝑛) → (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
64		nnz 12584	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ ℕ → 𝑞 ∈ ℤ)
65	19	nnzd 12590	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ ℤ)
66		eluz 12841	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℤ ∧ (𝐹‘𝑛) ∈ ℤ) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) ↔ 𝑞 ≤ (𝐹‘𝑛)))
67	64, 65, 66	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) ↔ 𝑞 ≤ (𝐹‘𝑛)))
68	67	adantrlr 720	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℕ ∧ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) ∧ 𝑛 ∈ ℕ)) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) ↔ 𝑞 ≤ (𝐹‘𝑛)))
69	68	anassrs 467	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) ↔ 𝑞 ≤ (𝐹‘𝑛)))
70	64	peano2zd 12674	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ ℕ → (𝑞 + 1) ∈ ℤ)
71	40	nnzd 12590	. . . . . . . . . . . . . 14 ⊢ ((𝐹:ℕ⟶ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℤ)
72	26, 71	sylan2 592	. . . . . . . . . . . . 13 ⊢ ((𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ) → (𝐹‘(𝑛 + 1)) ∈ ℤ)
73		eluz 12841	. . . . . . . . . . . . 13 ⊢ (((𝑞 + 1) ∈ ℤ ∧ (𝐹‘(𝑛 + 1)) ∈ ℤ) → ((𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
74	70, 72, 73	syl2an 595	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ 𝑛 ∈ ℕ)) → ((𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
75	74	adantrlr 720	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℕ ∧ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) ∧ 𝑛 ∈ ℕ)) → ((𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
76	75	anassrs 467	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝑞 + 1) ≤ (𝐹‘(𝑛 + 1))))
77	63, 69, 76	3imtr4d 294	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) → (𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1))))
78		fveq2 6891	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑛 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑛 + 1)))
79	78	eleq1d 2817	. . . . . . . . . 10 ⊢ (𝑘 = (𝑛 + 1) → ((𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1))))
80	79	rspcev 3612	. . . . . . . . 9 ⊢ (((𝑛 + 1) ∈ ℕ ∧ (𝐹‘(𝑛 + 1)) ∈ (ℤ_≥‘(𝑞 + 1))) → ∃𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1)))
81	27, 77, 80	syl6an 681	. . . . . . . 8 ⊢ (((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) → ∃𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1))))
82	81	rexlimdva 3154	. . . . . . 7 ⊢ ((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) → ∃𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1))))
83		fveq2 6891	. . . . . . . . 9 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
84	83	eleq1d 2817	. . . . . . . 8 ⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1))))
85	84	cbvrexvw 3234	. . . . . . 7 ⊢ (∃𝑘 ∈ ℕ (𝐹‘𝑘) ∈ (ℤ_≥‘(𝑞 + 1)) ↔ ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1)))
86	82, 85	imbitrdi 250	. . . . . 6 ⊢ ((𝑞 ∈ ℕ ∧ (𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)))) → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1))))
87	86	ex 412	. . . . 5 ⊢ (𝑞 ∈ ℕ → ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → (∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1)))))
88	87	a2d 29	. . . 4 ⊢ (𝑞 ∈ ℕ → (((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝑞)) → ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘(𝑞 + 1)))))
89	4, 8, 12, 16, 25, 88	nnind 12235	. . 3 ⊢ (𝐴 ∈ ℕ → ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴)))
90	89	com12 32	. 2 ⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1))) → (𝐴 ∈ ℕ → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴)))
91	90	3impia 1116	1 ⊢ ((𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ ℕ (𝐹‘𝑚) < (𝐹‘(𝑚 + 1)) ∧ 𝐴 ∈ ℕ) → ∃𝑛 ∈ ℕ (𝐹‘𝑛) ∈ (ℤ_≥‘𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 ∅c0 4322 class class class wbr 5148 ⟶wf 6539 ‘cfv 6543 (class class class)co 7412 ℝcr 11112 1c1 11114 + caddc 11116 < clt 11253 ≤ cle 11254 ℕcn 12217 ℤcz 12563 ℤ_≥cuz 12827

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7728 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7859 df-2nd 7979 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-er 8706 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-nn 12218 df-n0 12478 df-z 12564 df-uz 12828

This theorem is referenced by: incsequz2 36921

W3C validator