Theorem faclbnd4lem4 8203

Description: Lemma for faclbnd4 8204. Prove the 0 < N case by induction on K.

Assertion

Ref	Expression
faclbnd4lem4	|- ((N e. NN /\ K e. NN0 /\ M e. NN0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))

Proof of Theorem faclbnd4lem4

Step	Hyp	Ref	Expression
1		opreq1 4889	. . . . . 6 |- (n = N -> (n^K) = (N^K))
2		opreq2 4890	. . . . . 6 |- (n = N -> (M^n) = (M^N))
3	1, 2	opreq12d 4900	. . . . 5 |- (n = N -> ((n^K) x. (M^n)) = ((N^K) x. (M^N)))
4		fveq2 4681	. . . . . 6 |- (n = N -> (!` n) = (!` N))
5	4	opreq2d 4898	. . . . 5 |- (n = N -> (((2^(K^2)) x. (M^(M + K))) x. (!` n)) = (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
6	3, 5	breq12d 3351	. . . 4 |- (n = N -> (((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n)) <-> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N))))
7	6	rcla4va 2378	. . 3 |- ((N e. NN /\ A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n))) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
8		faclbnd4lem3 8202	. . . . . . . . . . . . . 14 |- (((M e. NN0 /\ j e. NN0) /\ (n - 1) = 0) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
9		nnge1 7126	. . . . . . . . . . . . . . . . 17 |- (n e. NN -> 1 <_ n)
10	9	adantr 425	. . . . . . . . . . . . . . . 16 |- ((n e. NN /\ n <_ 1) -> 1 <_ n)
11		letri3 6687	. . . . . . . . . . . . . . . . . . 19 |- ((n e. RR /\ 1 e. RR) -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
12		nnre 7112	. . . . . . . . . . . . . . . . . . 19 |- (n e. NN -> n e. RR)
13		1re 6598	. . . . . . . . . . . . . . . . . . 19 |- 1 e. RR
14	11, 12, 13	sylancl 525	. . . . . . . . . . . . . . . . . 18 |- (n e. NN -> (n = 1 <-> (n <_ 1 /\ 1 <_ n)))
15	14	biimpar 461	. . . . . . . . . . . . . . . . 17 |- ((n e. NN /\ (n <_ 1 /\ 1 <_ n)) -> n = 1)
16	15	anassrs 489	. . . . . . . . . . . . . . . 16 |- (((n e. NN /\ n <_ 1) /\ 1 <_ n) -> n = 1)
17	10, 16	mpdan 768	. . . . . . . . . . . . . . 15 |- ((n e. NN /\ n <_ 1) -> n = 1)
18		opreq1 4889	. . . . . . . . . . . . . . . 16 |- (n = 1 -> (n - 1) = (1 - 1))
19		ax1cn 6422	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
20	19	subidi 6551	. . . . . . . . . . . . . . . 16 |- (1 - 1) = 0
21	18, 20	syl6eq 1944	. . . . . . . . . . . . . . 15 |- (n = 1 -> (n - 1) = 0)
22	17, 21	syl 12	. . . . . . . . . . . . . 14 |- ((n e. NN /\ n <_ 1) -> (n - 1) = 0)
23	8, 22	sylan2 500	. . . . . . . . . . . . 13 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ n <_ 1)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
24	23	a1d 15	. . . . . . . . . . . 12 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ n <_ 1)) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
25		1nn 7117	. . . . . . . . . . . . . . . 16 |- 1 e. NN
26		nnsub 7141	. . . . . . . . . . . . . . . 16 |- ((1 e. NN /\ n e. NN) -> (1 < n <-> (n - 1) e. NN))
27	25, 26	mpan 759	. . . . . . . . . . . . . . 15 |- (n e. NN -> (1 < n <-> (n - 1) e. NN))
28	27	biimpa 460	. . . . . . . . . . . . . 14 |- ((n e. NN /\ 1 < n) -> (n - 1) e. NN)
29		opreq1 4889	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (m^j) = ((n - 1)^j))
30		opreq2 4890	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (M^m) = (M^(n - 1)))
31	29, 30	opreq12d 4900	. . . . . . . . . . . . . . . 16 |- (m = (n - 1) -> ((m^j) x. (M^m)) = (((n - 1)^j) x. (M^(n - 1))))
32		fveq2 4681	. . . . . . . . . . . . . . . . 17 |- (m = (n - 1) -> (!` m) = (!` (n - 1)))
33	32	opreq2d 4898	. . . . . . . . . . . . . . . 16 |- (m = (n - 1) -> (((2^(j^2)) x. (M^(M + j))) x. (!` m)) = (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))))
34	31, 33	breq12d 3351	. . . . . . . . . . . . . . 15 |- (m = (n - 1) -> (((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) <-> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
35	34	rcla4v 2376	. . . . . . . . . . . . . 14 |- ((n - 1) e. NN -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
36	28, 35	syl 12	. . . . . . . . . . . . 13 |- ((n e. NN /\ 1 < n) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
37	36	adantl 424	. . . . . . . . . . . 12 |- (((M e. NN0 /\ j e. NN0) /\ (n e. NN /\ 1 < n)) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
38	24, 37	jaodan 471	. . . . . . . . . . 11 |- (((M e. NN0 /\ j e. NN0) /\ ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n))) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
39		lelttric 6805	. . . . . . . . . . . . . 14 |- ((n e. RR /\ 1 e. RR) -> (n <_ 1 \/ 1 < n))
40	39, 12, 13	sylancl 525	. . . . . . . . . . . . 13 |- (n e. NN -> (n <_ 1 \/ 1 < n))
41	40	ancli 320	. . . . . . . . . . . 12 |- (n e. NN -> (n e. NN /\ (n <_ 1 \/ 1 < n)))
42		andi 665	. . . . . . . . . . . 12 |- ((n e. NN /\ (n <_ 1 \/ 1 < n)) <-> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
43	41, 42	sylib 215	. . . . . . . . . . 11 |- (n e. NN -> ((n e. NN /\ n <_ 1) \/ (n e. NN /\ 1 < n)))
44	38, 43	sylan2 500	. . . . . . . . . 10 |- (((M e. NN0 /\ j e. NN0) /\ n e. NN) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> (((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1)))))
45		faclbnd4lem2 8201	. . . . . . . . . . 11 |- ((M e. NN0 /\ j e. NN0 /\ n e. NN) -> ((((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))) -> ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
46	45	3expa 1067	. . . . . . . . . 10 |- (((M e. NN0 /\ j e. NN0) /\ n e. NN) -> ((((n - 1)^j) x. (M^(n - 1))) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` (n - 1))) -> ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
47	44, 46	syld 30	. . . . . . . . 9 |- (((M e. NN0 /\ j e. NN0) /\ n e. NN) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
48	47	r19.21adva 2182	. . . . . . . 8 |- ((M e. NN0 /\ j e. NN0) -> (A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)) -> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
49		opreq1 4889	. . . . . . . . . . 11 |- (n = m -> (n^j) = (m^j))
50		opreq2 4890	. . . . . . . . . . 11 |- (n = m -> (M^n) = (M^m))
51	49, 50	opreq12d 4900	. . . . . . . . . 10 |- (n = m -> ((n^j) x. (M^n)) = ((m^j) x. (M^m)))
52		fveq2 4681	. . . . . . . . . . 11 |- (n = m -> (!` n) = (!` m))
53	52	opreq2d 4898	. . . . . . . . . 10 |- (n = m -> (((2^(j^2)) x. (M^(M + j))) x. (!` n)) = (((2^(j^2)) x. (M^(M + j))) x. (!` m)))
54	51, 53	breq12d 3351	. . . . . . . . 9 |- (n = m -> (((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n)) <-> ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m))))
55	54	cbvralv 2280	. . . . . . . 8 |- (A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n)) <-> A.m e. NN ((m^j) x. (M^m)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` m)))
56	48, 55	syl5ib 223	. . . . . . 7 |- ((M e. NN0 /\ j e. NN0) -> (A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n)) -> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
57	56	expcom 403	. . . . . 6 |- (j e. NN0 -> (M e. NN0 -> (A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n)) -> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n)))))
58	57	a2d 16	. . . . 5 |- (j e. NN0 -> ((M e. NN0 -> A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n))) -> (M e. NN0 -> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n)))))
59		faclbnd3 8199	. . . . . . . 8 |- ((M e. NN0 /\ n e. NN0) -> (M^n) <_ ((M^M) x. (!` n)))
60		nnnn0 7315	. . . . . . . 8 |- (n e. NN -> n e. NN0)
61	59, 60	sylan2 500	. . . . . . 7 |- ((M e. NN0 /\ n e. NN) -> (M^n) <_ ((M^M) x. (!` n)))
62		nncn 7113	. . . . . . . . . . 11 |- (n e. NN -> n e. CC)
63		exp0 7814	. . . . . . . . . . 11 |- (n e. CC -> (n^0) = 1)
64	62, 63	syl 12	. . . . . . . . . 10 |- (n e. NN -> (n^0) = 1)
65	64	opreq1d 4897	. . . . . . . . 9 |- (n e. NN -> ((n^0) x. (M^n)) = (1 x. (M^n)))
66	65	adantl 424	. . . . . . . 8 |- ((M e. NN0 /\ n e. NN) -> ((n^0) x. (M^n)) = (1 x. (M^n)))
67		expcl 7824	. . . . . . . . . 10 |- ((M e. CC /\ n e. NN0) -> (M^n) e. CC)
68		nn0cn 7318	. . . . . . . . . 10 |- (M e. NN0 -> M e. CC)
69	67, 68, 60	syl2an 503	. . . . . . . . 9 |- ((M e. NN0 /\ n e. NN) -> (M^n) e. CC)
70		mulid2 6578	. . . . . . . . 9 |- ((M^n) e. CC -> (1 x. (M^n)) = (M^n))
71	69, 70	syl 12	. . . . . . . 8 |- ((M e. NN0 /\ n e. NN) -> (1 x. (M^n)) = (M^n))
72	66, 71	eqtrd 1925	. . . . . . 7 |- ((M e. NN0 /\ n e. NN) -> ((n^0) x. (M^n)) = (M^n))
73		sq0 7880	. . . . . . . . . . . . . 14 |- (0^2) = 0
74	73	opreq2i 4893	. . . . . . . . . . . . 13 |- (2^(0^2)) = (2^0)
75		2cn 7164	. . . . . . . . . . . . . 14 |- 2 e. CC
76		exp0 7814	. . . . . . . . . . . . . 14 |- (2 e. CC -> (2^0) = 1)
77	75, 76	ax-mp 7	. . . . . . . . . . . . 13 |- (2^0) = 1
78	74, 77	eqtri 1908	. . . . . . . . . . . 12 |- (2^(0^2)) = 1
79	78	a1i 8	. . . . . . . . . . 11 |- (M e. NN0 -> (2^(0^2)) = 1)
80		addid1 6463	. . . . . . . . . . . . 13 |- (M e. CC -> (M + 0) = M)
81	68, 80	syl 12	. . . . . . . . . . . 12 |- (M e. NN0 -> (M + 0) = M)
82	81	opreq2d 4898	. . . . . . . . . . 11 |- (M e. NN0 -> (M^(M + 0)) = (M^M))
83	79, 82	opreq12d 4900	. . . . . . . . . 10 |- (M e. NN0 -> ((2^(0^2)) x. (M^(M + 0))) = (1 x. (M^M)))
84		expcl 7824	. . . . . . . . . . . 12 |- ((M e. CC /\ M e. NN0) -> (M^M) e. CC)
85	68, 84	mpancom 769	. . . . . . . . . . 11 |- (M e. NN0 -> (M^M) e. CC)
86		mulid2 6578	. . . . . . . . . . 11 |- ((M^M) e. CC -> (1 x. (M^M)) = (M^M))
87	85, 86	syl 12	. . . . . . . . . 10 |- (M e. NN0 -> (1 x. (M^M)) = (M^M))
88	83, 87	eqtrd 1925	. . . . . . . . 9 |- (M e. NN0 -> ((2^(0^2)) x. (M^(M + 0))) = (M^M))
89	88	opreq1d 4897	. . . . . . . 8 |- (M e. NN0 -> (((2^(0^2)) x. (M^(M + 0))) x. (!` n)) = ((M^M) x. (!` n)))
90	89	adantr 425	. . . . . . 7 |- ((M e. NN0 /\ n e. NN) -> (((2^(0^2)) x. (M^(M + 0))) x. (!` n)) = ((M^M) x. (!` n)))
91	61, 72, 90	3brtr4d 3367	. . . . . 6 |- ((M e. NN0 /\ n e. NN) -> ((n^0) x. (M^n)) <_ (((2^(0^2)) x. (M^(M + 0))) x. (!` n)))
92	91	r19.21aiva 2176	. . . . 5 |- (M e. NN0 -> A.n e. NN ((n^0) x. (M^n)) <_ (((2^(0^2)) x. (M^(M + 0))) x. (!` n)))
93		opreq2 4890	. . . . . . . . 9 |- (m = 0 -> (n^m) = (n^0))
94	93	opreq1d 4897	. . . . . . . 8 |- (m = 0 -> ((n^m) x. (M^n)) = ((n^0) x. (M^n)))
95		opreq1 4889	. . . . . . . . . . 11 |- (m = 0 -> (m^2) = (0^2))
96	95	opreq2d 4898	. . . . . . . . . 10 |- (m = 0 -> (2^(m^2)) = (2^(0^2)))
97		opreq2 4890	. . . . . . . . . . 11 |- (m = 0 -> (M + m) = (M + 0))
98	97	opreq2d 4898	. . . . . . . . . 10 |- (m = 0 -> (M^(M + m)) = (M^(M + 0)))
99	96, 98	opreq12d 4900	. . . . . . . . 9 |- (m = 0 -> ((2^(m^2)) x. (M^(M + m))) = ((2^(0^2)) x. (M^(M + 0))))
100	99	opreq1d 4897	. . . . . . . 8 |- (m = 0 -> (((2^(m^2)) x. (M^(M + m))) x. (!` n)) = (((2^(0^2)) x. (M^(M + 0))) x. (!` n)))
101	94, 100	breq12d 3351	. . . . . . 7 |- (m = 0 -> (((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> ((n^0) x. (M^n)) <_ (((2^(0^2)) x. (M^(M + 0))) x. (!` n))))
102	101	ralbidv 2123	. . . . . 6 |- (m = 0 -> (A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> A.n e. NN ((n^0) x. (M^n)) <_ (((2^(0^2)) x. (M^(M + 0))) x. (!` n))))
103	102	imbi2d 674	. . . . 5 |- (m = 0 -> ((M e. NN0 -> A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n))) <-> (M e. NN0 -> A.n e. NN ((n^0) x. (M^n)) <_ (((2^(0^2)) x. (M^(M + 0))) x. (!` n)))))
104		opreq2 4890	. . . . . . . . 9 |- (m = j -> (n^m) = (n^j))
105	104	opreq1d 4897	. . . . . . . 8 |- (m = j -> ((n^m) x. (M^n)) = ((n^j) x. (M^n)))
106		opreq1 4889	. . . . . . . . . . 11 |- (m = j -> (m^2) = (j^2))
107	106	opreq2d 4898	. . . . . . . . . 10 |- (m = j -> (2^(m^2)) = (2^(j^2)))
108		opreq2 4890	. . . . . . . . . . 11 |- (m = j -> (M + m) = (M + j))
109	108	opreq2d 4898	. . . . . . . . . 10 |- (m = j -> (M^(M + m)) = (M^(M + j)))
110	107, 109	opreq12d 4900	. . . . . . . . 9 |- (m = j -> ((2^(m^2)) x. (M^(M + m))) = ((2^(j^2)) x. (M^(M + j))))
111	110	opreq1d 4897	. . . . . . . 8 |- (m = j -> (((2^(m^2)) x. (M^(M + m))) x. (!` n)) = (((2^(j^2)) x. (M^(M + j))) x. (!` n)))
112	105, 111	breq12d 3351	. . . . . . 7 |- (m = j -> (((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n))))
113	112	ralbidv 2123	. . . . . 6 |- (m = j -> (A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n))))
114	113	imbi2d 674	. . . . 5 |- (m = j -> ((M e. NN0 -> A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n))) <-> (M e. NN0 -> A.n e. NN ((n^j) x. (M^n)) <_ (((2^(j^2)) x. (M^(M + j))) x. (!` n)))))
115		opreq2 4890	. . . . . . . . 9 |- (m = (j + 1) -> (n^m) = (n^(j + 1)))
116	115	opreq1d 4897	. . . . . . . 8 |- (m = (j + 1) -> ((n^m) x. (M^n)) = ((n^(j + 1)) x. (M^n)))
117		opreq1 4889	. . . . . . . . . . 11 |- (m = (j + 1) -> (m^2) = ((j + 1)^2))
118	117	opreq2d 4898	. . . . . . . . . 10 |- (m = (j + 1) -> (2^(m^2)) = (2^((j + 1)^2)))
119		opreq2 4890	. . . . . . . . . . 11 |- (m = (j + 1) -> (M + m) = (M + (j + 1)))
120	119	opreq2d 4898	. . . . . . . . . 10 |- (m = (j + 1) -> (M^(M + m)) = (M^(M + (j + 1))))
121	118, 120	opreq12d 4900	. . . . . . . . 9 |- (m = (j + 1) -> ((2^(m^2)) x. (M^(M + m))) = ((2^((j + 1)^2)) x. (M^(M + (j + 1)))))
122	121	opreq1d 4897	. . . . . . . 8 |- (m = (j + 1) -> (((2^(m^2)) x. (M^(M + m))) x. (!` n)) = (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n)))
123	116, 122	breq12d 3351	. . . . . . 7 |- (m = (j + 1) -> (((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
124	123	ralbidv 2123	. . . . . 6 |- (m = (j + 1) -> (A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n))))
125	124	imbi2d 674	. . . . 5 |- (m = (j + 1) -> ((M e. NN0 -> A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n))) <-> (M e. NN0 -> A.n e. NN ((n^(j + 1)) x. (M^n)) <_ (((2^((j + 1)^2)) x. (M^(M + (j + 1)))) x. (!` n)))))
126		opreq2 4890	. . . . . . . . 9 |- (m = K -> (n^m) = (n^K))
127	126	opreq1d 4897	. . . . . . . 8 |- (m = K -> ((n^m) x. (M^n)) = ((n^K) x. (M^n)))
128		opreq1 4889	. . . . . . . . . . 11 |- (m = K -> (m^2) = (K^2))
129	128	opreq2d 4898	. . . . . . . . . 10 |- (m = K -> (2^(m^2)) = (2^(K^2)))
130		opreq2 4890	. . . . . . . . . . 11 |- (m = K -> (M + m) = (M + K))
131	130	opreq2d 4898	. . . . . . . . . 10 |- (m = K -> (M^(M + m)) = (M^(M + K)))
132	129, 131	opreq12d 4900	. . . . . . . . 9 |- (m = K -> ((2^(m^2)) x. (M^(M + m))) = ((2^(K^2)) x. (M^(M + K))))
133	132	opreq1d 4897	. . . . . . . 8 |- (m = K -> (((2^(m^2)) x. (M^(M + m))) x. (!` n)) = (((2^(K^2)) x. (M^(M + K))) x. (!` n)))
134	127, 133	breq12d 3351	. . . . . . 7 |- (m = K -> (((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n))))
135	134	ralbidv 2123	. . . . . 6 |- (m = K -> (A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n)) <-> A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n))))
136	135	imbi2d 674	. . . . 5 |- (m = K -> ((M e. NN0 -> A.n e. NN ((n^m) x. (M^n)) <_ (((2^(m^2)) x. (M^(M + m))) x. (!` n))) <-> (M e. NN0 -> A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n)))))
137	58, 92, 103, 114, 125, 136	nn0indALT 7425	. . . 4 |- (K e. NN0 -> (M e. NN0 -> A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n))))
138	137	imp 377	. . 3 |- ((K e. NN0 /\ M e. NN0) -> A.n e. NN ((n^K) x. (M^n)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` n)))
139	7, 138	sylan2 500	. 2 |- ((N e. NN /\ (K e. NN0 /\ M e. NN0)) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))
140	139	3impb 1063	1 |- ((N e. NN /\ K e. NN0 /\ M e. NN0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105   class class class wbr 3338  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   <_ cle 6448  NNcn 6449  NN0cn0 6450   < clt 6653  2c2 7145  ^cexp 7811  !cfa 8183

This theorem is referenced by:  faclbnd4 8204

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-2 7154  df-n0 7309  df-z 7345  df-seq1 7721  df-exp 7812  df-fac 8184

Copyright terms: Public domain