Theorem letri3 10123

Description: Trichotomy law. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
letri3	|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )

Proof of Theorem letri3

Step	Hyp	Ref	Expression
1		lttri3 10121	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
2		ancom 466	. . 3 |- ( ( -. B < A /\ -. A < B ) <-> ( -. A < B /\ -. B < A ) )
3	1, 2	syl6bbr 278	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. B < A /\ -. A < B ) ) )
4		lenlt 10116	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
5		lenlt 10116	. . . 4 |- ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> -. A < B ) )
6	5	ancoms 469	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( B <_ A <-> -. A < B ) )
7	4, 6	anbi12d 747	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B <_ A ) <-> ( -. B < A /\ -. A < B ) ) )
8	3, 7	bitr4d 271	1 |- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  eqlelt  10125  eqlei  10147  eqlei2  10148  letri3i  10153  letri3d  10179  lesub0  10545  eqord1  10556  lbreu  10973  nnle1eq1  11048  nn0le0eq0  11321  zextle  11450  uz11  11710  uzin  11720  uzwo  11751  qsqueeze  12032  elfz1eq  12352  faclbnd4lem4  13083  swrdccat3blem  13495  repswswrd  13531  sqeqd  13906  max0add  14050  fsum00  14530  reef11  14849  dvdsabseq  15035  nn0seqcvgd  15283  infpnlem1  15614  psrbaglesupp  19368  gzrngunit  19812  nmoeq0  22540  oprpiece1res2  22751  pcoval2  22816  minveclem7  23206  pjthlem1  23208  iblposlem  23558  dvferm  23751  dveq0  23763  dv11cn  23764  fta1blem  23928  dgrco  24031  aalioulem3  24089  logf1o2  24396  cxpsqrtlem  24448  ang180lem3  24541  chpeq0  24933  chteq0  24934  lgsdir  25057  lgsabs1  25061  minvecolem7  27739  pjhthlem1  28250  pjnormssi  29027  hstles  29090  stge1i  29097  stle0i  29098  stlesi  29100  cdj3lem1  29293  derangen  31154  bfplem2  33622  bfp  33623  acongeq  37550  jm2.26lem3  37568  dvconstbi  38533  zgeltp1eq  41318  zgtp1leeq  42311