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

Theorem avril1 12757
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 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.)

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 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))

Proof of Theorem avril1
StepHypRef Expression
1 equid 1580 . . . . . . . 8 |- x = x
2 dfnul2 2923 . . . . . . . . . 10 |- (/) = {x | -. x = x}
32abeq2i 2054 . . . . . . . . 9 |- (x e. (/) <-> -. x = x)
43con2bii 337 . . . . . . . 8 |- (x = x <-> -. x e. (/))
51, 4mpbi 212 . . . . . . 7 |- -. x e. (/)
6 eleq1 2012 . . . . . . 7 |- (x = <.F, 0>. -> (x e. (/) <-> <.F, 0>. e. (/)))
75, 6mtbii 310 . . . . . 6 |- (x = <.F, 0>. -> -. <.F, 0>. e. (/))
87vtocleg 2420 . . . . 5 |- (<.F, 0>. e. _V -> -. <.F, 0>. e. (/))
9 elex 2366 . . . . . 6 |- (<.F, 0>. e. (/) -> <.F, 0>. e. _V)
109con3i 124 . . . . 5 |- (-. <.F, 0>. e. _V -> -. <.F, 0>. e. (/))
118, 10pm2.61i 153 . . . 4 |- -. <.F, 0>. e. (/)
12 df-br 3374 . . . . 5 |- (F(/)(0 x. 1) <-> <.F, (0 x. 1)>. e. (/))
13 0cn 7096 . . . . . . . 8 |- 0 e. CC
1413mulid1i 7098 . . . . . . 7 |- (0 x. 1) = 0
1514opeq2i 3211 . . . . . 6 |- <.F, (0 x. 1)>. = <.F, 0>.
1615eleq1i 2015 . . . . 5 |- (<.F, (0 x. 1)>. e. (/) <-> <.F, 0>. e. (/))
1712, 16bitri 254 . . . 4 |- (F(/)(0 x. 1) <-> <.F, 0>. e. (/))
1811, 17mtbir 307 . . 3 |- -. F(/)(0 x. 1)
1918intnan 881 . 2 |- -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1))
20 df-i 7007 . . . . . . . 8 |- _i = <.0R, 1R>.
2120fveq1i 4682 . . . . . . 7 |- (_i` 1) = (<.0R, 1R>.` 1)
22 df-fv 4032 . . . . . . 7 |- (<.0R, 1R>.` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2321, 22eqtri 1973 . . . . . 6 |- (_i` 1) = U.{y | (<.0R, 1R>."{1}) = {y}}
2423breq2i 3381 . . . . 5 |- (A~PRR(_i` 1) <-> A~PRRU.{y | (<.0R, 1R>."{1}) = {y}})
25 df-r 7008 . . . . . . 7 |- RR = (R. X. {0R})
26 sseq2 2700 . . . . . . . . 9 |- (RR = (R. X. {0R}) -> (z C_ RR <-> z C_ (R. X. {0R})))
2726abbidv 2062 . . . . . . . 8 |- (RR = (R. X. {0R}) -> {z | z C_ RR} = {z | z C_ (R. X. {0R})})
28 df-pw 3081 . . . . . . . 8 |- ~PRR = {z | z C_ RR}
29 df-pw 3081 . . . . . . . 8 |- ~P(R. X. {0R}) = {z | z C_ (R. X. {0R})}
3027, 28, 293eqtr4g 2009 . . . . . . 7 |- (RR = (R. X. {0R}) -> ~PRR = ~P(R. X. {0R}))
3125, 30ax-mp 8 . . . . . 6 |- ~PRR = ~P(R. X. {0R})
3231breqi 3379 . . . . 5 |- (A~PRRU.{y | (<.0R, 1R>."{1}) = {y}} <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3324, 32bitri 254 . . . 4 |- (A~PRR(_i` 1) <-> A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}})
3433anbi1i 695 . . 3 |- ((A~PRR(_i` 1) /\ F(/)(0 x. 1)) <-> (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
3534notbii 304 . 2 |- (-. (A~PRR(_i` 1) /\ F(/)(0 x. 1)) <-> -. (A~P(R. X. {0R})U.{y | (<.0R, 1R>."{1}) = {y}} /\ F(/)(0 x. 1)))
3619, 35mpbir 213 1 |- -. (A~PRR(_i` 1) /\ F(/)(0 x. 1))
Colors of variables: wff set class
Syntax hints:  -. wn 3   /\ wa 377   = wceq 1449   e. wcel 1451  {cab 1940  _Vcvv 2358   C_ wss 2657  (/)c0 2921  ~Pcpw 3079  {csn 3092  <.cop 3094  U.cuni 3228   class class class wbr 3373   X. cxp 4002  "cima 4007  ` cfv 4016  (class class class)co 4931  R.cnr 6748  0Rc0r 6749  1Rc1r 6750  RRcr 6997  0cc0 6998  1c1 6999  _ici 7000   x. cmul 7003
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-resscn 7052  ax-1cn 7053  ax-icn 7054  ax-addcl 7055  ax-mulcl 7057  ax-mulcom 7059  ax-mulass 7061  ax-distr 7062  ax-i2m1 7063  ax-1rid 7065  ax-cnre 7068
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3an 939  df-ex 1372  df-sb 1626  df-clab 1941  df-cleq 1946  df-clel 1949  df-ral 2166  df-rex 2167  df-v 2360  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-nul 2922  df-pw 3081  df-sn 3096  df-pr 3097  df-op 3100  df-uni 3229  df-br 3374  df-opab 3428  df-xp 4018  df-cnv 4020  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fv 4032  df-ov 4933  df-i 7007  df-r 7008
Copyright terms: Public domain