Theorem lenltd 8074

Description: 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
lenltd	⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem lenltd

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		lenlt 8032	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∈ wcel 2148   class class class wbr 4003  ℝcr 7809   < clt 7991   ≤ cle 7992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-xr 7995  df-le 7997

This theorem is referenced by:  ltnsymd  8076  nltled  8077  lensymd  8078  leadd1  8386  lemul1  8549  leltap  8581  ap0gt0  8596  prodgt0  8808  prodge0  8810  lediv1  8825  lemuldiv  8837  lerec  8840  lt2msq  8842  le2msq  8857  squeeze0  8860  suprleubex  8910  0mnnnnn0  9207  elnn0z  9265  uzm1  9557  infregelbex  9597  fztri3or  10038  fzdisj  10051  uzdisj  10092  nn0disj  10137  fzouzdisj  10179  elfzonelfzo  10229  flqeqceilz  10317  modifeq2int  10385  modsumfzodifsn  10395  nn0leexp2  10689  expcanlem  10694  fimaxq  10806  resqrexlemoverl  11029  leabs  11082  absle  11097  maxleast  11221  minmax  11237  climge0  11332  pcfac  12347  cxple  14307