Theorem incsequz 29831

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

Assertion

Ref	Expression
incsequz	|- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) /\ A e. NN ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) )

Distinct variable groups:   m, F, n   A, m, n

Proof of Theorem incsequz

Dummy variables k p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5857	. . . . . . 7 |- ( p = 1 -> ( ZZ>= ` p ) = ( ZZ>= ` 1 ) )
2	1	eleq2d 2530	. . . . . 6 |- ( p = 1 -> ( ( F ` n ) e. ( ZZ>= ` p ) <-> ( F ` n ) e. ( ZZ>= ` 1 ) ) )
3	2	rexbidv 2966	. . . . 5 |- ( p = 1 -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) <-> E. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) ) )
4	3	imbi2d 316	. . . 4 |- ( p = 1 -> ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) ) <-> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) ) ) )
5		fveq2 5857	. . . . . . 7 |- ( p = q -> ( ZZ>= ` p ) = ( ZZ>= ` q ) )
6	5	eleq2d 2530	. . . . . 6 |- ( p = q -> ( ( F ` n ) e. ( ZZ>= ` p ) <-> ( F ` n ) e. ( ZZ>= ` q ) ) )
7	6	rexbidv 2966	. . . . 5 |- ( p = q -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) <-> E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) ) )
8	7	imbi2d 316	. . . 4 |- ( p = q -> ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) ) <-> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) ) ) )
9		fveq2 5857	. . . . . . 7 |- ( p = ( q + 1 ) -> ( ZZ>= ` p ) = ( ZZ>= ` ( q + 1 ) ) )
10	9	eleq2d 2530	. . . . . 6 |- ( p = ( q + 1 ) -> ( ( F ` n ) e. ( ZZ>= ` p ) <-> ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) )
11	10	rexbidv 2966	. . . . 5 |- ( p = ( q + 1 ) -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) <-> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) )
12	11	imbi2d 316	. . . 4 |- ( p = ( q + 1 ) -> ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) ) <-> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) ) )
13		fveq2 5857	. . . . . . 7 |- ( p = A -> ( ZZ>= ` p ) = ( ZZ>= ` A ) )
14	13	eleq2d 2530	. . . . . 6 |- ( p = A -> ( ( F ` n ) e. ( ZZ>= ` p ) <-> ( F ` n ) e. ( ZZ>= ` A ) ) )
15	14	rexbidv 2966	. . . . 5 |- ( p = A -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) <-> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) ) )
16	15	imbi2d 316	. . . 4 |- ( p = A -> ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` p ) ) <-> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) ) ) )
17		1nn 10536	. . . . . . 7 |- 1 e. NN
18		ne0i 3784	. . . . . . 7 |- ( 1 e. NN -> NN =/= (/) )
19	17, 18	ax-mp 5	. . . . . 6 |- NN =/= (/)
20		ffvelrn 6010	. . . . . . . 8 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` n ) e. NN )
21		elnnuz 11107	. . . . . . . 8 |- ( ( F ` n ) e. NN <-> ( F ` n ) e. ( ZZ>= ` 1 ) )
22	20, 21	sylib 196	. . . . . . 7 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` n ) e. ( ZZ>= ` 1 ) )
23	22	ralrimiva 2871	. . . . . 6 |- ( F : NN --> NN -> A. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) )
24		r19.2z 3910	. . . . . 6 |- ( ( NN =/= (/) /\ A. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) )
25	19, 23, 24	sylancr 663	. . . . 5 |- ( F : NN --> NN -> E. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) )
26	25	adantr 465	. . . 4 |- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` 1 ) )
27		peano2nn 10537	. . . . . . . . . 10 |- ( n e. NN -> ( n + 1 ) e. NN )
28	27	adantl 466	. . . . . . . . 9 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( n + 1 ) e. NN )
29		nnre 10532	. . . . . . . . . . . . 13 |- ( q e. NN -> q e. RR )
30	29	ad2antrr 725	. . . . . . . . . . . 12 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> q e. RR )
31	20	nnred 10540	. . . . . . . . . . . . . 14 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` n ) e. RR )
32	31	adantlr 714	. . . . . . . . . . . . 13 |- ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) /\ n e. NN ) -> ( F ` n ) e. RR )
33	32	adantll 713	. . . . . . . . . . . 12 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( F ` n ) e. RR )
34		1re 9584	. . . . . . . . . . . . 13 |- 1 e. RR
35	34	a1i 11	. . . . . . . . . . . 12 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> 1 e. RR )
36	30, 33, 35	leadd1d 10135	. . . . . . . . . . 11 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( q <_ ( F ` n ) <-> ( q + 1 ) <_ ( ( F ` n ) + 1 ) ) )
37		fveq2 5857	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( F ` m ) = ( F ` n ) )
38		oveq1 6282	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( m + 1 ) = ( n + 1 ) )
39	38	fveq2d 5861	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( F ` ( m + 1 ) ) = ( F ` ( n + 1 ) ) )
40	37, 39	breq12d 4453	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( ( F ` m ) < ( F ` ( m + 1 ) ) <-> ( F ` n ) < ( F ` ( n + 1 ) ) ) )
41	40	rspcv 3203	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> ( A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) -> ( F ` n ) < ( F ` ( n + 1 ) ) ) )
42	41	imdistani 690	. . . . . . . . . . . . . . 15 |- ( ( n e. NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> ( n e. NN /\ ( F ` n ) < ( F ` ( n + 1 ) ) ) )
43		ffvelrn 6010	. . . . . . . . . . . . . . . . . . 19 |- ( ( F : NN --> NN /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) e. NN )
44	27, 43	sylan2 474	. . . . . . . . . . . . . . . . . 18 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` ( n + 1 ) ) e. NN )
45		nnltp1le 10907	. . . . . . . . . . . . . . . . . 18 |- ( ( ( F ` n ) e. NN /\ ( F ` ( n + 1 ) ) e. NN ) -> ( ( F ` n ) < ( F ` ( n + 1 ) ) <-> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) ) )
46	20, 44, 45	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( F : NN --> NN /\ n e. NN ) -> ( ( F ` n ) < ( F ` ( n + 1 ) ) <-> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) ) )
47	46	biimpa 484	. . . . . . . . . . . . . . . 16 |- ( ( ( F : NN --> NN /\ n e. NN ) /\ ( F ` n ) < ( F ` ( n + 1 ) ) ) -> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) )
48	47	anasss 647	. . . . . . . . . . . . . . 15 |- ( ( F : NN --> NN /\ ( n e. NN /\ ( F ` n ) < ( F ` ( n + 1 ) ) ) ) -> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) )
49	42, 48	sylan2 474	. . . . . . . . . . . . . 14 |- ( ( F : NN --> NN /\ ( n e. NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) -> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) )
50	49	anass1rs 805	. . . . . . . . . . . . 13 |- ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) /\ n e. NN ) -> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) )
51	50	adantll 713	. . . . . . . . . . . 12 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) )
52		peano2re 9741	. . . . . . . . . . . . . . . 16 |- ( q e. RR -> ( q + 1 ) e. RR )
53	29, 52	syl 16	. . . . . . . . . . . . . . 15 |- ( q e. NN -> ( q + 1 ) e. RR )
54	53	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( q e. NN /\ F : NN --> NN ) /\ n e. NN ) -> ( q + 1 ) e. RR )
55		peano2nn 10537	. . . . . . . . . . . . . . . . 17 |- ( ( F ` n ) e. NN -> ( ( F ` n ) + 1 ) e. NN )
56	20, 55	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( F : NN --> NN /\ n e. NN ) -> ( ( F ` n ) + 1 ) e. NN )
57	56	nnred 10540	. . . . . . . . . . . . . . 15 |- ( ( F : NN --> NN /\ n e. NN ) -> ( ( F ` n ) + 1 ) e. RR )
58	57	adantll 713	. . . . . . . . . . . . . 14 |- ( ( ( q e. NN /\ F : NN --> NN ) /\ n e. NN ) -> ( ( F ` n ) + 1 ) e. RR )
59	43	nnred 10540	. . . . . . . . . . . . . . . 16 |- ( ( F : NN --> NN /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) e. RR )
60	27, 59	sylan2 474	. . . . . . . . . . . . . . 15 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` ( n + 1 ) ) e. RR )
61	60	adantll 713	. . . . . . . . . . . . . 14 |- ( ( ( q e. NN /\ F : NN --> NN ) /\ n e. NN ) -> ( F ` ( n + 1 ) ) e. RR )
62		letr 9667	. . . . . . . . . . . . . 14 |- ( ( ( q + 1 ) e. RR /\ ( ( F ` n ) + 1 ) e. RR /\ ( F ` ( n + 1 ) ) e. RR ) -> ( ( ( q + 1 ) <_ ( ( F ` n ) + 1 ) /\ ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) ) -> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
63	54, 58, 61, 62	syl3anc 1223	. . . . . . . . . . . . 13 |- ( ( ( q e. NN /\ F : NN --> NN ) /\ n e. NN ) -> ( ( ( q + 1 ) <_ ( ( F ` n ) + 1 ) /\ ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) ) -> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
64	63	adantlrr 720	. . . . . . . . . . . 12 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( ( q + 1 ) <_ ( ( F ` n ) + 1 ) /\ ( ( F ` n ) + 1 ) <_ ( F ` ( n + 1 ) ) ) -> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
65	51, 64	mpan2d 674	. . . . . . . . . . 11 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( q + 1 ) <_ ( ( F ` n ) + 1 ) -> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
66	36, 65	sylbid 215	. . . . . . . . . 10 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( q <_ ( F ` n ) -> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
67		nnz 10875	. . . . . . . . . . . . 13 |- ( q e. NN -> q e. ZZ )
68	20	nnzd 10954	. . . . . . . . . . . . 13 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` n ) e. ZZ )
69		eluz 11084	. . . . . . . . . . . . 13 |- ( ( q e. ZZ /\ ( F ` n ) e. ZZ ) -> ( ( F ` n ) e. ( ZZ>= ` q ) <-> q <_ ( F ` n ) ) )
70	67, 68, 69	syl2an 477	. . . . . . . . . . . 12 |- ( ( q e. NN /\ ( F : NN --> NN /\ n e. NN ) ) -> ( ( F ` n ) e. ( ZZ>= ` q ) <-> q <_ ( F ` n ) ) )
71	70	adantrlr 722	. . . . . . . . . . 11 |- ( ( q e. NN /\ ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) /\ n e. NN ) ) -> ( ( F ` n ) e. ( ZZ>= ` q ) <-> q <_ ( F ` n ) ) )
72	71	anassrs 648	. . . . . . . . . 10 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( F ` n ) e. ( ZZ>= ` q ) <-> q <_ ( F ` n ) ) )
73	67	peano2zd 10958	. . . . . . . . . . . . 13 |- ( q e. NN -> ( q + 1 ) e. ZZ )
74	43	nnzd 10954	. . . . . . . . . . . . . 14 |- ( ( F : NN --> NN /\ ( n + 1 ) e. NN ) -> ( F ` ( n + 1 ) ) e. ZZ )
75	27, 74	sylan2 474	. . . . . . . . . . . . 13 |- ( ( F : NN --> NN /\ n e. NN ) -> ( F ` ( n + 1 ) ) e. ZZ )
76		eluz 11084	. . . . . . . . . . . . 13 |- ( ( ( q + 1 ) e. ZZ /\ ( F ` ( n + 1 ) ) e. ZZ ) -> ( ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
77	73, 75, 76	syl2an 477	. . . . . . . . . . . 12 |- ( ( q e. NN /\ ( F : NN --> NN /\ n e. NN ) ) -> ( ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
78	77	adantrlr 722	. . . . . . . . . . 11 |- ( ( q e. NN /\ ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) /\ n e. NN ) ) -> ( ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
79	78	anassrs 648	. . . . . . . . . 10 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( q + 1 ) <_ ( F ` ( n + 1 ) ) ) )
80	66, 72, 79	3imtr4d 268	. . . . . . . . 9 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( F ` n ) e. ( ZZ>= ` q ) -> ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) ) )
81		fveq2 5857	. . . . . . . . . . 11 |- ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
82	81	eleq1d 2529	. . . . . . . . . 10 |- ( k = ( n + 1 ) -> ( ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) ) )
83	82	rspcev 3207	. . . . . . . . 9 |- ( ( ( n + 1 ) e. NN /\ ( F ` ( n + 1 ) ) e. ( ZZ>= ` ( q + 1 ) ) ) -> E. k e. NN ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) )
84	28, 80, 83	syl6an 545	. . . . . . . 8 |- ( ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) /\ n e. NN ) -> ( ( F ` n ) e. ( ZZ>= ` q ) -> E. k e. NN ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) ) )
85	84	rexlimdva 2948	. . . . . . 7 |- ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) -> E. k e. NN ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) ) )
86		fveq2 5857	. . . . . . . . 9 |- ( k = n -> ( F ` k ) = ( F ` n ) )
87	86	eleq1d 2529	. . . . . . . 8 |- ( k = n -> ( ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) <-> ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) )
88	87	cbvrexv 3082	. . . . . . 7 |- ( E. k e. NN ( F ` k ) e. ( ZZ>= ` ( q + 1 ) ) <-> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) )
89	85, 88	syl6ib 226	. . . . . 6 |- ( ( q e. NN /\ ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) ) -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) )
90	89	ex 434	. . . . 5 |- ( q e. NN -> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> ( E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) ) )
91	90	a2d 26	. . . 4 |- ( q e. NN -> ( ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` q ) ) -> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` ( q + 1 ) ) ) ) )
92	4, 8, 12, 16, 26, 91	nnind 10543	. . 3 |- ( A e. NN -> ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) ) )
93	92	com12 31	. 2 |- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) ) -> ( A e. NN -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) ) )
94	93	3impia 1188	1 |- ( ( F : NN --> NN /\ A. m e. NN ( F ` m ) < ( F ` ( m + 1 ) ) /\ A e. NN ) -> E. n e. NN ( F ` n ) e. ( ZZ>= ` A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   =/= wne 2655   A.wral 2807   E.wrex 2808   (/)c0 3778   class class class wbr 4440   -->wf 5575   ` cfv 5579  (class class class)co 6275   RRcr 9480   1c1 9482   + caddc 9484   < clt 9617   <_ cle 9618   NNcn 10525   ZZcz 10853   ZZ>=cuz 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-recs 7032  df-rdg 7066  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9796  df-neg 9797  df-nn 10526  df-n0 10785  df-z 10854  df-uz 11072

This theorem is referenced by:  incsequz2  29832