HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem sin01bndlem1 7409
Description: Lemma for sin01bnd 7414 and cos01bnd 7415.
Assertion
Ref Expression
sin01bndlem1 |- (5 / ((!` 4) x. 4)) < (1 / 6)
Proof of Theorem sin01bndlem1
StepHypRef Expression
1 3pos 5938 . . . . . 6 |- 0 < 3
2 0re 5412 . . . . . . 7 |- 0 e. RR
3 3re 5928 . . . . . . 7 |- 3 e. RR
4 5re 5930 . . . . . . 7 |- 5 e. RR
52, 3, 4ltadd1 5565 . . . . . 6 |- (0 < 3 <-> (0 + 5) < (3 + 5))
61, 5mpbi 189 . . . . 5 |- (0 + 5) < (3 + 5)
74recn 5286 . . . . . 6 |- 5 e. CC
87addid2 5303 . . . . 5 |- (0 + 5) = 5
9 cu2 6571 . . . . . 6 |- (2^3) = 8
10 5p3e8 5960 . . . . . 6 |- (5 + 3) = 8
11 3nn 5947 . . . . . . . 8 |- 3 e. NN
1211nncn 5880 . . . . . . 7 |- 3 e. CC
137, 12addcom 5294 . . . . . 6 |- (5 + 3) = (3 + 5)
149, 10, 133eqtr2r 1494 . . . . 5 |- (3 + 5) = (2^3)
156, 8, 143brtr3 2632 . . . 4 |- 5 < (2^3)
16 2nn 5946 . . . . . 6 |- 2 e. NN
17 nnge1t 5891 . . . . . 6 |- (2 e. NN -> 1 <_ 2)
1816, 17ax-mp 7 . . . . 5 |- 1 <_ 2
19 lep1t 5768 . . . . . . 7 |- (3 e. RR -> 3 <_ (3 + 1))
203, 19ax-mp 7 . . . . . 6 |- 3 <_ (3 + 1)
21 df-4 5919 . . . . . 6 |- 4 = (3 + 1)
2220, 21breqtrr 2630 . . . . 5 |- 3 <_ 4
23 2re 5926 . . . . . . 7 |- 2 e. RR
2411nnnn0 6054 . . . . . . 7 |- 3 e. NN0
25 4nn 5949 . . . . . . . 8 |- 4 e. NN
2625nnnn0 6054 . . . . . . 7 |- 4 e. NN0
2723, 24, 263pm3.2i 816 . . . . . 6 |- (2 e. RR /\ 3 e. NN0 /\ 4 e. NN0)
28 expwordit 6534 . . . . . 6 |- (((2 e. RR /\ 3 e. NN0 /\ 4 e. NN0) /\ (1 <_ 2 /\ 3 <_ 4)) -> (2^3) <_ (2^4))
2927, 28mpan 693 . . . . 5 |- ((1 <_ 2 /\ 3 <_ 4) -> (2^3) <_ (2^4))
3018, 22, 29mp2an 695 . . . 4 |- (2^3) <_ (2^4)
31 8re 5933 . . . . . 6 |- 8 e. RR
329, 31eqeltr 1536 . . . . 5 |- (2^3) e. RR
33 nnexpclt 6508 . . . . . . 7 |- ((2 e. NN /\ 4 e. NN0) -> (2^4) e. NN)
3416, 26, 33mp2an 695 . . . . . 6 |- (2^4) e. NN
3534nnre 5879 . . . . 5 |- (2^4) e. RR
364, 32, 35ltletr 5561 . . . 4 |- ((5 < (2^3) /\ (2^3) <_ (2^4)) -> 5 < (2^4))
3715, 30, 36mp2an 695 . . 3 |- 5 < (2^4)
38 6re 5931 . . . . 5 |- 6 e. RR
3938, 35remulcl 5307 . . . 4 |- (6 x. (2^4)) e. RR
40 6pos 5941 . . . . 5 |- 0 < 6
4134nngt0 5898 . . . . 5 |- 0 < (2^4)
4238, 35, 40, 41mulgt0i 5582 . . . 4 |- 0 < (6 x. (2^4))
434, 35, 39, 42ltdiv1i 5779 . . 3 |- (5 < (2^4) <-> (5 / (6 x. (2^4))) < ((2^4) / (6 x. (2^4))))
4437, 43mpbi 189 . 2 |- (5 / (6 x. (2^4))) < ((2^4) / (6 x. (2^4)))
4521fveq2i 3712 . . . . . . 7 |- (!` 4) = (!` (3 + 1))
46 facp1t 6873 . . . . . . . 8 |- (3 e. NN0 -> (!` (3 + 1)) = ((!` 3) x. (3 + 1)))
4724, 46ax-mp 7 . . . . . . 7 |- (!` (3 + 1)) = ((!` 3) x. (3 + 1))
48 sq2 6569 . . . . . . . . 9 |- (2^2) = 4
4948, 21eqtr2 1488 . . . . . . . 8 |- (3 + 1) = (2^2)
5049opreq2i 3957 . . . . . . 7 |- ((!` 3) x. (3 + 1)) = ((!` 3) x. (2^2))
5145, 47, 503eqtr 1491 . . . . . 6 |- (!` 4) = ((!` 3) x. (2^2))
5251opreq1i 3956 . . . . 5 |- ((!` 4) x. (2^2)) = (((!` 3) x. (2^2)) x. (2^2))
5348opreq2i 3957 . . . . 5 |- ((!` 4) x. (2^2)) = ((!` 4) x. 4)
54 fac3 6875 . . . . . . 7 |- (!` 3) = 6
5538recn 5286 . . . . . . 7 |- 6 e. CC
5654, 55eqeltr 1536 . . . . . 6 |- (!` 3) e. CC
57 4re 5929 . . . . . . . 8 |- 4 e. RR
5857recn 5286 . . . . . . 7 |- 4 e. CC
5948, 58eqeltr 1536 . . . . . 6 |- (2^2) e. CC
6056, 59, 59mulass 5297 . . . . 5 |- (((!` 3) x. (2^2)) x. (2^2)) = ((!` 3) x. ((2^2) x. (2^2)))
6152, 53, 603eqtr3 1495 . . . 4 |- ((!` 4) x. 4) = ((!` 3) x. ((2^2) x. (2^2)))
62 2p2e4 5948 . . . . . . 7 |- (2 + 2) = 4
6362opreq2i 3957 . . . . . 6 |- (2^(2 + 2)) = (2^4)
64 2cn 5927 . . . . . . 7 |- 2 e. CC
65 2nn0 6062 . . . . . . 7 |- 2 e. NN0
66 expaddt 6527 . . . . . . 7 |- ((2 e. CC /\ 2 e. NN0 /\ 2 e. NN0) -> (2^(2 + 2)) = ((2^2) x. (2^2)))
6764, 65, 65, 66mp3an 913 . . . . . 6 |- (2^(2 + 2)) = ((2^2) x. (2^2))
6863, 67eqtr3 1489 . . . . 5 |- (2^4) = ((2^2) x. (2^2))
6968opreq2i 3957 . . . 4 |- ((!` 3) x. (2^4)) = ((!` 3) x. ((2^2) x. (2^2)))
7054opreq1i 3956 . . . 4 |- ((!` 3) x. (2^4)) = (6 x. (2^4))
7161, 69, 703eqtr2 1493 . . 3 |- ((!` 4) x. 4) = (6 x. (2^4))
7271opreq2i 3957 . 2 |- (5 / ((!` 4) x. 4)) = (5 / (6 x. (2^4)))
7334nncn 5880 . . . . . 6 |- (2^4) e. CC
7434nnne0 5899 . . . . . 6 |- (2^4) =/= 0
7573, 74divid 5726 . . . . 5 |- ((2^4) / (2^4)) = 1
7675opreq2i 3957 . . . 4 |- ((1 / 6) x. ((2^4) / (2^4))) = ((1 / 6) x. 1)
77 ax1cn 5241 . . . . 5 |- 1 e. CC
7838, 40gt0ne0i 5591 . . . . 5 |- 6 =/= 0
7977, 55, 73, 73, 78, 74divmuldiv 5742 . . . 4 |- ((1 / 6) x. ((2^4) / (2^4))) = ((1 x. (2^4)) / (6 x. (2^4)))
8055, 78reccl 5682 . . . . 5 |- (1 / 6) e. CC
8180mulid1 5304 . . . 4 |- ((1 / 6) x. 1) = (1 / 6)
8276, 79, 813eqtr3 1495 . . 3 |- ((1 x. (2^4)) / (6 x. (2^4))) = (1 / 6)
8373mulid2 5305 . . . 4 |- (1 x. (2^4)) = (2^4)
8483opreq1i 3956 . . 3 |- ((1 x. (2^4)) / (6 x. (2^4))) = ((2^4) / (6 x. (2^4)))
8582, 84eqtr3 1489 . 2 |- (1 / 6) = ((2^4) / (6 x. (2^4)))
8644, 72, 853brtr4 2633 1 |- (5 / ((!` 4) x. 4)) < (1 / 6)
Colors of variables: wff set class
Syntax hints:   /\ wa 223   /\ w3a 773   = wceq 953   e. wcel 955   class class class wbr 2609  ` cfv 3172  (class class class)co 3948  CCcc 5204  RRcr 5205  0cc0 5206  1c1 5207   + caddc 5209   x. cmul 5211   / cdiv 5266   <_ cle 5267  NNcn 5268  NN0cn0 5269   < clt 5458  2c2 5908  3c3 5909  4c4 5910  5c5 5911  6c6 5912  8c8 5914  ^cexp 6500  !cfa 6868
This theorem is referenced by:  sin01bndlem2 7410  cos01bndlem2 7412
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-oadd 4119  df-omul 4120  df-er 4245  df-ec 4247  df-qs 4250  df-en 4351  df-dom 4352  df-sdom 4353  df-ni 4972  df-pli 4973  df-mi 4974  df-lti 4975  df-plpq 5007  df-mpq 5008  df-enq 5009  df-nq 5010  df-plq 5011  df-mq 5012  df-rq 5013  df-ltq 5014  df-1q 5015  df-np 5058  df-1p 5059  df-plp 5060  df-mp 5061  df-ltp 5062  df-plpr 5136  df-mpr 5137  df-enr 5138  df-nr 5139  df-plr 5140  df-mr 5141  df-ltr 5142  df-0r 5143  df-1r 5144  df-m1r 5145  df-c 5212  df-0 5213  df-1 5214  df-i 5215  df-r 5216  df-plus 5217  df-mul 5218  df-lt 5219  df-sub 5328  df-neg 5330  df-pnf 5459  df-mnf 5460  df-xr 5461  df-ltxr 5462  df-le 5463  df-div 5672  df-n 5873  df-2 5917  df-3 5918  df-4 5919  df-5 5920  df-6 5921  df-7 5922  df-8 5923  df-n0 6047  df-z 6083  df-seq1 6245  df-exp 6501  df-fac 6869
Copyright terms: Public domain