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

Theorem avril1 13772
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 1545 . . . . . . . 8
2 dfnul2 2904 . . . . . . . . . 10
32abeq2i 2019 . . . . . . . . 9
43con2bii 321 . . . . . . . 8
51, 4mpbi 197 . . . . . . 7
6 eleq1 1977 . . . . . . 7
75, 6mtbii 291 . . . . . 6
87vtocleg 2386 . . . . 5
9 elex 2332 . . . . . 6
109con3i 125 . . . . 5
118, 10pm2.61i 154 . . . 4
12 df-br 3371 . . . . 5
13 0cn 7268 . . . . . . . 8
1413mulid1i 7270 . . . . . . 7
1514opeq2i 3205 . . . . . 6
1615eleq1i 1980 . . . . 5
1712, 16bitri 238 . . . 4
1811, 17mtbir 288 . . 3
1918intnan 840 . 2
20 df-i 7179 . . . . . . . 8
2120fveq1i 4718 . . . . . . 7
22 df-fv 4035 . . . . . . 7
2321, 22eqtri 1938 . . . . . 6
2423breq2i 3378 . . . . 5
25 df-r 7180 . . . . . . 7
26 sseq2 2677 . . . . . . . . 9
2726abbidv 2026 . . . . . . . 8
28 df-pw 3068 . . . . . . . 8
29 df-pw 3068 . . . . . . . 8
3027, 28, 293eqtr4g 1974 . . . . . . 7
3125, 30ax-mp 8 . . . . . 6
3231breqi 3376 . . . . 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 1414   wcel 1416  cab 1905  cvv 2324   wss 2634  c0 2902  cpw 3066  csn 3079  cop 3082  cuni 3223   class class class wbr 3370   cxp 4005  cima 4010  cfv 4019  (class class class)co 4979  cnr 6920  c0r 6921  c1r 6922  cr 7169  cc0 7170  c1 7171  ci 7172   cmul 7175
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-resscn 7224  ax-1cn 7225  ax-icn 7226  ax-addcl 7227  ax-mulcl 7229  ax-mulcom 7231  ax-mulass 7233  ax-distr 7234  ax-i2m1 7235  ax-1rid 7237  ax-cnre 7240
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-clab 1906  df-cleq 1911  df-clel 1914  df-ral 2131  df-rex 2132  df-v 2326  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-nul 2903  df-pw 3068  df-sn 3085  df-pr 3086  df-op 3088  df-uni 3224  df-br 3371  df-opab 3425  df-xp 4021  df-cnv 4023  df-dm 4025  df-rn 4026  df-res 4027  df-ima 4028  df-fv 4035  df-ov 4981  df-i 7179  df-r 7180
Copyright terms: Public domain