Theorem leltt 4278

Description: 'Less than or equal to' expressed in terms of 'less than'.

Assertion

Ref	Expression
leltt	⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ ¬ B < A))

Proof of Theorem leltt

Step	Hyp	Ref	Expression
1		opelxpi 2455	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ⟨A, B⟩ ∈ (ℝ × ℝ))
2		df-le 4277	. . . . . . 7 ⊢ ≤ = ((ℝ × ℝ) ∖ ◡ < )
3	2	eleq2i 1153	. . . . . 6 ⊢ (⟨A, B⟩ ∈ ≤ ↔ ⟨A, B⟩ ∈ ((ℝ × ℝ) ∖ ◡ < ))
4		eldif 1496	. . . . . 6 ⊢ (⟨A, B⟩ ∈ ((ℝ × ℝ) ∖ ◡ < ) ↔ (⟨A, B⟩ ∈ (ℝ × ℝ) ∧ ¬ ⟨A, B⟩ ∈ ◡ < ))
5	3, 4	bitr 151	. . . . 5 ⊢ (⟨A, B⟩ ∈ ≤ ↔ (⟨A, B⟩ ∈ (ℝ × ℝ) ∧ ¬ ⟨A, B⟩ ∈ ◡ < ))
6	5	baib 506	. . . 4 ⊢ (⟨A, B⟩ ∈ (ℝ × ℝ) → (⟨A, B⟩ ∈ ≤ ↔ ¬ ⟨A, B⟩ ∈ ◡ < ))
7	1, 6	syl 12	. . 3 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (⟨A, B⟩ ∈ ≤ ↔ ¬ ⟨A, B⟩ ∈ ◡ < ))
8		df-br 2063	. . 3 ⊢ (A ≤ B ↔ ⟨A, B⟩ ∈ ≤ )
9	7, 8	syl5bb 410	. 2 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ ¬ ⟨A, B⟩ ∈ ◡ < ))
10		opelcnvg 2517	. . . 4 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (⟨A, B⟩ ∈ ◡ < ↔ ⟨B, A⟩ ∈ < ))
11		df-br 2063	. . . 4 ⊢ (B < A ↔ ⟨B, A⟩ ∈ < )
12	10, 11	syl6rbbr 417	. . 3 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (B < A ↔ ⟨A, B⟩ ∈ ◡ < ))
13	12	negbid 463	. 2 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (¬ B < A ↔ ¬ ⟨A, B⟩ ∈ ◡ < ))
14	9, 13	bitr4d 409	1 ⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → (A ≤ B ↔ ¬ B < A))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196   ∈ wcel 1092   ∖ cdif 1484  ⟨cop 1810   class class class wbr 2054   × cxp 2408  ^◡ccnv 2409  ℝcr 4027   < clt 4033   ≤ cle 4092

This theorem is referenced by:  letri3t 4283  leloet 4284  lenltt 4285  lelt 4301  ltaddsubt 4357  ledivt 4405  nnge1t 4439  lt1nnn 4442  nnleltp1t 4448  suprub 4513  nn0ge0t 4550  nn0ltp1let 4556  elnnz1 4581  zltp1let 4597  uzwo 4605  nnwoOLD 4608  indstr 4611  zbtwnre 4619  sqr0 4730  znnenlem 4929  znnen 4930  projlem13 5205

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-le 4277

metamath.org