MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  avril1 Unicode version

Theorem avril1 21710
Description: Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle of quidquid german dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object  x equals itself (proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we demonstrate that the power set of the real numbers, as a relation on the value of the imaginary unit, does not conjoin with an empty relation on the product of the additive and multiplicative identity elements, leading to this startling conclusion that has left even seasoned professional mathematicians scratching their heads. (Contributed by Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.) (New usage is discouraged.)

A reply to skeptics can be found at http://us.metamath.org/mpeuni/mmnotes.txt, under the 1-Apr-2006 entry.

Assertion
Ref Expression
avril1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )

Proof of Theorem avril1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 equid 1684 . . . . . . . 8  |-  x  =  x
2 dfnul2 3590 . . . . . . . . . 10  |-  (/)  =  {
x  |  -.  x  =  x }
32abeq2i 2511 . . . . . . . . 9  |-  ( x  e.  (/)  <->  -.  x  =  x )
43con2bii 323 . . . . . . . 8  |-  ( x  =  x  <->  -.  x  e.  (/) )
51, 4mpbi 200 . . . . . . 7  |-  -.  x  e.  (/)
6 eleq1 2464 . . . . . . 7  |-  ( x  =  <. F ,  0
>.  ->  ( x  e.  (/) 
<-> 
<. F ,  0 >.  e.  (/) ) )
75, 6mtbii 294 . . . . . 6  |-  ( x  =  <. F ,  0
>.  ->  -.  <. F , 
0 >.  e.  (/) )
87vtocleg 2982 . . . . 5  |-  ( <. F ,  0 >.  e. 
_V  ->  -.  <. F , 
0 >.  e.  (/) )
9 elex 2924 . . . . . 6  |-  ( <. F ,  0 >.  e.  (/)  ->  <. F ,  0
>.  e.  _V )
109con3i 129 . . . . 5  |-  ( -. 
<. F ,  0 >.  e.  _V  ->  -.  <. F , 
0 >.  e.  (/) )
118, 10pm2.61i 158 . . . 4  |-  -.  <. F ,  0 >.  e.  (/)
12 df-br 4173 . . . . 5  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
( 0  x.  1 ) >.  e.  (/) )
13 0cn 9040 . . . . . . . 8  |-  0  e.  CC
1413mulid1i 9048 . . . . . . 7  |-  ( 0  x.  1 )  =  0
1514opeq2i 3948 . . . . . 6  |-  <. F , 
( 0  x.  1 ) >.  =  <. F ,  0 >.
1615eleq1i 2467 . . . . 5  |-  ( <. F ,  ( 0  x.  1 ) >.  e.  (/)  <->  <. F ,  0
>.  e.  (/) )
1712, 16bitri 241 . . . 4  |-  ( F
(/) ( 0  x.  1 )  <->  <. F , 
0 >.  e.  (/) )
1811, 17mtbir 291 . . 3  |-  -.  F (/) ( 0  x.  1 )
1918intnan 881 . 2  |-  -.  ( A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y
)  /\  F (/) ( 0  x.  1 ) )
20 df-i 8955 . . . . . . . 8  |-  _i  =  <. 0R ,  1R >.
2120fveq1i 5688 . . . . . . 7  |-  ( _i
`  1 )  =  ( <. 0R ,  1R >. `  1 )
22 df-fv 5421 . . . . . . 7  |-  ( <. 0R ,  1R >. `  1
)  =  ( iota y 1 <. 0R ,  1R >. y )
2321, 22eqtri 2424 . . . . . 6  |-  ( _i
`  1 )  =  ( iota y 1
<. 0R ,  1R >. y )
2423breq2i 4180 . . . . 5  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P RR ( iota y 1
<. 0R ,  1R >. y ) )
25 df-r 8956 . . . . . . 7  |-  RR  =  ( R.  X.  { 0R } )
26 sseq2 3330 . . . . . . . . 9  |-  ( RR  =  ( R.  X.  { 0R } )  -> 
( z  C_  RR  <->  z 
C_  ( R.  X.  { 0R } ) ) )
2726abbidv 2518 . . . . . . . 8  |-  ( RR  =  ( R.  X.  { 0R } )  ->  { z  |  z 
C_  RR }  =  { z  |  z 
C_  ( R.  X.  { 0R } ) } )
28 df-pw 3761 . . . . . . . 8  |-  ~P RR  =  { z  |  z 
C_  RR }
29 df-pw 3761 . . . . . . . 8  |-  ~P ( R.  X.  { 0R }
)  =  { z  |  z  C_  ( R.  X.  { 0R }
) }
3027, 28, 293eqtr4g 2461 . . . . . . 7  |-  ( RR  =  ( R.  X.  { 0R } )  ->  ~P RR  =  ~P ( R.  X.  { 0R }
) )
3125, 30ax-mp 8 . . . . . 6  |-  ~P RR  =  ~P ( R.  X.  { 0R } )
3231breqi 4178 . . . . 5  |-  ( A ~P RR ( iota y 1 <. 0R ,  1R >. y )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3324, 32bitri 241 . . . 4  |-  ( A ~P RR ( _i
`  1 )  <->  A ~P ( R.  X.  { 0R } ) ( iota y 1 <. 0R ,  1R >. y ) )
3433anbi1i 677 . . 3  |-  ( ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <-> 
( A ~P ( R.  X.  { 0R }
) ( iota y
1 <. 0R ,  1R >. y )  /\  F (/) ( 0  x.  1 ) ) )
3534notbii 288 . 2  |-  ( -.  ( A ~P RR ( _i `  1 )  /\  F (/) ( 0  x.  1 ) )  <->  -.  ( A ~P ( R.  X.  { 0R }
) ( iota y
1 <. 0R ,  1R >. y )  /\  F (/) ( 0  x.  1 ) ) )
3619, 35mpbir 201 1  |-  -.  ( A ~P RR ( _i
`  1 )  /\  F (/) ( 0  x.  1 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359    = wceq 1649    e. wcel 1721   {cab 2390   _Vcvv 2916    C_ wss 3280   (/)c0 3588   ~Pcpw 3759   {csn 3774   <.cop 3777   class class class wbr 4172    X. cxp 4835   iotacio 5375   ` cfv 5413  (class class class)co 6040   R.cnr 8698   0Rc0r 8699   1Rc1r 8700   RRcr 8945   0cc0 8946   1c1 8947   _ici 8948    x. cmul 8951
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulcom 9010  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1rid 9016  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-i 8955  df-r 8956
  Copyright terms: Public domain W3C validator