Theorem faclbnd4lem3 8587

Description: Lemma for faclbnd4 8589. The N = 0 case.

Assertion

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

Proof of Theorem faclbnd4lem3

Step	Hyp	Ref	Expression
1		elnn0 7650	. . . . 5 |- (K e. NN0 <-> (K e. NN \/ K = 0))
2		0exp 8216	. . . . . . . 8 |- (K e. NN -> (0^K) = 0)
3	2	adantl 448	. . . . . . 7 |- ((M e. NN0 /\ K e. NN) -> (0^K) = 0)
4		nnnn0 7655	. . . . . . . . 9 |- (K e. NN -> K e. NN0)
5		2nn0 7665	. . . . . . . . . . . 12 |- 2 e. NN0
6		nn0expcl 8204	. . . . . . . . . . . . 13 |- ((K e. NN0 /\ 2 e. NN0) -> (K^2) e. NN0)
7	5, 6	mpan2 679	. . . . . . . . . . . 12 |- (K e. NN0 -> (K^2) e. NN0)
8		nn0expcl 8204	. . . . . . . . . . . 12 |- ((2 e. NN0 /\ (K^2) e. NN0) -> (2^(K^2)) e. NN0)
9	5, 7, 8	sylancr 662	. . . . . . . . . . 11 |- (K e. NN0 -> (2^(K^2)) e. NN0)
10	9	adantl 448	. . . . . . . . . 10 |- ((M e. NN0 /\ K e. NN0) -> (2^(K^2)) e. NN0)
11		nn0addcl 7670	. . . . . . . . . . 11 |- ((M e. NN0 /\ K e. NN0) -> (M + K) e. NN0)
12		nn0expcl 8204	. . . . . . . . . . 11 |- ((M e. NN0 /\ (M + K) e. NN0) -> (M^(M + K)) e. NN0)
13	11, 12	syldan 595	. . . . . . . . . 10 |- ((M e. NN0 /\ K e. NN0) -> (M^(M + K)) e. NN0)
14		nn0mulcl 7673	. . . . . . . . . 10 |- (((2^(K^2)) e. NN0 /\ (M^(M + K)) e. NN0) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
15	10, 13, 14	syl11anc 659	. . . . . . . . 9 |- ((M e. NN0 /\ K e. NN0) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
16	4, 15	sylan2 600	. . . . . . . 8 |- ((M e. NN0 /\ K e. NN) -> ((2^(K^2)) x. (M^(M + K))) e. NN0)
17		nn0ge0 7667	. . . . . . . 8 |- (((2^(K^2)) x. (M^(M + K))) e. NN0 -> 0 <_ ((2^(K^2)) x. (M^(M + K))))
18	16, 17	syl 13	. . . . . . 7 |- ((M e. NN0 /\ K e. NN) -> 0 <_ ((2^(K^2)) x. (M^(M + K))))
19	3, 18	eqbrtrd 3527	. . . . . 6 |- ((M e. NN0 /\ K e. NN) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
20		elnn0 7650	. . . . . . . . . 10 |- (M e. NN0 <-> (M e. NN \/ M = 0))
21		nnnn0 7655	. . . . . . . . . . . . 13 |- (M e. NN -> M e. NN0)
22		0nn0 7663	. . . . . . . . . . . . 13 |- 0 e. NN0
23		nn0addcl 7670	. . . . . . . . . . . . 13 |- ((M e. NN0 /\ 0 e. NN0) -> (M + 0) e. NN0)
24	21, 22, 23	sylancl 660	. . . . . . . . . . . 12 |- (M e. NN -> (M + 0) e. NN0)
25		nnexpcl 8203	. . . . . . . . . . . 12 |- ((M e. NN /\ (M + 0) e. NN0) -> (M^(M + 0)) e. NN)
26	24, 25	mpdan 673	. . . . . . . . . . 11 |- (M e. NN -> (M^(M + 0)) e. NN)
27		id 15	. . . . . . . . . . . . . 14 |- (M = 0 -> M = 0)
28		opreq1 4986	. . . . . . . . . . . . . . 15 |- (M = 0 -> (M + 0) = (0 + 0))
29		0cn 6831	. . . . . . . . . . . . . . . 16 |- 0 e. CC
30	29	addid1i 6978	. . . . . . . . . . . . . . 15 |- (0 + 0) = 0
31	28, 30	syl6eq 2193	. . . . . . . . . . . . . 14 |- (M = 0 -> (M + 0) = 0)
32	27, 31	opreq12d 4996	. . . . . . . . . . . . 13 |- (M = 0 -> (M^(M + 0)) = (0^0))
33		exp0 8198	. . . . . . . . . . . . . 14 |- (0 e. CC -> (0^0) = 1)
34	29, 33	ax-mp 7	. . . . . . . . . . . . 13 |- (0^0) = 1
35	32, 34	syl6eq 2193	. . . . . . . . . . . 12 |- (M = 0 -> (M^(M + 0)) = 1)
36		1nn 7450	. . . . . . . . . . . 12 |- 1 e. NN
37	35, 36	syl6eqel 2230	. . . . . . . . . . 11 |- (M = 0 -> (M^(M + 0)) e. NN)
38	26, 37	jaoi 453	. . . . . . . . . 10 |- ((M e. NN \/ M = 0) -> (M^(M + 0)) e. NN)
39	20, 38	sylbi 225	. . . . . . . . 9 |- (M e. NN0 -> (M^(M + 0)) e. NN)
40		nnmulcl 7457	. . . . . . . . . 10 |- ((1 e. NN /\ (M^(M + 0)) e. NN) -> (1 x. (M^(M + 0))) e. NN)
41	36, 40	mpan 677	. . . . . . . . 9 |- ((M^(M + 0)) e. NN -> (1 x. (M^(M + 0))) e. NN)
42		nnge1 7459	. . . . . . . . 9 |- ((1 x. (M^(M + 0))) e. NN -> 1 <_ (1 x. (M^(M + 0))))
43	39, 41, 42	3syl 41	. . . . . . . 8 |- (M e. NN0 -> 1 <_ (1 x. (M^(M + 0))))
44	43	adantr 447	. . . . . . 7 |- ((M e. NN0 /\ K = 0) -> 1 <_ (1 x. (M^(M + 0))))
45		opreq2 4987	. . . . . . . . . 10 |- (K = 0 -> (0^K) = (0^0))
46	45, 34	syl6eq 2193	. . . . . . . . 9 |- (K = 0 -> (0^K) = 1)
47		sq0i 8265	. . . . . . . . . . . 12 |- (K = 0 -> (K^2) = 0)
48	47	opreq2d 4994	. . . . . . . . . . 11 |- (K = 0 -> (2^(K^2)) = (2^0))
49		2cn 7497	. . . . . . . . . . . 12 |- 2 e. CC
50		exp0 8198	. . . . . . . . . . . 12 |- (2 e. CC -> (2^0) = 1)
51	49, 50	ax-mp 7	. . . . . . . . . . 11 |- (2^0) = 1
52	48, 51	syl6eq 2193	. . . . . . . . . 10 |- (K = 0 -> (2^(K^2)) = 1)
53		opreq2 4987	. . . . . . . . . . 11 |- (K = 0 -> (M + K) = (M + 0))
54	53	opreq2d 4994	. . . . . . . . . 10 |- (K = 0 -> (M^(M + K)) = (M^(M + 0)))
55	52, 54	opreq12d 4996	. . . . . . . . 9 |- (K = 0 -> ((2^(K^2)) x. (M^(M + K))) = (1 x. (M^(M + 0))))
56	46, 55	breq12d 3520	. . . . . . . 8 |- (K = 0 -> ((0^K) <_ ((2^(K^2)) x. (M^(M + K))) <-> 1 <_ (1 x. (M^(M + 0)))))
57	56	adantl 448	. . . . . . 7 |- ((M e. NN0 /\ K = 0) -> ((0^K) <_ ((2^(K^2)) x. (M^(M + K))) <-> 1 <_ (1 x. (M^(M + 0)))))
58	44, 57	mpbird 318	. . . . . 6 |- ((M e. NN0 /\ K = 0) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
59	19, 58	jaodan 826	. . . . 5 |- ((M e. NN0 /\ (K e. NN \/ K = 0)) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
60	1, 59	sylan2b 601	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> (0^K) <_ ((2^(K^2)) x. (M^(M + K))))
61		nn0cn 7658	. . . . . . 7 |- (M e. NN0 -> M e. CC)
62		exp0 8198	. . . . . . 7 |- (M e. CC -> (M^0) = 1)
63	61, 62	syl 13	. . . . . 6 |- (M e. NN0 -> (M^0) = 1)
64	63	opreq2d 4994	. . . . 5 |- (M e. NN0 -> ((0^K) x. (M^0)) = ((0^K) x. 1))
65		nn0expcl 8204	. . . . . . 7 |- ((0 e. NN0 /\ K e. NN0) -> (0^K) e. NN0)
66	22, 65	mpan 677	. . . . . 6 |- (K e. NN0 -> (0^K) e. NN0)
67		nn0cn 7658	. . . . . 6 |- ((0^K) e. NN0 -> (0^K) e. CC)
68		mulid1 6832	. . . . . 6 |- ((0^K) e. CC -> ((0^K) x. 1) = (0^K))
69	66, 67, 68	3syl 41	. . . . 5 |- (K e. NN0 -> ((0^K) x. 1) = (0^K))
70	64, 69	sylan9eq 2197	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> ((0^K) x. (M^0)) = (0^K))
71		nn0cn 7658	. . . . 5 |- (((2^(K^2)) x. (M^(M + K))) e. NN0 -> ((2^(K^2)) x. (M^(M + K))) e. CC)
72		mulid1 6832	. . . . 5 |- (((2^(K^2)) x. (M^(M + K))) e. CC -> (((2^(K^2)) x. (M^(M + K))) x. 1) = ((2^(K^2)) x. (M^(M + K))))
73	15, 71, 72	3syl 41	. . . 4 |- ((M e. NN0 /\ K e. NN0) -> (((2^(K^2)) x. (M^(M + K))) x. 1) = ((2^(K^2)) x. (M^(M + K))))
74	60, 70, 73	3brtr4d 3537	. . 3 |- ((M e. NN0 /\ K e. NN0) -> ((0^K) x. (M^0)) <_ (((2^(K^2)) x. (M^(M + K))) x. 1))
75	74	adantr 447	. 2 |- (((M e. NN0 /\ K e. NN0) /\ N = 0) -> ((0^K) x. (M^0)) <_ (((2^(K^2)) x. (M^(M + K))) x. 1))
76		opreq1 4986	. . . . 5 |- (N = 0 -> (N^K) = (0^K))
77		opreq2 4987	. . . . 5 |- (N = 0 -> (M^N) = (M^0))
78	76, 77	opreq12d 4996	. . . 4 |- (N = 0 -> ((N^K) x. (M^N)) = ((0^K) x. (M^0)))
79		fveq2 4765	. . . . . 6 |- (N = 0 -> (!` N) = (!` 0))
80		fac0 8571	. . . . . 6 |- (!` 0) = 1
81	79, 80	syl6eq 2193	. . . . 5 |- (N = 0 -> (!` N) = 1)
82	81	opreq2d 4994	. . . 4 |- (N = 0 -> (((2^(K^2)) x. (M^(M + K))) x. (!` N)) = (((2^(K^2)) x. (M^(M + K))) x. 1))
83	78, 82	breq12d 3520	. . 3 |- (N = 0 -> (((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)) <-> ((0^K) x. (M^0)) <_ (((2^(K^2)) x. (M^(M + K))) x. 1)))
84	83	adantl 448	. 2 |- (((M e. NN0 /\ K e. NN0) /\ N = 0) -> (((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)) <-> ((0^K) x. (M^0)) <_ (((2^(K^2)) x. (M^(M + K))) x. 1)))
85	75, 84	mpbird 318	1 |- (((M e. NN0 /\ K e. NN0) /\ N = 0) -> ((N^K) x. (M^N)) <_ (((2^(K^2)) x. (M^(M + K))) x. (!` N)))

Syntax hints:   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   = wceq 1586   e. wcel 1588   class class class wbr 3507  ` cfv 4131  (class class class)co 4981  CCcc 6750  0cc0 6752  1c1 6753   + caddc 6755   x. cmul 6757   <_ cle 6841  NNcn 6992  NN0cn0 6993  2c2 7478  ^cexp 8195  !cfa 8568

This theorem is referenced by:  faclbnd4lem4 8588  faclbnd4 8589

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-n 7441  df-2 7487  df-n0 7649  df-z 7686  df-seq1 8094  df-exp 8196  df-fac 8569

Copyright terms: Public domain