ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  amgm2 Unicode version
Theorem amgm2 9714
Description: Arithmetic-geometric mean inequality for n = 2. (Contributed by Mario Carneiro, 2-Jul-2014.)
Assertion
Ref Expression
amgm2 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) )
Proof of Theorem amgm2
StepHypRef Expression
1 2cn 7986 . . . . . 6 |- 2 e. CC
2 simpll 481 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
3 simprl 483 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
4 remulcl 7009 . . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
52, 3, 4syl2anc 391 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A x. B ) e. RR )
6 mulge0 7610 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
7 resqrtcl 9627 . . . . . . . 8 |- ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> ( sqr ` ( A x. B ) ) e. RR )
85, 6, 7syl2anc 391 . . . . . . 7 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) e. RR )
98recnd 7054 . . . . . 6 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) e. CC )
10 sqmul 9316 . . . . . 6 |- ( ( 2 e. CC /\ ( sqr ` ( A x. B ) ) e. CC ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( sqr ` ( A x. B ) ) ^ 2 ) ) )
111, 9, 10sylancr 393 . . . . 5 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) ^ 2 ) = ( ( 2 ^ 2 ) x. ( ( sqr ` ( A x. B ) ) ^ 2 ) ) )
12 sq2 9349 . . . . . . 7 |- ( 2 ^ 2 ) = 4
1312oveq1i 5522 . . . . . 6 |- ( ( 2 ^ 2 ) x. ( ( sqr ` ( A x. B ) ) ^ 2 ) ) = ( 4 x. ( ( sqr ` ( A x. B ) ) ^ 2 ) )
14 resqrtth 9629 . . . . . . . 8 |- ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> ( ( sqr ` ( A x. B ) ) ^ 2 ) = ( A x. B ) )
155, 6, 14syl2anc 391 . . . . . . 7 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqr ` ( A x. B ) ) ^ 2 ) = ( A x. B ) )
1615oveq2d 5528 . . . . . 6 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 4 x. ( ( sqr ` ( A x. B ) ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )
1713, 16syl5eq 2084 . . . . 5 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 ^ 2 ) x. ( ( sqr ` ( A x. B ) ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )
1811, 17eqtrd 2072 . . . 4 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) ^ 2 ) = ( 4 x. ( A x. B ) ) )
192, 3resubcld 7379 . . . . . . 7 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A - B ) e. RR )
2019sqge0d 9407 . . . . . 6 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( ( A - B ) ^ 2 ) )
212recnd 7054 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. CC )
223recnd 7054 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. CC )
23 binom2 9362 . . . . . . . . . 10 |- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
2421, 22, 23syl2anc 391 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
25 binom2sub 9364 . . . . . . . . . 10 |- ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
2621, 22, 25syl2anc 391 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
2724, 26oveq12d 5530 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) - ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) ) )
282resqcld 9406 . . . . . . . . . . 11 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A ^ 2 ) e. RR )
29 2re 7985 . . . . . . . . . . . 12 |- 2 e. RR
30 remulcl 7009 . . . . . . . . . . . 12 |- ( ( 2 e. RR /\ ( A x. B ) e. RR ) -> ( 2 x. ( A x. B ) ) e. RR )
3129, 5, 30sylancr 393 . . . . . . . . . . 11 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 x. ( A x. B ) ) e. RR )
3228, 31readdcld 7055 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) e. RR )
3332recnd 7054 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) e. CC )
3428, 31resubcld 7379 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) e. RR )
3534recnd 7054 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) e. CC )
363resqcld 9406 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B ^ 2 ) e. RR )
3736recnd 7054 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B ^ 2 ) e. CC )
3833, 35, 37pnpcan2d 7360 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) - ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) ) )
3931recnd 7054 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 x. ( A x. B ) ) e. CC )
40392timesd 8167 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 x. ( 2 x. ( A x. B ) ) ) = ( ( 2 x. ( A x. B ) ) + ( 2 x. ( A x. B ) ) ) )
41 2t2e4 8069 . . . . . . . . . . 11 |- ( 2 x. 2 ) = 4
4241oveq1i 5522 . . . . . . . . . 10 |- ( ( 2 x. 2 ) x. ( A x. B ) ) = ( 4 x. ( A x. B ) )
43 2cnd 7988 . . . . . . . . . . 11 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 2 e. CC )
445recnd 7054 . . . . . . . . . . 11 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A x. B ) e. CC )
4543, 43, 44mulassd 7050 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. 2 ) x. ( A x. B ) ) = ( 2 x. ( 2 x. ( A x. B ) ) ) )
4642, 45syl5eqr 2086 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 4 x. ( A x. B ) ) = ( 2 x. ( 2 x. ( A x. B ) ) ) )
4728recnd 7054 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A ^ 2 ) e. CC )
4847, 39, 39pnncand 7361 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) ) = ( ( 2 x. ( A x. B ) ) + ( 2 x. ( A x. B ) ) ) )
4940, 46, 483eqtr4rd 2083 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) - ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) ) = ( 4 x. ( A x. B ) ) )
5027, 38, 493eqtrd 2076 . . . . . . 7 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )
512, 3readdcld 7055 . . . . . . . . . 10 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A + B ) e. RR )
5251resqcld 9406 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) ^ 2 ) e. RR )
5352recnd 7054 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A + B ) ^ 2 ) e. CC )
5419resqcld 9406 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A - B ) ^ 2 ) e. RR )
5554recnd 7054 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A - B ) ^ 2 ) e. CC )
56 4re 7992 . . . . . . . . . 10 |- 4 e. RR
57 remulcl 7009 . . . . . . . . . 10 |- ( ( 4 e. RR /\ ( A x. B ) e. RR ) -> ( 4 x. ( A x. B ) ) e. RR )
5856, 5, 57sylancr 393 . . . . . . . . 9 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 4 x. ( A x. B ) ) e. RR )
5958recnd 7054 . . . . . . . 8 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 4 x. ( A x. B ) ) e. CC )
60 subsub23 7216 . . . . . . . 8 |- ( ( ( ( A + B ) ^ 2 ) e. CC /\ ( ( A - B ) ^ 2 ) e. CC /\ ( 4 x. ( A x. B ) ) e. CC ) -> ( ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) <-> ( ( ( A + B ) ^ 2 ) - ( 4 x. ( A x. B ) ) ) = ( ( A - B ) ^ 2 ) ) )
6153, 55, 59, 60syl3anc 1135 . . . . . . 7 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) <-> ( ( ( A + B ) ^ 2 ) - ( 4 x. ( A x. B ) ) ) = ( ( A - B ) ^ 2 ) ) )
6250, 61mpbid 135 . . . . . 6 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( A + B ) ^ 2 ) - ( 4 x. ( A x. B ) ) ) = ( ( A - B ) ^ 2 ) )
6320, 62breqtrrd 3790 . . . . 5 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( ( ( A + B ) ^ 2 ) - ( 4 x. ( A x. B ) ) ) )
6452, 58subge0d 7526 . . . . 5 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 0 <_ ( ( ( A + B ) ^ 2 ) - ( 4 x. ( A x. B ) ) ) <-> ( 4 x. ( A x. B ) ) <_ ( ( A + B ) ^ 2 ) ) )
6563, 64mpbid 135 . . . 4 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 4 x. ( A x. B ) ) <_ ( ( A + B ) ^ 2 ) )
6618, 65eqbrtrd 3784 . . 3 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) ^ 2 ) <_ ( ( A + B ) ^ 2 ) )
67 remulcl 7009 . . . . 5 |- ( ( 2 e. RR /\ ( sqr ` ( A x. B ) ) e. RR ) -> ( 2 x. ( sqr ` ( A x. B ) ) ) e. RR )
6829, 8, 67sylancr 393 . . . 4 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 x. ( sqr ` ( A x. B ) ) ) e. RR )
69 sqrtge0 9631 . . . . . 6 |- ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> 0 <_ ( sqr ` ( A x. B ) ) )
705, 6, 69syl2anc 391 . . . . 5 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( sqr ` ( A x. B ) ) )
71 0le2 8006 . . . . . 6 |- 0 <_ 2
72 mulge0 7610 . . . . . 6 |- ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( ( sqr ` ( A x. B ) ) e. RR /\ 0 <_ ( sqr ` ( A x. B ) ) ) ) -> 0 <_ ( 2 x. ( sqr ` ( A x. B ) ) ) )
7329, 71, 72mpanl12 412 . . . . 5 |- ( ( ( sqr ` ( A x. B ) ) e. RR /\ 0 <_ ( sqr ` ( A x. B ) ) ) -> 0 <_ ( 2 x. ( sqr ` ( A x. B ) ) ) )
748, 70, 73syl2anc 391 . . . 4 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( 2 x. ( sqr ` ( A x. B ) ) ) )
75 addge0 7446 . . . . 5 |- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A + B ) )
7675an4s 522 . . . 4 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A + B ) )
7768, 51, 74, 76le2sqd 9412 . . 3 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) <_ ( A + B ) <-> ( ( 2 x. ( sqr ` ( A x. B ) ) ) ^ 2 ) <_ ( ( A + B ) ^ 2 ) ) )
7866, 77mpbird 156 . 2 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 x. ( sqr ` ( A x. B ) ) ) <_ ( A + B ) )
79 2pos 8007 . . . . 5 |- 0 < 2
8029, 79pm3.2i 257 . . . 4 |- ( 2 e. RR /\ 0 < 2 )
8180a1i 9 . . 3 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( 2 e. RR /\ 0 < 2 ) )
82 lemuldiv2 7848 . . 3 |- ( ( ( sqr ` ( A x. B ) ) e. RR /\ ( A + B ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) <_ ( A + B ) <-> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) ) )
838, 51, 81, 82syl3anc 1135 . 2 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( 2 x. ( sqr ` ( A x. B ) ) ) <_ ( A + B ) <-> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) ) )
8478, 83mpbid 135 1 |- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqr ` ( A x. B ) ) <_ ( ( A + B ) / 2 ) )
Colors of variables: wff set class
Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   = wceq 1243   e. wcel 1393   class class class wbr 3764   ` cfv 4902  (class class class)co 5512   CCcc 6887   RRcr 6888   0cc0 6889   + caddc 6892   x. cmul 6894   < clt 7060   <_ cle 7061   - cmin 7182   / cdiv 7651   2c2 7964   4c4 7966   ^cexp 9254   sqrcsqrt 9594
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-13 1404  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-coll 3872  ax-sep 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944  ax-un 4170  ax-setind 4262  ax-iinf 4311  ax-cnex 6975  ax-resscn 6976  ax-1cn 6977  ax-1re 6978  ax-icn 6979  ax-addcl 6980  ax-addrcl 6981  ax-mulcl 6982  ax-mulrcl 6983  ax-addcom 6984  ax-mulcom 6985  ax-addass 6986  ax-mulass 6987  ax-distr 6988  ax-i2m1 6989  ax-1rid 6991  ax-0id 6992  ax-rnegex 6993  ax-precex 6994  ax-cnre 6995  ax-pre-ltirr 6996  ax-pre-ltwlin 6997  ax-pre-lttrn 6998  ax-pre-apti 6999  ax-pre-ltadd 7000  ax-pre-mulgt0 7001  ax-pre-mulext 7002  ax-arch 7003  ax-caucvg 7004
This theorem depends on definitions:  df-bi 110  df-dc 743  df-3or 886  df-3an 887  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-nel 2207  df-ral 2311  df-rex 2312  df-reu 2313  df-rmo 2314  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-if 3332  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-int 3616  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-eprel 4026  df-id 4030  df-po 4033  df-iso 4034  df-iord 4103  df-on 4105  df-suc 4108  df-iom 4314  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-rn 4356  df-res 4357  df-ima 4358  df-iota 4867  df-fun 4904  df-fn 4905  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909  df-fv 4910  df-riota 5468  df-ov 5515  df-oprab 5516  df-mpt2 5517  df-1st 5767  df-2nd 5768  df-recs 5920  df-irdg 5957  df-frec 5978  df-1o 6001  df-2o 6002  df-oadd 6005  df-omul 6006  df-er 6106  df-ec 6108  df-qs 6112  df-ni 6402  df-pli 6403  df-mi 6404  df-lti 6405  df-plpq 6442  df-mpq 6443  df-enq 6445  df-nqqs 6446  df-plqqs 6447  df-mqqs 6448  df-1nqqs 6449  df-rq 6450  df-ltnqqs 6451  df-enq0 6522  df-nq0 6523  df-0nq0 6524  df-plq0 6525  df-mq0 6526  df-inp 6564  df-i1p 6565  df-iplp 6566  df-iltp 6568  df-enr 6811  df-nr 6812  df-ltr 6815  df-0r 6816  df-1r 6817  df-0 6896  df-1 6897  df-r 6899  df-lt 6902  df-pnf 7062  df-mnf 7063  df-xr 7064  df-ltxr 7065  df-le 7066  df-sub 7184  df-neg 7185  df-reap 7566  df-ap 7573  df-div 7652  df-inn 7915  df-2 7973  df-3 7974  df-4 7975  df-n0 8182  df-z 8246  df-uz 8474  df-rp 8584  df-iseq 9212  df-iexp 9255  df-rsqrt 9596
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator