Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > apadd1 | Unicode version | ||
| Description: Addition respects apartness. Analogue of addcan 8499 for apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) |
| Ref | Expression |
|---|---|
| apadd1 |
     ![/\](wedge.gif "/\"){kind=small} 
   #
  #
|
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnre 8315 |
. . 3
     | |
| 2 | 1 | 3ad2ant3 1051 |
. 2
|
| 3 | cnre 8315 |
. . . . . . 7
| |
| 4 | 3 | 3ad2ant2 1050 |
. . . . . 6
|
| 5 | 4 | ad2antrr 492 |
. . . . 5
|
| 6 | cnre 8315 |
. . . . . . . . . . 11
| |
| 7 | 6 | 3ad2ant1 1049 |
. . . . . . . . . 10
|
| 8 | 7 | ad2antrr 492 |
. . . . . . . . 9
|
| 9 | 8 | ad2antrr 492 |
. . . . . . . 8
|
| 10 | simplrl 541 |
. . . . . . . . . . . 12
| |
| 11 | simplrr 542 |
. . . . . . . . . . . 12
| |
| 12 | simprl 535 |
. . . . . . . . . . . . 13
| |
| 13 | 12 | ad3antrrr 496 |
. . . . . . . . . . . 12
|
| 14 | simprr 537 |
. . . . . . . . . . . . 13
| |
| 15 | 14 | ad3antrrr 496 |
. . . . . . . . . . . 12
|
| 16 | apreim 8924 |
. . . . . . . . . . . 12
#
# 
# | |
| 17 | 10, 11, 13, 15, 16 | syl22anc 1279 |
. . . . . . . . . . 11
#
#
# |
| 18 | simpr 110 |
. . . . . . . . . . . 12
| |
| 19 | simpllr 540 |
. . . . . . . . . . . 12
| |
| 20 | 18, 19 | breq12d 4141 |
. . . . . . . . . . 11
#
# |
| 21 | simprl 535 |
. . . . . . . . . . . . . . . 16
| |
| 22 | 21 | ad2antrr 492 |
. . . . . . . . . . . . . . 15
|
| 23 | 22 | ad3antrrr 496 |
. . . . . . . . . . . . . 14
|
| 24 | 10, 23 | readdcld 8348 |
. . . . . . . . . . . . 13
|
| 25 | simprr 537 |
. . . . . . . . . . . . . . . 16
| |
| 26 | 25 | ad2antrr 492 |
. . . . . . . . . . . . . . 15
|
| 27 | 26 | ad3antrrr 496 |
. . . . . . . . . . . . . 14
|
| 28 | 11, 27 | readdcld 8348 |
. . . . . . . . . . . . 13
|
| 29 | 13, 23 | readdcld 8348 |
. . . . . . . . . . . . 13
|
| 30 | 15, 27 | readdcld 8348 |
. . . . . . . . . . . . 13
|
| 31 | apreim 8924 |
. . . . . . . . . . . . 13
#
# # | |
| 32 | 24, 28, 29, 30, 31 | syl22anc 1279 |
. . . . . . . . . . . 12
#
# # |
| 33 | 10 | recnd 8347 |
. . . . . . . . . . . . . . 15
|
| 34 | ax-icn 8267 |
. . . . . . . . . . . . . . . . 17
| |
| 35 | 34 | a1i 9 |
. . . . . . . . . . . . . . . 16
|
| 36 | 11 | recnd 8347 |
. . . . . . . . . . . . . . . 16
|
| 37 | 35, 36 | mulcld 8339 |
. . . . . . . . . . . . . . 15
|
| 38 | 23 | recnd 8347 |
. . . . . . . . . . . . . . 15
|
| 39 | 27 | recnd 8347 |
. . . . . . . . . . . . . . . 16
|
| 40 | 35, 39 | mulcld 8339 |
. . . . . . . . . . . . . . 15
|
| 41 | 33, 37, 38, 40 | add4d 8488 |
. . . . . . . . . . . . . 14
|
| 42 | simplr 533 |
. . . . . . . . . . . . . . . 16
| |
| 43 | 42 | ad3antrrr 496 |
. . . . . . . . . . . . . . 15
|
| 44 | 18, 43 | oveq12d 6096 |
. . . . . . . . . . . . . 14
|
| 45 | 35, 36, 39 | adddid 8343 |
. . . . . . . . . . . . . . 15
|
| 46 | 45 | oveq2d 6094 |
. . . . . . . . . . . . . 14
|
| 47 | 41, 44, 46 | 3eqtr4d 2281 |
. . . . . . . . . . . . 13
|
| 48 | 13 | recnd 8347 |
. . . . . . . . . . . . . . 15
|
| 49 | 15 | recnd 8347 |
. . . . . . . . . . . . . . . 16
|
| 50 | 35, 49 | mulcld 8339 |
. . . . . . . . . . . . . . 15
|
| 51 | 48, 50, 38, 40 | add4d 8488 |
. . . . . . . . . . . . . 14
|
| 52 | 19, 43 | oveq12d 6096 |
. . . . . . . . . . . . . 14
|
| 53 | 35, 49, 39 | adddid 8343 |
. . . . . . . . . . . . . . 15
|
| 54 | 53 | oveq2d 6094 |
. . . . . . . . . . . . . 14
|
| 55 | 51, 52, 54 | 3eqtr4d 2281 |
. . . . . . . . . . . . 13
|
| 56 | 47, 55 | breq12d 4141 |
. . . . . . . . . . . 12
#
# |
| 57 | reapadd1 8917 |
. . . . . . . . . . . . . 14
#
# | |
| 58 | 10, 13, 23, 57 | syl3anc 1278 |
. . . . . . . . . . . . 13
#
# |
| 59 | reapadd1 8917 |
. . . . . . . . . . . . . 14
#
# | |
| 60 | 11, 15, 27, 59 | syl3anc 1278 |
. . . . . . . . . . . . 13
#
# |
| 61 | 58, 60 | orbi12d 805 |
. . . . . . . . . . . 12
# #
# # |
| 62 | 32, 56, 61 | 3bitr4d 220 |
. . . . . . . . . . 11
#
#
# |
| 63 | 17, 20, 62 | 3bitr4d 220 |
. . . . . . . . . 10
#
#
|
| 64 | 63 | ex 115 |
. . . . . . . . 9
#
#
|
| 65 | 64 | rexlimdvva 2676 |
. . . . . . . 8
#
#
|
| 66 | 9, 65 | mpd 13 |
. . . . . . 7
#
#
|
| 67 | 66 | ex 115 |
. . . . . 6
#
#
|
| 68 | 67 | rexlimdvva 2676 |
. . . . 5
#
#
|
| 69 | 5, 68 | mpd 13 |
. . . 4
#
#
|
| 70 | 69 | ex 115 |
. . 3
#
#
|
| 71 | 70 | rexlimdvva 2676 |
. 2
#
#
|
| 72 | 2, 71 | mpd 13 |
1
#
#
|
| Colors of variables: wff set class |
| Syntax hints: wi 4
wa 104
wb 105 wo 720 w3a 1009 wceq 1402 wcel 2209 wrex 2529 class class class wbr 4128
(class class class)co 6078 cc 8170 cr 8171 ci 8174 caddc 8175 cmul 8177 # cap 8902 |
| 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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4247 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-setind 4682 ax-cnex 8263 ax-resscn 8264 ax-1cn 8265 ax-1re 8266 ax-icn 8267 ax-addcl 8268 ax-addrcl 8269 ax-mulcl 8270 ax-mulrcl 8271 ax-addcom 8272 ax-mulcom 8273 ax-addass 8274 ax-mulass 8275 ax-distr 8276 ax-i2m1 8277 ax-0lt1 8278 ax-1rid 8279 ax-0id 8280 ax-rnegex 8281 ax-precex 8282 ax-cnre 8283 ax-pre-ltirr 8284 ax-pre-lttrn 8286 ax-pre-apti 8287 ax-pre-ltadd 8288 ax-pre-mulgt0 8289 |
| This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-br 4129 df-opab 4191 df-id 4436 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-iota 5335 df-fun 5377 df-fv 5383 df-riota 6031 df-ov 6081 df-oprab 6082 df-mpo 6083 df-pnf 8355 df-mnf 8356 df-ltxr 8358 df-sub 8492 df-neg 8493 df-reap 8896 df-ap 8903 |
| This theorem is referenced by: apadd2 8930 addext 8931 apsub1 8963 subap0 8964 |
| Copyright terms: Public domain | W3C validator |