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

Theorem avril1 12978
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 1556 . . . . . . . 8
2 dfnul2 2901 . . . . . . . . . 10
32abeq2i 2030 . . . . . . . . 9
43con2bii 323 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 1988 . . . . . . 7
75, 6mtbii 293 . . . . . 6
87vtocleg 2397 . . . . 5
9 elex 2343 . . . . . 6
109con3i 124 . . . . 5
118, 10pm2.61i 153 . . . 4
12 df-br 3359 . . . . 5
13 0cn 7104 . . . . . . . 8
1413mulid1i 7106 . . . . . . 7
1514opeq2i 3196 . . . . . 6
1615eleq1i 1991 . . . . 5
1712, 16bitri 239 . . . 4
1811, 17mtbir 290 . . 3
1918intnan 857 . 2
20 df-i 7015 . . . . . . . 8
2120fveq1i 4673 . . . . . . 7
22 df-fv 4019 . . . . . . 7
2321, 22eqtri 1949 . . . . . 6
2423breq2i 3366 . . . . 5
25 df-r 7016 . . . . . . 7
26 sseq2 2677 . . . . . . . . 9
2726abbidv 2038 . . . . . . . 8
28 df-pw 3063 . . . . . . . 8
29 df-pw 3063 . . . . . . . 8
3027, 28, 293eqtr4g 1985 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3364 . . . . 5
3324, 32bitri 239 . . . 4
3433anbi1i 677 . . 3
3534notbii 287 . 2
3619, 35mpbir 198 1
Colors of variables: wff set class
Syntax hints:   wn 3   wa 360   wceq 1425   wcel 1427  cab 1916  cvv 2335   wss 2634  c0 2899  cpw 3061  csn 3074  cop 3077  cuni 3213   class class class wbr 3358   cxp 3989  cima 3994  cfv 4003  (class class class)co 4924  cnr 6756  c0r 6757  c1r 6758  cr 7005  cc0 7006  c1 7007  ci 7008   cmul 7011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-resscn 7060  ax-1cn 7061  ax-icn 7062  ax-addcl 7063  ax-mulcl 7065  ax-mulcom 7067  ax-mulass 7069  ax-distr 7070  ax-i2m1 7071  ax-1rid 7073  ax-cnre 7076
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-clab 1917  df-cleq 1922  df-clel 1925  df-ral 2142  df-rex 2143  df-v 2337  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-nul 2900  df-pw 3063  df-sn 3080  df-pr 3081  df-op 3083  df-uni 3214  df-br 3359  df-opab 3413  df-xp 4005  df-cnv 4007  df-dm 4009  df-rn 4010  df-res 4011  df-ima 4012  df-fv 4019  df-ov 4926  df-i 7015  df-r 7016
Copyright terms: Public domain