HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem avril1 16171
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 germanus dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object 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.)

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

Assertion
Ref Expression
avril1

Proof of Theorem avril1
StepHypRef Expression
1 equid 1697 . . . . . . . 8
2 dfnul2 3087 . . . . . . . . . 10
32abeq2i 2191 . . . . . . . . 9
43con2bii 321 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 2149 . . . . . . 7
75, 6mtbii 291 . . . . . 6
87vtocleg 2562 . . . . 5
9 elex 2508 . . . . . 6
109con3i 125 . . . . 5
118, 10pm2.61i 154 . . . 4
12 df-br 3592 . . . . 5
13 0cn 8164 . . . . . . . 8
1413mulid1i 8166 . . . . . . 7
1514opeq2i 3412 . . . . . 6
1615eleq1i 2152 . . . . 5
1712, 16bitri 238 . . . 4
1811, 17mtbir 288 . . 3
1918intnan 840 . 2
20 df-i 8070 . . . . . . . 8
2120fveq1i 4993 . . . . . . 7
22 df-fv 4277 . . . . . . 7
2321, 22eqtri 2110 . . . . . 6
2423breq2i 3599 . . . . 5
25 df-r 8071 . . . . . . 7
26 sseq2 2853 . . . . . . . . 9
2726abbidv 2198 . . . . . . . 8
28 df-pw 3256 . . . . . . . 8
29 df-pw 3256 . . . . . . . 8
3027, 28, 293eqtr4g 2146 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3597 . . . . 5
3324, 32bitri 238 . . . 4
3433anbi1i 672 . . 3
3534notbii 285 . 2
3619, 35mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wa 357   wceq 1531   wcel 1533  cab 2077  cvv 2500   wss 2810  c0 3085  cpw 3254  csn 3268  cop 3271  cuni 3434   class class class wbr 3591   cxp 4247  cima 4252  cfv 4261  (class class class)co 5296  cnr 7813  c0r 7814  c1r 7815  cr 8060  cc0 8061  c1 8062  ci 8063   cmul 8066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-resscn 8117  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-mulcl 8122  ax-mulcom 8124  ax-mulass 8126  ax-distr 8127  ax-i2m1 8128  ax-1rid 8130  ax-cnre 8133
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-xp 4263  df-cnv 4265  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fv 4277  df-ov 5298  df-i 8070  df-r 8071
Copyright terms: Public domain