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	⊢ 𝑄 = ( ℂfld ↾s ℚ )
	qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
Assertion	qabvle	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		qrng.q	⊢ 𝑄 = ( ℂfld ↾s ℚ )
2		qabsabv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑄 )
3		fveq2	⊢ ( 𝑘 = 0 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 0 ) )
4		id	⊢ ( 𝑘 = 0 → 𝑘 = 0 )
5	3 4	breq12d	⊢ ( 𝑘 = 0 → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ↔ ( 𝐹 ‘ 0 ) ≤ 0 ) )
6	5	imbi2d	⊢ ( 𝑘 = 0 → ( ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ) ↔ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) ≤ 0 ) ) )
7		fveq2	⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
8		id	⊢ ( 𝑘 = 𝑛 → 𝑘 = 𝑛 )
9	7 8	breq12d	⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ↔ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) )
10	9	imbi2d	⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ) ↔ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) )
11		fveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑛 + 1 ) ) )
12		id	⊢ ( 𝑘 = ( 𝑛 + 1 ) → 𝑘 = ( 𝑛 + 1 ) )
13	11 12	breq12d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ↔ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) ) )
14	13	imbi2d	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ) ↔ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) ) ) )
15		fveq2	⊢ ( 𝑘 = 𝑁 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑁 ) )
16		id	⊢ ( 𝑘 = 𝑁 → 𝑘 = 𝑁 )
17	15 16	breq12d	⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ↔ ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 ) )
18	17	imbi2d	⊢ ( 𝑘 = 𝑁 → ( ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑘 ) ≤ 𝑘 ) ↔ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 ) ) )
19	1	qrng0	⊢ 0 = ( 0g ‘ 𝑄 )
20	2 19	abv0	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )
21		0le0	⊢ 0 ≤ 0
22	20 21	eqbrtrdi	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) ≤ 0 )
23		nn0p1nn	⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ )
24	23	ad2antrl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ℕ )
25		nnq	⊢ ( ( 𝑛 + 1 ) ∈ ℕ → ( 𝑛 + 1 ) ∈ ℚ )
26	24 25	syl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ℚ )
27	1	qrngbas	⊢ ℚ = ( Base ‘ 𝑄 )
28	2 27	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 + 1 ) ∈ ℚ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
29	26 28	syldan	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
30		nn0z	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
31	30	ad2antrl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 𝑛 ∈ ℤ )
32		zq	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℚ )
33	31 32	syl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 𝑛 ∈ ℚ )
34	2 27	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
35	33 34	syldan	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ∈ ℝ )
36		peano2re	⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ℝ → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℝ )
37	35 36	syl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ∈ ℝ )
38	31	zred	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 𝑛 ∈ ℝ )
39		peano2re	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 + 1 ) ∈ ℝ )
40	38 39	syl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝑛 + 1 ) ∈ ℝ )
41		simpl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 𝐹 ∈ 𝐴 )
42		1z	⊢ 1 ∈ ℤ
43		zq	⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
44	42 43	mp1i	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 1 ∈ ℚ )
45		qex	⊢ ℚ ∈ V
46		cnfldadd	⊢ + = ( +g ‘ ℂfld )
47	1 46	ressplusg	⊢ ( ℚ ∈ V → + = ( +g ‘ 𝑄 ) )
48	45 47	ax-mp	⊢ + = ( +g ‘ 𝑄 )
49	2 27 48	abvtri	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℚ ∧ 1 ∈ ℚ ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) + ( 𝐹 ‘ 1 ) ) )
50	41 33 44 49	syl3anc	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) + ( 𝐹 ‘ 1 ) ) )
51		ax-1ne0	⊢ 1 ≠ 0
52	1	qrng1	⊢ 1 = ( 1r ‘ 𝑄 )
53	2 52 19	abv1z	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )
54	51 53	mpan2	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 1 ) = 1 )
55	54	adantr	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ 1 ) = 1 )
56	55	oveq2d	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) + ( 𝐹 ‘ 1 ) ) = ( ( 𝐹 ‘ 𝑛 ) + 1 ) )
57	50 56	breqtrd	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( ( 𝐹 ‘ 𝑛 ) + 1 ) )
58		1red	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → 1 ∈ ℝ )
59		simprr	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 )
60	35 38 58 59	leadd1dd	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( ( 𝐹 ‘ 𝑛 ) + 1 ) ≤ ( 𝑛 + 1 ) )
61	29 37 40 57 60	letrd	⊢ ( ( 𝐹 ∈ 𝐴 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) ) → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) )
62	61	expr	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) ) )
63	62	expcom	⊢ ( 𝑛 ∈ ℕ0 → ( 𝐹 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) ) ) )
64	63	a2d	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑛 ) ≤ 𝑛 ) → ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) ≤ ( 𝑛 + 1 ) ) ) )
65	6 10 14 18 22 64	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 ) )
66	65	impcom	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑁 ) ≤ 𝑁 )