faclbnd4lem4

Description: Lemma for faclbnd4 . Prove the 0 < N case by induction on K . (Contributed by NM, 19-Dec-2005)

		Ref	Expression
	Assertion	faclbnd4lem4	$⊢ (N \in ℕ \land K \in ℕ_{0} \land M \in ℕ_{0}) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ n = m \to n^{j} = m^{j}$
2		oveq2	$⊢ n = m \to M^{n} = M^{m}$
3	1 2	oveq12d	$⊢ n = m \to n^{j} M^{n} = m^{j} M^{m}$
4		fveq2	$⊢ n = m \to n! = m!$
5	4	oveq2d	$⊢ n = m \to 2^{j^{2}} M^{M + j} n! = 2^{j^{2}} M^{M + j} m!$
6	3 5	breq12d	$⊢ n = m \to (n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n! \leftrightarrow m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m!)$
7	6	cbvralvw	$⊢ \forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n! \leftrightarrow \forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m!$
8		nnre	$⊢ n \in ℕ \to n \in ℝ$
9		1re	$⊢ 1 \in ℝ$
10		lelttric	$⊢ (n \in ℝ \land 1 \in ℝ) \to (n \leq 1 \lor 1 < n)$
11	8 9 10	sylancl	$⊢ n \in ℕ \to (n \leq 1 \lor 1 < n)$
12	11	ancli	$⊢ n \in ℕ \to (n \in ℕ \land (n \leq 1 \lor 1 < n))$
13		andi	$⊢ (n \in ℕ \land (n \leq 1 \lor 1 < n)) \leftrightarrow ((n \in ℕ \land n \leq 1) \lor (n \in ℕ \land 1 < n))$
14	12 13	sylib	$⊢ n \in ℕ \to ((n \in ℕ \land n \leq 1) \lor (n \in ℕ \land 1 < n))$
15		nnge1	$⊢ n \in ℕ \to 1 \leq n$
16		letri3	$⊢ (n \in ℝ \land 1 \in ℝ) \to (n = 1 \leftrightarrow (n \leq 1 \land 1 \leq n))$
17	8 9 16	sylancl	$⊢ n \in ℕ \to (n = 1 \leftrightarrow (n \leq 1 \land 1 \leq n))$
18	17	biimpar	$⊢ (n \in ℕ \land (n \leq 1 \land 1 \leq n)) \to n = 1$
19	18	anassrs	$⊢ ((n \in ℕ \land n \leq 1) \land 1 \leq n) \to n = 1$
20	15 19	mpidan	$⊢ (n \in ℕ \land n \leq 1) \to n = 1$
21		oveq1	$⊢ n = 1 \to n - 1 = 1 - 1$
22		1m1e0	$⊢ 1 - 1 = 0$
23	21 22	eqtrdi	$⊢ n = 1 \to n - 1 = 0$
24	20 23	syl	$⊢ (n \in ℕ \land n \leq 1) \to n - 1 = 0$
25		faclbnd4lem3	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land n - 1 = 0) \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!$
26	24 25	sylan2	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land (n \in ℕ \land n \leq 1)) \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!$
27	26	a1d	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land (n \in ℕ \land n \leq 1)) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
28		1nn	$⊢ 1 \in ℕ$
29		nnsub	$⊢ (1 \in ℕ \land n \in ℕ) \to (1 < n \leftrightarrow n - 1 \in ℕ)$
30	28 29	mpan	$⊢ n \in ℕ \to (1 < n \leftrightarrow n - 1 \in ℕ)$
31	30	biimpa	$⊢ (n \in ℕ \land 1 < n) \to n - 1 \in ℕ$
32		oveq1	$⊢ m = n - 1 \to m^{j} = {(n - 1)}^{j}$
33		oveq2	$⊢ m = n - 1 \to M^{m} = M^{n - 1}$
34	32 33	oveq12d	$⊢ m = n - 1 \to m^{j} M^{m} = {(n - 1)}^{j} M^{n - 1}$
35		fveq2	$⊢ m = n - 1 \to m! = (n - 1)!$
36	35	oveq2d	$⊢ m = n - 1 \to 2^{j^{2}} M^{M + j} m! = 2^{j^{2}} M^{M + j} (n - 1)!$
37	34 36	breq12d	$⊢ m = n - 1 \to (m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \leftrightarrow {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
38	37	rspcv	$⊢ n - 1 \in ℕ \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
39	31 38	syl	$⊢ (n \in ℕ \land 1 < n) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
40	39	adantl	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land (n \in ℕ \land 1 < n)) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
41	27 40	jaodan	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land ((n \in ℕ \land n \leq 1) \lor (n \in ℕ \land 1 < n))) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
42	14 41	sylan2	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land n \in ℕ) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to {(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)!)$
43		faclbnd4lem2	$⊢ (M \in ℕ_{0} \land j \in ℕ_{0} \land n \in ℕ) \to ({(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)! \to n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
44	43	3expa	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land n \in ℕ) \to ({(n - 1)}^{j} M^{n - 1} \leq 2^{j^{2}} M^{M + j} (n - 1)! \to n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
45	42 44	syld	$⊢ ((M \in ℕ_{0} \land j \in ℕ_{0}) \land n \in ℕ) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
46	45	ralrimdva	$⊢ (M \in ℕ_{0} \land j \in ℕ_{0}) \to (\forall m \in ℕ m^{j} M^{m} \leq 2^{j^{2}} M^{M + j} m! \to \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
47	7 46	biimtrid	$⊢ (M \in ℕ_{0} \land j \in ℕ_{0}) \to (\forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n! \to \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
48	47	expcom	$⊢ j \in ℕ_{0} \to (M \in ℕ_{0} \to (\forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n! \to \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!))$
49	48	a2d	$⊢ j \in ℕ_{0} \to ((M \in ℕ_{0} \to \forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n!) \to (M \in ℕ_{0} \to \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!))$
50		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
51		faclbnd3	$⊢ (M \in ℕ_{0} \land n \in ℕ_{0}) \to M^{n} \leq M^{M} n!$
52	50 51	sylan2	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to M^{n} \leq M^{M} n!$
53		nncn	$⊢ n \in ℕ \to n \in ℂ$
54	53	exp0d	$⊢ n \in ℕ \to n^{0} = 1$
55	54	oveq1d	$⊢ n \in ℕ \to n^{0} M^{n} = 1 M^{n}$
56	55	adantl	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to n^{0} M^{n} = 1 M^{n}$
57		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
58		expcl	$⊢ (M \in ℂ \land n \in ℕ_{0}) \to M^{n} \in ℂ$
59	57 50 58	syl2an	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to M^{n} \in ℂ$
60	59	mullidd	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to 1 M^{n} = M^{n}$
61	56 60	eqtrd	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to n^{0} M^{n} = M^{n}$
62		sq0	$⊢ 0^{2} = 0$
63	62	oveq2i	$⊢ 2^{0^{2}} = 2^{0}$
64		2cn	$⊢ 2 \in ℂ$
65		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
66	64 65	ax-mp	$⊢ 2^{0} = 1$
67	63 66	eqtri	$⊢ 2^{0^{2}} = 1$
68	67	a1i	$⊢ M \in ℕ_{0} \to 2^{0^{2}} = 1$
69	57	addridd	$⊢ M \in ℕ_{0} \to M + 0 = M$
70	69	oveq2d	$⊢ M \in ℕ_{0} \to M^{M + 0} = M^{M}$
71	68 70	oveq12d	$⊢ M \in ℕ_{0} \to 2^{0^{2}} M^{M + 0} = 1 M^{M}$
72		expcl	$⊢ (M \in ℂ \land M \in ℕ_{0}) \to M^{M} \in ℂ$
73	57 72	mpancom	$⊢ M \in ℕ_{0} \to M^{M} \in ℂ$
74	73	mullidd	$⊢ M \in ℕ_{0} \to 1 M^{M} = M^{M}$
75	71 74	eqtrd	$⊢ M \in ℕ_{0} \to 2^{0^{2}} M^{M + 0} = M^{M}$
76	75	oveq1d	$⊢ M \in ℕ_{0} \to 2^{0^{2}} M^{M + 0} n! = M^{M} n!$
77	76	adantr	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to 2^{0^{2}} M^{M + 0} n! = M^{M} n!$
78	52 61 77	3brtr4d	$⊢ (M \in ℕ_{0} \land n \in ℕ) \to n^{0} M^{n} \leq 2^{0^{2}} M^{M + 0} n!$
79	78	ralrimiva	$⊢ M \in ℕ_{0} \to \forall n \in ℕ n^{0} M^{n} \leq 2^{0^{2}} M^{M + 0} n!$
80		oveq2	$⊢ m = 0 \to n^{m} = n^{0}$
81	80	oveq1d	$⊢ m = 0 \to n^{m} M^{n} = n^{0} M^{n}$
82		oveq1	$⊢ m = 0 \to m^{2} = 0^{2}$
83	82	oveq2d	$⊢ m = 0 \to 2^{m^{2}} = 2^{0^{2}}$
84		oveq2	$⊢ m = 0 \to M + m = M + 0$
85	84	oveq2d	$⊢ m = 0 \to M^{M + m} = M^{M + 0}$
86	83 85	oveq12d	$⊢ m = 0 \to 2^{m^{2}} M^{M + m} = 2^{0^{2}} M^{M + 0}$
87	86	oveq1d	$⊢ m = 0 \to 2^{m^{2}} M^{M + m} n! = 2^{0^{2}} M^{M + 0} n!$
88	81 87	breq12d	$⊢ m = 0 \to (n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow n^{0} M^{n} \leq 2^{0^{2}} M^{M + 0} n!)$
89	88	ralbidv	$⊢ m = 0 \to (\forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow \forall n \in ℕ n^{0} M^{n} \leq 2^{0^{2}} M^{M + 0} n!)$
90	89	imbi2d	$⊢ m = 0 \to ((M \in ℕ_{0} \to \forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n!) \leftrightarrow (M \in ℕ_{0} \to \forall n \in ℕ n^{0} M^{n} \leq 2^{0^{2}} M^{M + 0} n!))$
91		oveq2	$⊢ m = j \to n^{m} = n^{j}$
92	91	oveq1d	$⊢ m = j \to n^{m} M^{n} = n^{j} M^{n}$
93		oveq1	$⊢ m = j \to m^{2} = j^{2}$
94	93	oveq2d	$⊢ m = j \to 2^{m^{2}} = 2^{j^{2}}$
95		oveq2	$⊢ m = j \to M + m = M + j$
96	95	oveq2d	$⊢ m = j \to M^{M + m} = M^{M + j}$
97	94 96	oveq12d	$⊢ m = j \to 2^{m^{2}} M^{M + m} = 2^{j^{2}} M^{M + j}$
98	97	oveq1d	$⊢ m = j \to 2^{m^{2}} M^{M + m} n! = 2^{j^{2}} M^{M + j} n!$
99	92 98	breq12d	$⊢ m = j \to (n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n!)$
100	99	ralbidv	$⊢ m = j \to (\forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow \forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n!)$
101	100	imbi2d	$⊢ m = j \to ((M \in ℕ_{0} \to \forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n!) \leftrightarrow (M \in ℕ_{0} \to \forall n \in ℕ n^{j} M^{n} \leq 2^{j^{2}} M^{M + j} n!))$
102		oveq2	$⊢ m = j + 1 \to n^{m} = n^{j + 1}$
103	102	oveq1d	$⊢ m = j + 1 \to n^{m} M^{n} = n^{j + 1} M^{n}$
104		oveq1	$⊢ m = j + 1 \to m^{2} = {(j + 1)}^{2}$
105	104	oveq2d	$⊢ m = j + 1 \to 2^{m^{2}} = 2^{{(j + 1)}^{2}}$
106		oveq2	$⊢ m = j + 1 \to M + m = M + j + 1$
107	106	oveq2d	$⊢ m = j + 1 \to M^{M + m} = M^{M + j + 1}$
108	105 107	oveq12d	$⊢ m = j + 1 \to 2^{m^{2}} M^{M + m} = 2^{{(j + 1)}^{2}} M^{M + j + 1}$
109	108	oveq1d	$⊢ m = j + 1 \to 2^{m^{2}} M^{M + m} n! = 2^{{(j + 1)}^{2}} M^{M + j + 1} n!$
110	103 109	breq12d	$⊢ m = j + 1 \to (n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
111	110	ralbidv	$⊢ m = j + 1 \to (\forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!)$
112	111	imbi2d	$⊢ m = j + 1 \to ((M \in ℕ_{0} \to \forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n!) \leftrightarrow (M \in ℕ_{0} \to \forall n \in ℕ n^{j + 1} M^{n} \leq 2^{{(j + 1)}^{2}} M^{M + j + 1} n!))$
113		oveq2	$⊢ m = K \to n^{m} = n^{K}$
114	113	oveq1d	$⊢ m = K \to n^{m} M^{n} = n^{K} M^{n}$
115		oveq1	$⊢ m = K \to m^{2} = K^{2}$
116	115	oveq2d	$⊢ m = K \to 2^{m^{2}} = 2^{K^{2}}$
117		oveq2	$⊢ m = K \to M + m = M + K$
118	117	oveq2d	$⊢ m = K \to M^{M + m} = M^{M + K}$
119	116 118	oveq12d	$⊢ m = K \to 2^{m^{2}} M^{M + m} = 2^{K^{2}} M^{M + K}$
120	119	oveq1d	$⊢ m = K \to 2^{m^{2}} M^{M + m} n! = 2^{K^{2}} M^{M + K} n!$
121	114 120	breq12d	$⊢ m = K \to (n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!)$
122	121	ralbidv	$⊢ m = K \to (\forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n! \leftrightarrow \forall n \in ℕ n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!)$
123	122	imbi2d	$⊢ m = K \to ((M \in ℕ_{0} \to \forall n \in ℕ n^{m} M^{n} \leq 2^{m^{2}} M^{M + m} n!) \leftrightarrow (M \in ℕ_{0} \to \forall n \in ℕ n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!))$
124	49 79 90 101 112 123	nn0indALT	$⊢ K \in ℕ_{0} \to (M \in ℕ_{0} \to \forall n \in ℕ n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!)$
125	124	imp	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \forall n \in ℕ n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!$
126		oveq1	$⊢ n = N \to n^{K} = N^{K}$
127		oveq2	$⊢ n = N \to M^{n} = M^{N}$
128	126 127	oveq12d	$⊢ n = N \to n^{K} M^{n} = N^{K} M^{N}$
129		fveq2	$⊢ n = N \to n! = N!$
130	129	oveq2d	$⊢ n = N \to 2^{K^{2}} M^{M + K} n! = 2^{K^{2}} M^{M + K} N!$
131	128 130	breq12d	$⊢ n = N \to (n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n! \leftrightarrow N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!)$
132	131	rspcva	$⊢ (N \in ℕ \land \forall n \in ℕ n^{K} M^{n} \leq 2^{K^{2}} M^{M + K} n!) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
133	125 132	sylan2	$⊢ (N \in ℕ \land (K \in ℕ_{0} \land M \in ℕ_{0})) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$
134	133	3impb	$⊢ (N \in ℕ \land K \in ℕ_{0} \land M \in ℕ_{0}) \to N^{K} M^{N} \leq 2^{K^{2}} M^{M + K} N!$

Metamath Proof Explorer

Theorem faclbnd4lem4

Proof