|
|
| 21 行: |
21 行: |
| | hoe | | hoe |
| | hoe | | hoe |
| - | </nowiki>
| |
| - |
| |
| - | <nowiki>
| |
| - | environ
| |
| - |
| |
| - | vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
| |
| - | RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
| |
| - | TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
| |
| - | UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
| |
| - | notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
| |
| - | XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
| |
| - | FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
| |
| - | TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
| |
| - | constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
| |
| - | BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1;
| |
| - | registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
| |
| - | XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
| |
| - | XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
| |
| - | XREAL_0, RVSUM_1;
| |
| - | requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
| |
| - | definitions TARSKI, XBOOLE_0, INT_2, NAT_D, FINSEQ_1, VALUED_0,
| |
| - | PRE_POLY,FINSET_1,CARD_1;
| |
| - | theorems ORDINAL1, NEWTON, NAT_1, XCMPLX_1, INT_1, CARD_4, XREAL_0, RVSUM_1,
| |
| - | INT_2, PEPIN, FUNCT_1, CARD_2, PREPOWER, FINSEQ_1, TARSKI, XBOOLE_1,
| |
| - | FUNCOP_1, WSIERP_1, XBOOLE_0, FINSEQ_2, FINSEQ_3, FINSEQ_4, RELAT_1,
| |
| - | FINSOP_1, FUNCT_2, XREAL_1, XXREAL_0, NAT_D, VALUED_0, XXREAL_2,
| |
| - | FINSET_1,PARTFUN1, PRE_POLY, CARD_1;
| |
| - | schemes NAT_1, PRE_CIRC, FINSEQ_1, FINSEQ_2, PBOOLE, CLASSES1;
| |
| - |
| |
| - | begin
| |
| - |
| |
| - |
| |
| - | now
| |
| - | let
| |
| - | Humankind be finite set,
| |
| - | Tokyoite be Subset of Humankind,
| |
| - | Numberofhair be Function of Tokyoite,NAT ;
| |
| - |
| |
| - |
| |
| - | assume LM1:
| |
| - | card (Tokyoite) = 12*10|^6;
| |
| - | assume LM2:
| |
| - | for x be object
| |
| - | st x in Tokyoite
| |
| - | holds Numberofhair.x <= 10|^6;
| |
| - |
| |
| - |
| |
| - | LM0:
| |
| - | 10|^6 + 1 < 12*10|^6
| |
| - | proof
| |
| - | 0 < 10|^6 by PREPOWER:6;
| |
| - | then
| |
| - | P2: 1*10|^6 < 11* 10|^6 by XREAL_1:68;
| |
| - | P3: 1 < 10 & 2 <= 6;
| |
| - | then
| |
| - | 10 < 10 |^6 by PREPOWER:13;
| |
| - | then
| |
| - | 1 < 10 |^6 by XXREAL_0:2,P3;
| |
| - | then
| |
| - | 1 < 11*10|^6 by P2,XXREAL_0:2;
| |
| - | then
| |
| - | P4: 1*10|^6 + 1 < 1*10|^6 + 11*10|^6 by XREAL_1:8;
| |
| - | 1*10|^6 + 11*10|^6 = (1+11)*10|^6 ;
| |
| - | hence thesis by P4;
| |
| - | end;
| |
| - |
| |
| - |
| |
| - | LM3:
| |
| - | card (rng Numberofhair) <= 10|^6+1
| |
| - | proof
| |
| - | now let y be object ;
| |
| - | assume
| |
| - | y in rng Numberofhair;
| |
| - | then
| |
| - | consider x be object
| |
| - | such that
| |
| - | A1: x in Tokyoite & y=Numberofhair.x by FUNCT_2:11;
| |
| - | Numberofhair.x <= 10|^6 by A1,LM2;
| |
| - | then
| |
| - | Numberofhair.x < 10|^6+1 by NAT_1:16,XXREAL_0:2;
| |
| - | then
| |
| - | Numberofhair.x in Segm (10|^6+1) by NAT_1:44,A1;
| |
| - | hence
| |
| - | y in Segm (10|^6+1) by A1;
| |
| - | end;
| |
| - | then
| |
| - | A2: rng Numberofhair
| |
| - | c= Segm (10|^6+1) by TARSKI:def 3;
| |
| - | then
| |
| - | card rng Numberofhair <= card Segm (10|^6+1) by NAT_1:43;
| |
| - | then
| |
| - | card rng Numberofhair <= card (10|^6+1) by ORDINAL1:def 17;
| |
| - | hence
| |
| - | card rng Numberofhair <= (10|^6+1) ;
| |
| - | end;
| |
| - |
| |
| - | LM4:
| |
| - | card (rng (Numberofhair))
| |
| - | < card (Tokyoite)
| |
| - | proof
| |
| - | reconsider N1= card (rng (Numberofhair))
| |
| - | as Element of NAT ;
| |
| - | reconsider N2= card (Tokyoite)
| |
| - | as Element of NAT ;
| |
| - | A1: N1<=(10|^6+1) & N2=12*10|^6 by LM1,LM3;
| |
| - | then
| |
| - | N1 < N2 by A1,XXREAL_0:2,LM0;
| |
| - | hence thesis ;
| |
| - | end;
| |
| - |
| |
| - |
| |
| - | EX:
| |
| - | ex x,y be object
| |
| - | st x in Tokyoite
| |
| - | & y in Tokyoite
| |
| - | & x <> y
| |
| - | & Numberofhair.x = Numberofhair.y
| |
| - |
| |
| - | proof
| |
| - | assume
| |
| - | A1:
| |
| - | not
| |
| - | ( ex x,y be object
| |
| - | st x in Tokyoite
| |
| - | & y in Tokyoite
| |
| - | & x <> y
| |
| - | & Numberofhair.x = Numberofhair.y ) ;
| |
| - |
| |
| - | then
| |
| - | A2: for x,y be object
| |
| - | st x in Tokyoite
| |
| - | & y in Tokyoite
| |
| - | & x <> y
| |
| - | holds
| |
| - | Numberofhair.x <> Numberofhair.y ;
| |
| - |
| |
| - | A3: dom Numberofhair = Tokyoite by FUNCT_2:def 1;
| |
| - | then
| |
| - | for x,y be object st x in dom Numberofhair
| |
| - | & y in dom Numberofhair
| |
| - | & Numberofhair.x = Numberofhair.y
| |
| - | holds x = y by A2;
| |
| - | then
| |
| - | Numberofhair is one-to-one by FUNCT_1:def 4;
| |
| - | then
| |
| - | card (dom Numberofhair) = card (rng Numberofhair)
| |
| - | by CARD_1:70;
| |
| - | then
| |
| - | card (Tokyoite) = card (rng (Numberofhair))
| |
| - | by A3;
| |
| - | hence contradiction by LM4;
| |
| - | end;
| |
| - | end;
| |
| - |
| |
| - |
| |
| - |
| |
| | </nowiki> | | </nowiki> |
| | | | |
environ
vocabularies NUMBERS, REAL_1, FINSEQ_1, VALUED_0, XBOOLE_0, NEWTON, ARYTM_3,
RELAT_1, NAT_1, XXREAL_0, ARYTM_1, SUBSET_1, CARD_1, CARD_3, ORDINAL4,
TARSKI, INT_2, FUNCT_1, FINSEQ_2, PRE_POLY, PBOOLE, FINSET_1, XCMPLX_0,
UPROOTS, FUNCT_2, BINOP_2, SETWISEO, INT_1, FUNCOP_1, NAT_3, XREAL_0;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_D, INT_2, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, FINSEQ_2, VALUED_0, PBOOLE, RVSUM_1, NEWTON, WSIERP_1,
TREES_4, BINOP_2, FUNCOP_1, XXREAL_2, SETWOP_2, PRE_POLY;
constructors BINOP_1, SETWISEO, NAT_D, FINSEQOP, FINSOP_1, NEWTON, WSIERP_1,
BINOP_2, XXREAL_2, RELSET_1, PRE_POLY, REAL_1,CARD_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, INT_1, BINOP_2, MEMBERED, NEWTON, VALUED_0, FINSEQ_1,
XXREAL_2, CARD_1, FUNCT_2, RELSET_1, ZFMISC_1, FINSEQ_2, PRE_POLY,
XREAL_0, RVSUM_1;
