Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  konigsberg Unicode version

Theorem konigsberg 23082
 Description: The Konigsberg Bridge problem. If is the graph on four vertices , with edges , then vertices each have degree three, and has degree five, so there are four vertices of odd degree and thus by eupath 23076 the graph cannot have an Eulerian path. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
Hypotheses
Ref Expression
konigsberg.v
konigsberg.e
Assertion
Ref Expression
konigsberg EulPaths

Proof of Theorem konigsberg
StepHypRef Expression
1 prfi 7016 . . . . . 6
2 3ne0 9711 . . . . . . 7
3 1re 8717 . . . . . . . 8
4 1lt3 9767 . . . . . . . 8
53, 4gtneii 8810 . . . . . . 7
62, 5nelpri 3565 . . . . . 6
7 3nn0 9862 . . . . . . 7
8 hashunsng 11244 . . . . . . 7
97, 8ax-mp 10 . . . . . 6
101, 6, 9mp2an 656 . . . . 5
11 df-3 9685 . . . . . 6
12 ax-1ne0 8686 . . . . . . . . 9
1312necomi 2494 . . . . . . . 8
14 0nn0 9859 . . . . . . . . 9
15 1nn0 9860 . . . . . . . . 9
16 hashprg 11245 . . . . . . . . 9
1714, 15, 16mp2an 656 . . . . . . . 8
1813, 17mpbi 201 . . . . . . 7
1918oveq1i 5720 . . . . . 6
2011, 19eqtr4i 2276 . . . . 5
2110, 20eqtr4i 2276 . . . 4
22 konigsberg.v . . . . . . . 8
23 fzfi 10912 . . . . . . . 8
2422, 23eqeltri 2323 . . . . . . 7
25 ssrab2 3179 . . . . . . 7 VDeg
26 ssfi 6968 . . . . . . 7 VDeg VDeg
2724, 25, 26mp2an 656 . . . . . 6 VDeg
28 nn0uz 10141 . . . . . . . . . . . 12
297, 28eleqtri 2325 . . . . . . . . . . 11
30 eluzfz1 10681 . . . . . . . . . . 11
3129, 30ax-mp 10 . . . . . . . . . 10
3231, 22eleqtrri 2326 . . . . . . . . 9
33 2nn 9756 . . . . . . . . . 10
34 1nn 9637 . . . . . . . . . 10
35 2cn 9696 . . . . . . . . . . . . 13
3635mulid1i 8719 . . . . . . . . . . . 12
3736oveq1i 5720 . . . . . . . . . . 11
3837, 11eqtr4i 2276 . . . . . . . . . 10
39 1lt2 9765 . . . . . . . . . 10
4033, 15, 34, 38, 39ndvdsi 12483 . . . . . . . . 9
41 fveq2 5377 . . . . . . . . . . . . 13 VDeg VDeg
4224elexi 2736 . . . . . . . . . . . . . 14
43 df-s6 11379 . . . . . . . . . . . . . . 15 concat
44 df-s5 11378 . . . . . . . . . . . . . . . 16 concat
45 df-s4 11377 . . . . . . . . . . . . . . . . 17 concat
46 df-s3 11376 . . . . . . . . . . . . . . . . . 18 concat
47 df-s2 11375 . . . . . . . . . . . . . . . . . . 19 concat
48 3re 9697 . . . . . . . . . . . . . . . . . . . . . . . 24
493, 48, 4ltleii 8821 . . . . . . . . . . . . . . . . . . . . . . 23
5015, 28eleqtri 2325 . . . . . . . . . . . . . . . . . . . . . . . 24
517nn0zi 9927 . . . . . . . . . . . . . . . . . . . . . . . 24
52 elfz5 10668 . . . . . . . . . . . . . . . . . . . . . . . 24
5350, 51, 52mp2an 656 . . . . . . . . . . . . . . . . . . . . . . 23
5449, 53mpbir 202 . . . . . . . . . . . . . . . . . . . . . 22
5554, 22eleqtrri 2326 . . . . . . . . . . . . . . . . . . . . 21
5642, 32, 55umgrabi 23078 . . . . . . . . . . . . . . . . . . . 20
5756s1cld 11319 . . . . . . . . . . . . . . . . . . 19 Word
58 2re 9695 . . . . . . . . . . . . . . . . . . . . . . 23
59 2lt3 9766 . . . . . . . . . . . . . . . . . . . . . . 23
6058, 48, 59ltleii 8821 . . . . . . . . . . . . . . . . . . . . . 22
61 2nn0 9861 . . . . . . . . . . . . . . . . . . . . . . . 24
6261, 28eleqtri 2325 . . . . . . . . . . . . . . . . . . . . . . 23
63 elfz5 10668 . . . . . . . . . . . . . . . . . . . . . . 23
6462, 51, 63mp2an 656 . . . . . . . . . . . . . . . . . . . . . 22
6560, 64mpbir 202 . . . . . . . . . . . . . . . . . . . . 21
6665, 22eleqtrri 2326 . . . . . . . . . . . . . . . . . . . 20
6742, 32, 66umgrabi 23078 . . . . . . . . . . . . . . . . . . 19
6847, 57, 67cats1cld 11382 . . . . . . . . . . . . . . . . . 18 Word
69 eluzfz2 10682 . . . . . . . . . . . . . . . . . . . . 21
7029, 69ax-mp 10 . . . . . . . . . . . . . . . . . . . 20
7170, 22eleqtrri 2326 . . . . . . . . . . . . . . . . . . 19
7242, 32, 71umgrabi 23078 . . . . . . . . . . . . . . . . . 18
7346, 68, 72cats1cld 11382 . . . . . . . . . . . . . . . . 17 Word
7442, 55, 66umgrabi 23078 . . . . . . . . . . . . . . . . 17
7545, 73, 74cats1cld 11382 . . . . . . . . . . . . . . . 16 Word
7644, 75, 74cats1cld 11382 . . . . . . . . . . . . . . 15 Word
7742, 66, 71umgrabi 23078 . . . . . . . . . . . . . . 15
7843, 76, 77cats1cld 11382 . . . . . . . . . . . . . 14 Word
79 wrd0 11295 . . . . . . . . . . . . . . . . . . . . 21 Word
8079a1i 12 . . . . . . . . . . . . . . . . . . . 20 Word
8142, 32vdeg0i 23077 . . . . . . . . . . . . . . . . . . . 20 VDeg
82 1e0p1 10031 . . . . . . . . . . . . . . . . . . . 20
83 s0s1 11426 . . . . . . . . . . . . . . . . . . . 20 concat
8442, 80, 32, 81, 82, 55, 12, 83vdegp1bi 23080 . . . . . . . . . . . . . . . . . . 19 VDeg
85 df-2 9684 . . . . . . . . . . . . . . . . . . 19
86 2ne0 9709 . . . . . . . . . . . . . . . . . . 19
8742, 57, 32, 84, 85, 66, 86, 47vdegp1bi 23080 . . . . . . . . . . . . . . . . . 18 VDeg
8842, 68, 32, 87, 11, 71, 2, 46vdegp1bi 23080 . . . . . . . . . . . . . . . . 17 VDeg
8942, 73, 32, 88, 55, 12, 66, 86, 45vdegp1ai 23079 . . . . . . . . . . . . . . . 16 VDeg
9042, 75, 32, 89, 55, 12, 66, 86, 44vdegp1ai 23079 . . . . . . . . . . . . . . 15 VDeg
9142, 76, 32, 90, 66, 86, 71, 2, 43vdegp1ai 23079 . . . . . . . . . . . . . 14 VDeg
92 konigsberg.e . . . . . . . . . . . . . . 15
93 df-s7 11380 . . . . . . . . . . . . . . 15 concat
9492, 93eqtri 2273 . . . . . . . . . . . . . 14 concat
9542, 78, 32, 91, 66, 86, 71, 2, 94vdegp1ai 23079 . . . . . . . . . . . . 13 VDeg
9641, 95syl6eq 2301 . . . . . . . . . . . 12 VDeg
9796breq2d 3932 . . . . . . . . . . 11 VDeg
9897notbid 287 . . . . . . . . . 10 VDeg
9998elrab 2860 . . . . . . . . 9 VDeg
10032, 40, 99mpbir2an 891 . . . . . . . 8 VDeg
101 fveq2 5377 . . . . . . . . . . . . 13 VDeg VDeg
10242, 55vdeg0i 23077 . . . . . . . . . . . . . . . . . . . 20 VDeg
10342, 80, 55, 102, 82, 32, 13, 83vdegp1ci 23081 . . . . . . . . . . . . . . . . . . 19 VDeg
1043, 39gtneii 8810 . . . . . . . . . . . . . . . . . . 19
10542, 57, 55, 103, 32, 13, 66, 104, 47vdegp1ai 23079 . . . . . . . . . . . . . . . . . 18 VDeg
10642, 68, 55, 105, 32, 13, 71, 5, 46vdegp1ai 23079 . . . . . . . . . . . . . . . . 17 VDeg
10742, 73, 55, 106, 85, 66, 104, 45vdegp1bi 23080 . . . . . . . . . . . . . . . 16 VDeg
10842, 75, 55, 107, 11, 66, 104, 44vdegp1bi 23080 . . . . . . . . . . . . . . 15 VDeg
10942, 76, 55, 108, 66, 104, 71, 5, 43vdegp1ai 23079 . . . . . . . . . . . . . 14 VDeg
11042, 78, 55, 109, 66, 104, 71, 5, 94vdegp1ai 23079 . . . . . . . . . . . . 13 VDeg
111101, 110syl6eq 2301 . . . . . . . . . . . 12 VDeg
112111breq2d 3932 . . . . . . . . . . 11 VDeg
113112notbid 287 . . . . . . . . . 10 VDeg
114113elrab 2860 . . . . . . . . 9 VDeg
11555, 40, 114mpbir2an 891 . . . . . . . 8 VDeg
116 prssi 3671 . . . . . . . 8 VDeg VDeg VDeg
117100, 115, 116mp2an 656 . . . . . . 7 VDeg
118 fveq2 5377 . . . . . . . . . . . . 13 VDeg VDeg
11942, 71vdeg0i 23077 . . . . . . . . . . . . . . . . . . . 20 VDeg
120 0re 8718 . . . . . . . . . . . . . . . . . . . . 21
121 3pos 9710 . . . . . . . . . . . . . . . . . . . . 21
122120, 121ltneii 8811 . . . . . . . . . . . . . . . . . . . 20
1233, 4ltneii 8811 . . . . . . . . . . . . . . . . . . . 20
12442, 80, 71, 119, 32, 122, 55, 123, 83vdegp1ai 23079 . . . . . . . . . . . . . . . . . . 19 VDeg
12558, 59ltneii 8811 . . . . . . . . . . . . . . . . . . 19
12642, 57, 71, 124, 32, 122, 66, 125, 47vdegp1ai 23079 . . . . . . . . . . . . . . . . . 18 VDeg
12742, 68, 71, 126, 82, 32, 122, 46vdegp1ci 23081 . . . . . . . . . . . . . . . . 17 VDeg
12842, 73, 71, 127, 55, 123, 66, 125, 45vdegp1ai 23079 . . . . . . . . . . . . . . . 16 VDeg
12942, 75, 71, 128, 55, 123, 66, 125, 44vdegp1ai 23079 . . . . . . . . . . . . . . 15 VDeg
13042, 76, 71, 129, 85, 66, 125, 43vdegp1ci 23081 . . . . . . . . . . . . . 14 VDeg
13142, 78, 71, 130, 11, 66, 125, 94vdegp1ci 23081 . . . . . . . . . . . . 13 VDeg
132118, 131syl6eq 2301 . . . . . . . . . . . 12 VDeg
133132breq2d 3932 . . . . . . . . . . 11 VDeg
134133notbid 287 . . . . . . . . . 10 VDeg
135134elrab 2860 . . . . . . . . 9 VDeg
13671, 40, 135mpbir2an 891 . . . . . . . 8 VDeg
137 snssi 3659 . . . . . . . 8 VDeg VDeg
138136, 137ax-mp 10 . . . . . . 7 VDeg
139117, 138unssi 3260 . . . . . 6 VDeg
140 ssdomg 6793 . . . . . 6 VDeg VDeg VDeg
14127, 139, 140mp2 19 . . . . 5 VDeg
142 snfi 6826 . . . . . . 7
143 unfi 7009 . . . . . . 7
1441, 142, 143mp2an 656 . . . . . 6
145 hashdom 11239 . . . . . 6 VDeg VDeg VDeg
146144, 27, 145mp2an 656 . . . . 5 VDeg VDeg
147141, 146mpbir 202 . . . 4 VDeg
14821, 147eqbrtrri 3941 . . 3 VDeg
149 hashcl 11228 . . . . . 6 VDeg VDeg
15027, 149ax-mp 10 . . . . 5 VDeg
151150nn0rei 9855 . . . 4 VDeg
15248, 151lenlti 8818 . . 3 VDeg VDeg
153148, 152mpbi 201 . 2 VDeg
154 eupath 23076 . . . 4 EulPaths VDeg
155 elpri 3564 . . . 4 VDeg VDeg VDeg
156 id 21 . . . . . 6 VDeg VDeg
157156, 121syl6eqbr 3957 . . . . 5 VDeg VDeg
158 id 21 . . . . . 6 VDeg VDeg
159158, 59syl6eqbr 3957 . . . . 5 VDeg VDeg
160157, 159jaoi 370 . . . 4 VDeg VDeg VDeg
161154, 155, 1603syl 20 . . 3 EulPaths VDeg
162161necon1bi 2455 . 2 VDeg EulPaths
163153, 162ax-mp 10 1 EulPaths
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6   wb 178   wo 359   wa 360   wtru 1312   wceq 1619   wcel 1621   wne 2412  crab 2512   cdif 3075   cun 3076   wss 3078  c0 3362  cpw 3530  csn 3544  cpr 3545   class class class wbr 3920  cfv 4592  (class class class)co 5710   cdom 6747  cfn 6749  cc0 8617  c1 8618   caddc 8620   cmul 8622   clt 8747   cle 8748  c2 9675  c3 9676  cn0 9844  cz 9903  cuz 10109  cfz 10660  chash 11215  Word cword 11280   concat cconcat 11281  cs1 11282  cs2 11368  cs3 11369  cs4 11370  cs5 11371  cs6 11372  cs7 11373   cdivides 12405   EulPaths ceup 23032   VDeg cvdg 23033 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-rep 4028  ax-sep 4038  ax-nul 4046  ax-pow 4082  ax-pr 4108  ax-un 4403  ax-cnex 8673  ax-resscn 8674  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-mulcom 8681  ax-addass 8682  ax-mulass 8683  ax-distr 8684  ax-i2m1 8685  ax-1ne0 8686  ax-1rid 8687  ax-rnegex 8688  ax-rrecex 8689  ax-cnre 8690  ax-pre-lttri 8691  ax-pre-lttrn 8692  ax-pre-ltadd 8693  ax-pre-mulgt0 8694  ax-pre-sup 8695 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-nel 2415  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2516  df-v 2729  df-sbc 2922  df-csb 3010  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-pss 3091  df-nul 3363  df-if 3471  df-pw 3532  df-sn 3550  df-pr 3551  df-tp 3552  df-op 3553  df-uni 3728  df-int 3761  df-iun 3805  df-br 3921  df-opab 3975  df-mpt 3976  df-tr 4011  df-eprel 4198  df-id 4202  df-po 4207  df-so 4208  df-fr 4245  df-we 4247  df-ord 4288  df-on 4289  df-lim 4290  df-suc 4291  df-om 4548  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fo 4606  df-f1o 4607  df-fv 4608  df-ov 5713  df-oprab 5714  df-mpt2 5715  df-1st 5974  df-2nd 5975  df-iota 6143  df-riota 6190  df-recs 6274  df-rdg 6309  df-1o 6365  df-2o 6366  df-oadd 6369  df-er 6546  df-pm 6661  df-en 6750  df-dom 6751  df-sdom 6752  df-fin 6753  df-sup 7078  df-card 7456  df-cda 7678  df-pnf 8749  df-mnf 8750  df-xr 8751  df-ltxr 8752  df-le 8753  df-sub 8919  df-neg 8920  df-div 9304  df-n 9627  df-2 9684  df-3 9685  df-n0 9845  df-z 9904  df-uz 10110  df-rp 10234  df-fz 10661  df-fzo 10749  df-seq 10925  df-exp 10983  df-hash 11216  df-word 11286  df-concat 11287  df-s1 11288  df-s2 11375  df-s3 11376  df-s4 11377  df-s5 11378  df-s6 11379  df-s7 11380  df-cj 11461  df-re 11462  df-im 11463  df-sqr 11597  df-abs 11598  df-divides 12406  df-prime 12633  df-umgra 23034  df-eupa 23035  df-vdgr 23036
 Copyright terms: Public domain W3C validator