Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > xaddval | Unicode version |
Description: Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
xaddval |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0xr 7939 | . . . . . 6 | |
2 | 1 | a1i 9 | . . . . 5 |
3 | pnfxr 7945 | . . . . . 6 | |
4 | 3 | a1i 9 | . . . . 5 |
5 | xrmnfdc 9773 | . . . . . 6 DECID | |
6 | 5 | adantl 275 | . . . . 5 DECID |
7 | 2, 4, 6 | ifcldcd 3553 | . . . 4 |
8 | 7 | adantr 274 | . . 3 |
9 | mnfxr 7949 | . . . . . . 7 | |
10 | 9 | a1i 9 | . . . . . 6 |
11 | xrpnfdc 9772 | . . . . . . 7 DECID | |
12 | 11 | adantl 275 | . . . . . 6 DECID |
13 | 2, 10, 12 | ifcldcd 3553 | . . . . 5 |
14 | 13 | ad2antrr 480 | . . . 4 |
15 | 3 | a1i 9 | . . . . 5 |
16 | 9 | a1i 9 | . . . . . 6 |
17 | simp-4r 532 | . . . . . . . . 9 | |
18 | simpl 108 | . . . . . . . . . . 11 | |
19 | 18 | ad4antr 486 | . . . . . . . . . 10 |
20 | simpllr 524 | . . . . . . . . . . 11 | |
21 | 20 | neqned 2341 | . . . . . . . . . 10 |
22 | xrnemnf 9707 | . . . . . . . . . . 11 | |
23 | 22 | biimpi 119 | . . . . . . . . . 10 |
24 | 19, 21, 23 | syl2anc 409 | . . . . . . . . 9 |
25 | 17, 24 | ecased 1338 | . . . . . . . 8 |
26 | simplr 520 | . . . . . . . . 9 | |
27 | simpr 109 | . . . . . . . . . . 11 | |
28 | 27 | ad4antr 486 | . . . . . . . . . 10 |
29 | simpr 109 | . . . . . . . . . . 11 | |
30 | 29 | neqned 2341 | . . . . . . . . . 10 |
31 | xrnemnf 9707 | . . . . . . . . . . 11 | |
32 | 31 | biimpi 119 | . . . . . . . . . 10 |
33 | 28, 30, 32 | syl2anc 409 | . . . . . . . . 9 |
34 | 26, 33 | ecased 1338 | . . . . . . . 8 |
35 | 25, 34 | readdcld 7922 | . . . . . . 7 |
36 | 35 | rexrd 7942 | . . . . . 6 |
37 | 6 | ad3antrrr 484 | . . . . . 6 DECID |
38 | 16, 36, 37 | ifcldadc 3547 | . . . . 5 |
39 | 12 | ad2antrr 480 | . . . . 5 DECID |
40 | 15, 38, 39 | ifcldadc 3547 | . . . 4 |
41 | xrmnfdc 9773 | . . . . 5 DECID | |
42 | 41 | ad2antrr 480 | . . . 4 DECID |
43 | 14, 40, 42 | ifcldadc 3547 | . . 3 |
44 | xrpnfdc 9772 | . . . 4 DECID | |
45 | 44 | adantr 274 | . . 3 DECID |
46 | 8, 43, 45 | ifcldadc 3547 | . 2 |
47 | simpl 108 | . . . . 5 | |
48 | 47 | eqeq1d 2173 | . . . 4 |
49 | simpr 109 | . . . . . 6 | |
50 | 49 | eqeq1d 2173 | . . . . 5 |
51 | 50 | ifbid 3539 | . . . 4 |
52 | 47 | eqeq1d 2173 | . . . . 5 |
53 | 49 | eqeq1d 2173 | . . . . . 6 |
54 | 53 | ifbid 3539 | . . . . 5 |
55 | oveq12 5848 | . . . . . . 7 | |
56 | 50, 55 | ifbieq2d 3542 | . . . . . 6 |
57 | 53, 56 | ifbieq2d 3542 | . . . . 5 |
58 | 52, 54, 57 | ifbieq12d 3544 | . . . 4 |
59 | 48, 51, 58 | ifbieq12d 3544 | . . 3 |
60 | df-xadd 9703 | . . 3 | |
61 | 59, 60 | ovmpoga 5965 | . 2 |
62 | 46, 61 | mpd3an3 1327 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wo 698 DECID wdc 824 wceq 1342 wcel 2135 wne 2334 cif 3518 (class class class)co 5839 cr 7746 cc0 7747 caddc 7750 cpnf 7924 cmnf 7925 cxr 7926 cxad 9700 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-13 2137 ax-14 2138 ax-ext 2146 ax-sep 4097 ax-pow 4150 ax-pr 4184 ax-un 4408 ax-setind 4511 ax-cnex 7838 ax-resscn 7839 ax-1re 7841 ax-addrcl 7844 ax-rnegex 7856 |
This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 968 df-3an 969 df-tru 1345 df-fal 1348 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ne 2335 df-nel 2430 df-ral 2447 df-rex 2448 df-rab 2451 df-v 2726 df-sbc 2950 df-dif 3116 df-un 3118 df-in 3120 df-ss 3127 df-if 3519 df-pw 3558 df-sn 3579 df-pr 3580 df-op 3582 df-uni 3787 df-br 3980 df-opab 4041 df-id 4268 df-xp 4607 df-rel 4608 df-cnv 4609 df-co 4610 df-dm 4611 df-iota 5150 df-fun 5187 df-fv 5193 df-ov 5842 df-oprab 5843 df-mpo 5844 df-pnf 7929 df-mnf 7930 df-xr 7931 df-xadd 9703 |
This theorem is referenced by: xaddpnf1 9776 xaddpnf2 9777 xaddmnf1 9778 xaddmnf2 9779 pnfaddmnf 9780 mnfaddpnf 9781 rexadd 9782 |
Copyright terms: Public domain | W3C validator |