![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0lt1sr | GIF version |
Description: 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) |
Ref | Expression |
---|---|
0lt1sr | ⊢ 0R <R 1R |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1pr 6892 | . . . . . 6 ⊢ 1P ∈ P | |
2 | addclpr 6875 | . . . . . 6 ⊢ ((1P ∈ P ∧ 1P ∈ P) → (1P +P 1P) ∈ P) | |
3 | 1, 1, 2 | mp2an 417 | . . . . 5 ⊢ (1P +P 1P) ∈ P |
4 | ltaddpr 6935 | . . . . 5 ⊢ (((1P +P 1P) ∈ P ∧ 1P ∈ P) → (1P +P 1P)<P ((1P +P 1P) +P 1P)) | |
5 | 3, 1, 4 | mp2an 417 | . . . 4 ⊢ (1P +P 1P)<P ((1P +P 1P) +P 1P) |
6 | addcomprg 6916 | . . . . 5 ⊢ ((1P ∈ P ∧ (1P +P 1P) ∈ P) → (1P +P (1P +P 1P)) = ((1P +P 1P) +P 1P)) | |
7 | 1, 3, 6 | mp2an 417 | . . . 4 ⊢ (1P +P (1P +P 1P)) = ((1P +P 1P) +P 1P) |
8 | 5, 7 | breqtrri 3831 | . . 3 ⊢ (1P +P 1P)<P (1P +P (1P +P 1P)) |
9 | ltsrprg 7072 | . . . 4 ⊢ (((1P ∈ P ∧ 1P ∈ P) ∧ ((1P +P 1P) ∈ P ∧ 1P ∈ P)) → ([〈1P, 1P〉] ~R <R [〈(1P +P 1P), 1P〉] ~R ↔ (1P +P 1P)<P (1P +P (1P +P 1P)))) | |
10 | 1, 1, 3, 1, 9 | mp4an 418 | . . 3 ⊢ ([〈1P, 1P〉] ~R <R [〈(1P +P 1P), 1P〉] ~R ↔ (1P +P 1P)<P (1P +P (1P +P 1P))) |
11 | 8, 10 | mpbir 144 | . 2 ⊢ [〈1P, 1P〉] ~R <R [〈(1P +P 1P), 1P〉] ~R |
12 | df-0r 7056 | . 2 ⊢ 0R = [〈1P, 1P〉] ~R | |
13 | df-1r 7057 | . 2 ⊢ 1R = [〈(1P +P 1P), 1P〉] ~R | |
14 | 11, 12, 13 | 3brtr4i 3834 | 1 ⊢ 0R <R 1R |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 = wceq 1285 ∈ wcel 1434 〈cop 3420 class class class wbr 3806 (class class class)co 5569 [cec 6198 Pcnp 6629 1Pc1p 6630 +P cpp 6631 <P cltp 6633 ~R cer 6634 0Rc0r 6636 1Rc1r 6637 <R cltr 6641 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-coll 3914 ax-sep 3917 ax-nul 3925 ax-pow 3969 ax-pr 3994 ax-un 4218 ax-setind 4310 ax-iinf 4360 |
This theorem depends on definitions: df-bi 115 df-dc 777 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-ral 2358 df-rex 2359 df-reu 2360 df-rab 2362 df-v 2613 df-sbc 2826 df-csb 2919 df-dif 2985 df-un 2987 df-in 2989 df-ss 2996 df-nul 3269 df-pw 3403 df-sn 3423 df-pr 3424 df-op 3426 df-uni 3623 df-int 3658 df-iun 3701 df-br 3807 df-opab 3861 df-mpt 3862 df-tr 3897 df-eprel 4074 df-id 4078 df-po 4081 df-iso 4082 df-iord 4151 df-on 4153 df-suc 4156 df-iom 4363 df-xp 4400 df-rel 4401 df-cnv 4402 df-co 4403 df-dm 4404 df-rn 4405 df-res 4406 df-ima 4407 df-iota 4920 df-fun 4957 df-fn 4958 df-f 4959 df-f1 4960 df-fo 4961 df-f1o 4962 df-fv 4963 df-ov 5572 df-oprab 5573 df-mpt2 5574 df-1st 5824 df-2nd 5825 df-recs 5980 df-irdg 6045 df-1o 6091 df-2o 6092 df-oadd 6095 df-omul 6096 df-er 6200 df-ec 6202 df-qs 6206 df-ni 6642 df-pli 6643 df-mi 6644 df-lti 6645 df-plpq 6682 df-mpq 6683 df-enq 6685 df-nqqs 6686 df-plqqs 6687 df-mqqs 6688 df-1nqqs 6689 df-rq 6690 df-ltnqqs 6691 df-enq0 6762 df-nq0 6763 df-0nq0 6764 df-plq0 6765 df-mq0 6766 df-inp 6804 df-i1p 6805 df-iplp 6806 df-iltp 6808 df-enr 7051 df-nr 7052 df-ltr 7055 df-0r 7056 df-1r 7057 |
This theorem is referenced by: 1ne0sr 7091 ltadd1sr 7101 caucvgsrlemcl 7113 caucvgsrlemfv 7115 ax0lt1 7190 |
Copyright terms: Public domain | W3C validator |