Theorem qabvle

Description: By using induction on N , we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014)

	Ref	Expression
Hypotheses	qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
Assertion	qabvle	$$⊢\left(F\in A\wedge N\in {\mathbb{N}}_0\right)\to F\left(N\right)\le N$$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
2		qabsabv.a	$$⊢A=\mathrm{AbsVal}\left(Q\right)$$
3		fveq2	$$⊢k=0\to F\left(k\right)=F\left(0\right)$$
4		id	$$⊢k=0\to k=0$$
5	3 4	breq12d	$$⊢k=0\to \left(F\left(k\right)\le k\leftrightarrow F\left(0\right)\le 0\right)$$
6	5	imbi2d	$$⊢k=0\to \left(\left(F\in A\to F\left(k\right)\le k\right)\leftrightarrow \left(F\in A\to F\left(0\right)\le 0\right)\right)$$
7		fveq2	$$⊢k=n\to F\left(k\right)=F\left(n\right)$$
8		id	$$⊢k=n\to k=n$$
9	7 8	breq12d	$$⊢k=n\to \left(F\left(k\right)\le k\leftrightarrow F\left(n\right)\le n\right)$$
10	9	imbi2d	$$⊢k=n\to \left(\left(F\in A\to F\left(k\right)\le k\right)\leftrightarrow \left(F\in A\to F\left(n\right)\le n\right)\right)$$
11		fveq2	$$⊢k=n+1\to F\left(k\right)=F\left(n+1\right)$$
12		id	$$⊢k=n+1\to k=n+1$$
13	11 12	breq12d	$$⊢k=n+1\to \left(F\left(k\right)\le k\leftrightarrow F\left(n+1\right)\le n+1\right)$$
14	13	imbi2d	$$⊢k=n+1\to \left(\left(F\in A\to F\left(k\right)\le k\right)\leftrightarrow \left(F\in A\to F\left(n+1\right)\le n+1\right)\right)$$
15		fveq2	$$⊢k=N\to F\left(k\right)=F\left(N\right)$$
16		id	$$⊢k=N\to k=N$$
17	15 16	breq12d	$$⊢k=N\to \left(F\left(k\right)\le k\leftrightarrow F\left(N\right)\le N\right)$$
18	17	imbi2d	$$⊢k=N\to \left(\left(F\in A\to F\left(k\right)\le k\right)\leftrightarrow \left(F\in A\to F\left(N\right)\le N\right)\right)$$
19	1	qrng0	$$⊢0=0_Q$$
20	2 19	abv0	$$⊢F\in A\to F\left(0\right)=0$$
21		0le0	$$⊢0\le 0$$
22	20 21	eqbrtrdi	$$⊢F\in A\to F\left(0\right)\le 0$$
23		nn0p1nn	$$⊢n\in {\mathbb{N}}_0\to n+1\in \mathbb{N}$$
24	23	ad2antrl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n+1\in \mathbb{N}$$
25		nnq	$$⊢n+1\in \mathbb{N}\to n+1\in \mathbb{Q}$$
26	24 25	syl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n+1\in \mathbb{Q}$$
27	1	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
28	2 27	abvcl	$$⊢\left(F\in A\wedge n+1\in \mathbb{Q}\right)\to F\left(n+1\right)\in ℝ$$
29	26 28	syldan	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n+1\right)\in ℝ$$
30		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
31	30	ad2antrl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n\in \mathbb{Z}$$
32		zq	$$⊢n\in \mathbb{Z}\to n\in \mathbb{Q}$$
33	31 32	syl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n\in \mathbb{Q}$$
34	2 27	abvcl	$$⊢\left(F\in A\wedge n\in \mathbb{Q}\right)\to F\left(n\right)\in ℝ$$
35	33 34	syldan	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n\right)\in ℝ$$
36		peano2re	$$⊢F\left(n\right)\in ℝ\to F\left(n\right)+1\in ℝ$$
37	35 36	syl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n\right)+1\in ℝ$$
38	31	zred	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n\in ℝ$$
39		peano2re	$$⊢n\in ℝ\to n+1\in ℝ$$
40	38 39	syl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to n+1\in ℝ$$
41		simpl	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\in A$$
42		1z	$$⊢1\in \mathbb{Z}$$
43		zq	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Q}$$
44	42 43	mp1i	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to 1\in \mathbb{Q}$$
45		qex	$$⊢\mathbb{Q}\in \mathrm{V}$$
46		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
47	1 46	ressplusg	$$⊢\mathbb{Q}\in \mathrm{V}\to +={+}_Q$$
48	45 47	ax-mp	$$⊢+={+}_Q$$
49	2 27 48	abvtri	$$⊢\left(F\in A\wedge n\in \mathbb{Q}\wedge 1\in \mathbb{Q}\right)\to F\left(n+1\right)\le F\left(n\right)+F\left(1\right)$$
50	41 33 44 49	syl3anc	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n+1\right)\le F\left(n\right)+F\left(1\right)$$
51		ax-1ne0	$$⊢1\ne 0$$
52	1	qrng1	$$⊢1=1_Q$$
53	2 52 19	abv1z	$$⊢\left(F\in A\wedge 1\ne 0\right)\to F\left(1\right)=1$$
54	51 53	mpan2	$$⊢F\in A\to F\left(1\right)=1$$
55	54	adantr	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(1\right)=1$$
56	55	oveq2d	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n\right)+F\left(1\right)=F\left(n\right)+1$$
57	50 56	breqtrd	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n+1\right)\le F\left(n\right)+1$$
58		1red	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to 1\in ℝ$$
59		simprr	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n\right)\le n$$
60	35 38 58 59	leadd1dd	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n\right)+1\le n+1$$
61	29 37 40 57 60	letrd	$$⊢\left(F\in A\wedge \left(n\in {\mathbb{N}}_0\wedge F\left(n\right)\le n\right)\right)\to F\left(n+1\right)\le n+1$$
62	61	expr	$$⊢\left(F\in A\wedge n\in {\mathbb{N}}_0\right)\to \left(F\left(n\right)\le n\to F\left(n+1\right)\le n+1\right)$$
63	62	expcom	$$⊢n\in {\mathbb{N}}_0\to \left(F\in A\to \left(F\left(n\right)\le n\to F\left(n+1\right)\le n+1\right)\right)$$
64	63	a2d	$$⊢n\in {\mathbb{N}}_0\to \left(\left(F\in A\to F\left(n\right)\le n\right)\to \left(F\in A\to F\left(n+1\right)\le n+1\right)\right)$$
65	6 10 14 18 22 64	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(F\in A\to F\left(N\right)\le N\right)$$
66	65	impcom	$$⊢\left(F\in A\wedge N\in {\mathbb{N}}_0\right)\to F\left(N\right)\le N$$