Theorem monoord 6294

Description: Ordering relation for a monotonic sequence.

Hypotheses

Ref	Expression
monoord.1	|- F:NN-->RR
monoord.2	|- (x e. NN -> (F` x) <_ (F` (x + 1)))

Assertion

Ref	Expression
monoord	|- ((A e. NN /\ B e. NN /\ A <_ B) -> (F` A) <_ (F` B))

Distinct variable group:   x,F

Proof of Theorem monoord

Step	Hyp	Ref	Expression
1		breq2 2623	. . . . . 6 |- (y = 1 -> (A <_ y <-> A <_ 1))
2		fveq2 3724	. . . . . . 7 |- (y = 1 -> (F` y) = (F` 1))
3	2	breq2d 2630	. . . . . 6 |- (y = 1 -> ((F` A) <_ (F` y) <-> (F` A) <_ (F` 1)))
4	1, 3	imbi12d 626	. . . . 5 |- (y = 1 -> ((A <_ y -> (F` A) <_ (F` y)) <-> (A <_ 1 -> (F` A) <_ (F` 1))))
5	4	imbi2d 612	. . . 4 |- (y = 1 -> ((A e. NN -> (A <_ y -> (F` A) <_ (F` y))) <-> (A e. NN -> (A <_ 1 -> (F` A) <_ (F` 1)))))
6		breq2 2623	. . . . . 6 |- (y = z -> (A <_ y <-> A <_ z))
7		fveq2 3724	. . . . . . 7 |- (y = z -> (F` y) = (F` z))
8	7	breq2d 2630	. . . . . 6 |- (y = z -> ((F` A) <_ (F` y) <-> (F` A) <_ (F` z)))
9	6, 8	imbi12d 626	. . . . 5 |- (y = z -> ((A <_ y -> (F` A) <_ (F` y)) <-> (A <_ z -> (F` A) <_ (F` z))))
10	9	imbi2d 612	. . . 4 |- (y = z -> ((A e. NN -> (A <_ y -> (F` A) <_ (F` y))) <-> (A e. NN -> (A <_ z -> (F` A) <_ (F` z)))))
11		breq2 2623	. . . . . 6 |- (y = (z + 1) -> (A <_ y <-> A <_ (z + 1)))
12		fveq2 3724	. . . . . . 7 |- (y = (z + 1) -> (F` y) = (F` (z + 1)))
13	12	breq2d 2630	. . . . . 6 |- (y = (z + 1) -> ((F` A) <_ (F` y) <-> (F` A) <_ (F` (z + 1))))
14	11, 13	imbi12d 626	. . . . 5 |- (y = (z + 1) -> ((A <_ y -> (F` A) <_ (F` y)) <-> (A <_ (z + 1) -> (F` A) <_ (F` (z + 1)))))
15	14	imbi2d 612	. . . 4 |- (y = (z + 1) -> ((A e. NN -> (A <_ y -> (F` A) <_ (F` y))) <-> (A e. NN -> (A <_ (z + 1) -> (F` A) <_ (F` (z + 1))))))
16		breq2 2623	. . . . . 6 |- (y = B -> (A <_ y <-> A <_ B))
17		fveq2 3724	. . . . . . 7 |- (y = B -> (F` y) = (F` B))
18	17	breq2d 2630	. . . . . 6 |- (y = B -> ((F` A) <_ (F` y) <-> (F` A) <_ (F` B)))
19	16, 18	imbi12d 626	. . . . 5 |- (y = B -> ((A <_ y -> (F` A) <_ (F` y)) <-> (A <_ B -> (F` A) <_ (F` B))))
20	19	imbi2d 612	. . . 4 |- (y = B -> ((A e. NN -> (A <_ y -> (F` A) <_ (F` y))) <-> (A e. NN -> (A <_ B -> (F` A) <_ (F` B)))))
21		nnge1t 5943	. . . . 5 |- (A e. NN -> 1 <_ A)
22		nnret 5929	. . . . . . 7 |- (A e. NN -> A e. RR)
23		1re 5435	. . . . . . . 8 |- 1 e. RR
24		letri3t 5517	. . . . . . . 8 |- ((A e. RR /\ 1 e. RR) -> (A = 1 <-> (A <_ 1 /\ 1 <_ A)))
25	23, 24	mpan2 696	. . . . . . 7 |- (A e. RR -> (A = 1 <-> (A <_ 1 /\ 1 <_ A)))
26	22, 25	syl 10	. . . . . 6 |- (A e. NN -> (A = 1 <-> (A <_ 1 /\ 1 <_ A)))
27		eqlet 5571	. . . . . . . 8 |- (((F` A) e. RR /\ (F` A) = (F` 1)) -> (F` A) <_ (F` 1))
28		monoord.1	. . . . . . . . 9 |- F:NN-->RR
29	28	ffvelrni 3815	. . . . . . . 8 |- (A e. NN -> (F` A) e. RR)
30		fveq2 3724	. . . . . . . 8 |- (A = 1 -> (F` A) = (F` 1))
31	27, 29, 30	syl2an 454	. . . . . . 7 |- ((A e. NN /\ A = 1) -> (F` A) <_ (F` 1))
32	31	ex 373	. . . . . 6 |- (A e. NN -> (A = 1 -> (F` A) <_ (F` 1)))
33	26, 32	sylbird 205	. . . . 5 |- (A e. NN -> ((A <_ 1 /\ 1 <_ A) -> (F` A) <_ (F` 1)))
34	21, 33	mpan2d 702	. . . 4 |- (A e. NN -> (A <_ 1 -> (F` A) <_ (F` 1)))
35		leloet 5518	. . . . . . . . . 10 |- ((A e. RR /\ (z + 1) e. RR) -> (A <_ (z + 1) <-> (A < (z + 1) \/ A = (z + 1))))
36		peano2nn 5935	. . . . . . . . . . 11 |- (z e. NN -> (z + 1) e. NN)
37		nnret 5929	. . . . . . . . . . 11 |- ((z + 1) e. NN -> (z + 1) e. RR)
38	36, 37	syl 10	. . . . . . . . . 10 |- (z e. NN -> (z + 1) e. RR)
39	35, 22, 38	syl2an 454	. . . . . . . . 9 |- ((A e. NN /\ z e. NN) -> (A <_ (z + 1) <-> (A < (z + 1) \/ A = (z + 1))))
40	39	adantr 389	. . . . . . . 8 |- (((A e. NN /\ z e. NN) /\ (A <_ z -> (F` A) <_ (F` z))) -> (A <_ (z + 1) <-> (A < (z + 1) \/ A = (z + 1))))
41		nnleltp1t 5954	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> (A <_ z <-> A < (z + 1)))
42	41	adantr 389	. . . . . . . . . 10 |- (((A e. NN /\ z e. NN) /\ (A <_ z -> (F` A) <_ (F` z))) -> (A <_ z <-> A < (z + 1)))
43	29	ad2antrr 404	. . . . . . . . . . . . . 14 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` A) e. RR)
44	28	ffvelrni 3815	. . . . . . . . . . . . . . 15 |- (z e. NN -> (F` z) e. RR)
45	44	ad2antlr 405	. . . . . . . . . . . . . 14 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` z) e. RR)
46	28	ffvelrni 3815	. . . . . . . . . . . . . . . 16 |- ((z + 1) e. NN -> (F` (z + 1)) e. RR)
47	36, 46	syl 10	. . . . . . . . . . . . . . 15 |- (z e. NN -> (F` (z + 1)) e. RR)
48	47	ad2antlr 405	. . . . . . . . . . . . . 14 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` (z + 1)) e. RR)
49		pm3.27 323	. . . . . . . . . . . . . 14 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` A) <_ (F` z))
50		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (x = z -> (F` x) = (F` z))
51		opreq1 3968	. . . . . . . . . . . . . . . . . 18 |- (x = z -> (x + 1) = (z + 1))
52	51	fveq2d 3728	. . . . . . . . . . . . . . . . 17 |- (x = z -> (F` (x + 1)) = (F` (z + 1)))
53	50, 52	breq12d 2631	. . . . . . . . . . . . . . . 16 |- (x = z -> ((F` x) <_ (F` (x + 1)) <-> (F` z) <_ (F` (z + 1))))
54		monoord.2	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (F` x) <_ (F` (x + 1)))
55	53, 54	vtoclga 1852	. . . . . . . . . . . . . . 15 |- (z e. NN -> (F` z) <_ (F` (z + 1)))
56	55	ad2antlr 405	. . . . . . . . . . . . . 14 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` z) <_ (F` (z + 1)))
57	43, 45, 48, 49, 56	letrd 5526	. . . . . . . . . . . . 13 |- (((A e. NN /\ z e. NN) /\ (F` A) <_ (F` z)) -> (F` A) <_ (F` (z + 1)))
58	57	ex 373	. . . . . . . . . . . 12 |- ((A e. NN /\ z e. NN) -> ((F` A) <_ (F` z) -> (F` A) <_ (F` (z + 1))))
59	58	imim2d 25	. . . . . . . . . . 11 |- ((A e. NN /\ z e. NN) -> ((A <_ z -> (F` A) <_ (F` z)) -> (A <_ z -> (F` A) <_ (F` (z + 1)))))
60	59	imp 350	. . . . . . . . . 10 |- (((A e. NN /\ z e. NN) /\ (A <_ z -> (F` A) <_ (F` z))) -> (A <_ z -> (F` A) <_ (F` (z + 1))))
61	42, 60	sylbird 205	. . . . . . . . 9 |- (((A e. NN /\ z e. NN) /\ (A <_ z -> (F` A) <_ (F` z))) -> (A < (z + 1) -> (F` A) <_ (F` (z + 1))))
62		eqlet 5571	. . . . . . . . . . . 12 |- (((F` A) e. RR /\ (F` A) = (F` (z + 1))) -> (F` A) <_ (F` (z + 1)))
63		fveq2 3724	. . . . . . . . . . . 12 |- (A = (z + 1) -> (F