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 e. NN /\ K e. NN0 /\ M e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )

Proof

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

Metamath Proof Explorer

Theorem faclbnd4lem4

Proof