dalemrot - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemrot		Structured version Unicode version

Theorem dalemrot 35524

Description: Lemma for dath 35603. Rotate triangles

and

to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalemc.l
dalemc.j	$.\/$
dalemc.a
dalemrot.y	$.\/$ $.\/$
dalemrot.z	$.\/$ $.\/$

**Assertion**
Ref	Expression
dalemrot	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

**Proof of Theorem dalemrot**
Step	Hyp	Ref	Expression
1		dalema.ph	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemkehl 35490	. . . 4
3		dalemc.a	. . . . 5
4	1, 3	dalemceb 35505	. . . 4
5	2, 4	jca 532	. . 3 $/\$
6	1	dalemqea 35494	. . . 4
7	1	dalemrea 35495	. . . 4
8	1	dalempea 35493	. . . 4
9	6, 7, 8	3jca 1176	. . 3 $/\$ $/\$
10	1	dalemtea 35497	. . . 4
11	1	dalemuea 35498	. . . 4
12	1	dalemsea 35496	. . . 4
13	10, 11, 12	3jca 1176	. . 3 $/\$ $/\$
14	5, 9, 13	3jca 1176	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		dalemc.j	. . . . 5 $.\/$
16	1, 15, 3	dalemqrprot 35515	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
17		dalemrot.y	. . . . 5 $.\/$ $.\/$
18	1	dalemyeo 35499	. . . . 5
19	17, 18	syl5eqelr 2550	. . . 4 $.\/$ $.\/$
20	16, 19	eqeltrd 2545	. . 3 $.\/$ $.\/$
21	15, 3	hlatjrot 35240	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	2, 10, 11, 12, 21	syl13anc 1230	. . . 4 $.\/$ $.\/$ $.\/$ $.\/$
23		dalemrot.z	. . . . 5 $.\/$ $.\/$
24	1	dalemzeo 35500	. . . . 5
25	23, 24	syl5eqelr 2550	. . . 4 $.\/$ $.\/$
26	22, 25	eqeltrd 2545	. . 3 $.\/$ $.\/$
27	20, 26	jca 532	. 2 $.\/$ $.\/$ $/\$ $.\/$ $.\/$
28		simp312 1144	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
29	1, 28	sylbi 195	. . . 4 $.\/$
30		simp313 1145	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	1, 30	sylbi 195	. . . 4 $.\/$
32	1	dalem-clpjq 35504	. . . 4 $.\/$
33	29, 31, 32	3jca 1176	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
34		simp322 1147	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	1, 34	sylbi 195	. . . 4 $.\/$
36		simp323 1148	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37	1, 36	sylbi 195	. . . 4 $.\/$
38		simp321 1146	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39	1, 38	sylbi 195	. . . 4 $.\/$
40	35, 37, 39	3jca 1176	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
41	1	dalemclqjt 35502	. . . 4 $.\/$
42	1	dalemclrju 35503	. . . 4 $.\/$
43	1	dalemclpjs 35501	. . . 4 $.\/$
44	41, 42, 43	3jca 1176	. . 3 $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	33, 40, 44	3jca 1176	. 2 $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46	14, 27, 45	3jca 1176	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819 class class class wbr 4456

cfv 5594 (class class class)co 6296

cbs 14644

cple 14719

cjn 15700

catm 35131

chlt 35218

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-preset 15684 df-poset 15702 df-lub 15731 df-glb 15732 df-join 15733 df-meet 15734 df-lat 15803 df-ats 35135 df-atl 35166 df-cvlat 35190 df-hlat 35219

This theorem is referenced by: dalemeea 35530 dalem6 35535 dalem7 35536 dalem11 35541 dalem12 35542 dalem29 35568 dalem30 35569 dalem31N 35570 dalem32 35571 dalem33 35572 dalem34 35573 dalem35 35574 dalem36 35575 dalem37 35576 dalem40 35579 dalem46 35585 dalem47 35586 dalem49 35588 dalem50 35589 dalem58 35597 dalem59 35598

W3C validator