demoivreALT - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > demoivreALT		Unicode version

Theorem demoivreALT 11480

Description: Alternate proof of demoivre 11479. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
demoivreALT	$/\$

Proof of Theorem demoivreALT Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 5782	. . . . 5
2		oveq1 5781	. . . . . . 7
3	2	fveq2d 5425	. . . . . 6
4	2	fveq2d 5425	. . . . . . 7
5	4	oveq2d 5790	. . . . . 6
6	3, 5	oveq12d 5792	. . . . 5
7	1, 6	eqeq12d 2154	. . . 4
8	7	imbi2d 229	. . 3
9		oveq2 5782	. . . . 5
10		oveq1 5781	. . . . . . 7
11	10	fveq2d 5425	. . . . . 6
12	10	fveq2d 5425	. . . . . . 7
13	12	oveq2d 5790	. . . . . 6
14	11, 13	oveq12d 5792	. . . . 5
15	9, 14	eqeq12d 2154	. . . 4
16	15	imbi2d 229	. . 3
17		oveq2 5782	. . . . 5
18		oveq1 5781	. . . . . . 7
19	18	fveq2d 5425	. . . . . 6
20	18	fveq2d 5425	. . . . . . 7
21	20	oveq2d 5790	. . . . . 6
22	19, 21	oveq12d 5792	. . . . 5
23	17, 22	eqeq12d 2154	. . . 4
24	23	imbi2d 229	. . 3
25		oveq2 5782	. . . . 5
26		oveq1 5781	. . . . . . 7
27	26	fveq2d 5425	. . . . . 6
28	26	fveq2d 5425	. . . . . . 7
29	28	oveq2d 5790	. . . . . 6
30	27, 29	oveq12d 5792	. . . . 5
31	25, 30	eqeq12d 2154	. . . 4
32	31	imbi2d 229	. . 3
33		coscl 11414	. . . . . 6
34		ax-icn 7715	. . . . . . 7
35		sincl 11413	. . . . . . 7
36		mulcl 7747	. . . . . . 7 $/\$
37	34, 35, 36	sylancr 410	. . . . . 6
38		addcl 7745	. . . . . 6 $/\$
39	33, 37, 38	syl2anc 408	. . . . 5
40		exp0 10297	. . . . 5
41	39, 40	syl 14	. . . 4
42		mul02 8149	. . . . . . . 8
43	42	fveq2d 5425	. . . . . . 7
44		cos0 11437	. . . . . . 7
45	43, 44	syl6eq 2188	. . . . . 6
46	42	fveq2d 5425	. . . . . . . . 9
47		sin0 11436	. . . . . . . . 9
48	46, 47	syl6eq 2188	. . . . . . . 8
49	48	oveq2d 5790	. . . . . . 7
50	34	mul01i 8153	. . . . . . 7
51	49, 50	syl6eq 2188	. . . . . 6
52	45, 51	oveq12d 5792	. . . . 5
53		ax-1cn 7713	. . . . . 6
54	53	addid1i 7904	. . . . 5
55	52, 54	syl6eq 2188	. . . 4
56	41, 55	eqtr4d 2175	. . 3
57		expp1 10300	. . . . . . . . 9 $/\$
58	39, 57	sylan 281	. . . . . . . 8 $/\$
59	58	ancoms 266	. . . . . . 7 $/\$
60	59	adantr 274	. . . . . 6 $/\$ $/\$
61		oveq1 5781	. . . . . . 7
62	61	adantl 275	. . . . . 6 $/\$ $/\$
63		nn0cn 8987	. . . . . . . . . . . . 13
64		mulcl 7747	. . . . . . . . . . . . 13 $/\$
65	63, 64	sylan 281	. . . . . . . . . . . 12 $/\$
66		sinadd 11443	. . . . . . . . . . . 12 $/\$
67	65, 66	sylancom 416	. . . . . . . . . . 11 $/\$
68	33	adantl 275	. . . . . . . . . . . . 13 $/\$
69		sincl 11413	. . . . . . . . . . . . . 14
70	65, 69	syl 14	. . . . . . . . . . . . 13 $/\$
71		mulcom 7749	. . . . . . . . . . . . 13 $/\$
72	68, 70, 71	syl2anc 408	. . . . . . . . . . . 12 $/\$
73	72	oveq1d 5789	. . . . . . . . . . 11 $/\$
74		mulcl 7747	. . . . . . . . . . . . 13 $/\$
75	68, 70, 74	syl2anc 408	. . . . . . . . . . . 12 $/\$
76		coscl 11414	. . . . . . . . . . . . . 14
77	65, 76	syl 14	. . . . . . . . . . . . 13 $/\$
78	35	adantl 275	. . . . . . . . . . . . 13 $/\$
79		mulcl 7747	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	syl2anc 408	. . . . . . . . . . . 12 $/\$
81		addcom 7899	. . . . . . . . . . . 12 $/\$
82	75, 80, 81	syl2anc 408	. . . . . . . . . . 11 $/\$
83	67, 73, 82	3eqtr2d 2178	. . . . . . . . . 10 $/\$
84	83	oveq2d 5790	. . . . . . . . 9 $/\$
85	84	oveq2d 5790	. . . . . . . 8 $/\$
86		adddir 7757	. . . . . . . . . . . . 13 $/\$ $/\$
87		mulid2 7764	. . . . . . . . . . . . . . 15
88	87	oveq2d 5790	. . . . . . . . . . . . . 14
89	88	3ad2ant3 1004	. . . . . . . . . . . . 13 $/\$ $/\$
90	86, 89	eqtrd 2172	. . . . . . . . . . . 12 $/\$ $/\$
91	63, 90	syl3an1 1249	. . . . . . . . . . 11 $/\$ $/\$
92	53, 91	mp3an2 1303	. . . . . . . . . 10 $/\$
93	92	fveq2d 5425	. . . . . . . . 9 $/\$
94	92	fveq2d 5425	. . . . . . . . . 10 $/\$
95	94	oveq2d 5790	. . . . . . . . 9 $/\$
96	93, 95	oveq12d 5792	. . . . . . . 8 $/\$
97		mulcl 7747	. . . . . . . . . . . . . 14 $/\$
98	34, 97	mpan 420	. . . . . . . . . . . . 13
99	65, 69, 98	3syl 17	. . . . . . . . . . . 12 $/\$
100	33, 37	jca 304	. . . . . . . . . . . . 13 $/\$
101	100	adantl 275	. . . . . . . . . . . 12 $/\$ $/\$
102		muladd 8146	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
103	77, 99, 101, 102	syl21anc 1215	. . . . . . . . . . 11 $/\$
104	78, 34	jctil 310	. . . . . . . . . . . . . 14 $/\$ $/\$
105	70, 34	jctil 310	. . . . . . . . . . . . . 14 $/\$ $/\$
106		mul4 7894	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107		ixi 8345	. . . . . . . . . . . . . . . 16
108	107	oveq1i 5784	. . . . . . . . . . . . . . 15
109	106, 108	syl6eq 2188	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
110	104, 105, 109	syl2anc 408	. . . . . . . . . . . . 13 $/\$
111	110	oveq2d 5790	. . . . . . . . . . . 12 $/\$
112	111	oveq1d 5789	. . . . . . . . . . 11 $/\$
113		mul12 7891	. . . . . . . . . . . . . . . 16 $/\$ $/\$
114	34, 113	mp3an2 1303	. . . . . . . . . . . . . . 15 $/\$
115	77, 78, 114	syl2anc 408	. . . . . . . . . . . . . 14 $/\$
116		mul12 7891	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	34, 116	mp3an2 1303	. . . . . . . . . . . . . . 15 $/\$
118	68, 70, 117	syl2anc 408	. . . . . . . . . . . . . 14 $/\$
119	115, 118	oveq12d 5792	. . . . . . . . . . . . 13 $/\$
120		adddi 7752	. . . . . . . . . . . . . . 15 $/\$ $/\$
121	34, 120	mp3an1 1302	. . . . . . . . . . . . . 14 $/\$
122	80, 75, 121	syl2anc 408	. . . . . . . . . . . . 13 $/\$
123	119, 122	eqtr4d 2175	. . . . . . . . . . . 12 $/\$
124	123	oveq2d 5790	. . . . . . . . . . 11 $/\$
125	103, 112, 124	3eqtrd 2176	. . . . . . . . . 10 $/\$
126		mulcl 7747	. . . . . . . . . . . . . 14 $/\$
127	78, 70, 126	syl2anc 408	. . . . . . . . . . . . 13 $/\$
128		mulm1 8162	. . . . . . . . . . . . 13
129	127, 128	syl 14	. . . . . . . . . . . 12 $/\$
130	129	oveq2d 5790	. . . . . . . . . . 11 $/\$
131	130	oveq1d 5789	. . . . . . . . . 10 $/\$
132		mulcl 7747	. . . . . . . . . . . . 13 $/\$
133	77, 68, 132	syl2anc 408	. . . . . . . . . . . 12 $/\$
134		negsub 8010	. . . . . . . . . . . 12 $/\$
135	133, 127, 134	syl2anc 408	. . . . . . . . . . 11 $/\$
136	135	oveq1d 5789	. . . . . . . . . 10 $/\$
137	125, 131, 136	3eqtrd 2176	. . . . . . . . 9 $/\$
138		cosadd 11444	. . . . . . . . . . . 12 $/\$
139	65, 138	sylancom 416	. . . . . . . . . . 11 $/\$
140		mulcom 7749	. . . . . . . . . . . . 13 $/\$
141	70, 78, 140	syl2anc 408	. . . . . . . . . . . 12 $/\$
142	141	oveq2d 5790	. . . . . . . . . . 11 $/\$
143	139, 142	eqtrd 2172	. . . . . . . . . 10 $/\$
144	143	oveq1d 5789	. . . . . . . . 9 $/\$
145	137, 144	eqtr4d 2175	. . . . . . . 8 $/\$
146	85, 96, 145	3eqtr4rd 2183	. . . . . . 7 $/\$
147	146	adantr 274	. . . . . 6 $/\$ $/\$
148	60, 62, 147	3eqtrd 2176	. . . . 5 $/\$ $/\$
149	148	exp31 361	. . . 4
150	149	a2d 26	. . 3
151	8, 16, 24, 32, 56, 150	nn0ind 9165	. 2
152	151	impcom 124	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103 $/\$ w3a 962

wceq 1331

wcel 1480

cfv 5123 (class class class)co 5774

cc 7618

cc0 7620

c1 7621

ci 7622

caddc 7623

cmul 7625

cmin 7933

cneg 7934

cn0 8977

cexp 10292

csin 11350

ccos 11351

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-coll 4043 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502 ax-cnex 7711 ax-resscn 7712 ax-1cn 7713 ax-1re 7714 ax-icn 7715 ax-addcl 7716 ax-addrcl 7717 ax-mulcl 7718 ax-mulrcl 7719 ax-addcom 7720 ax-mulcom 7721 ax-addass 7722 ax-mulass 7723 ax-distr 7724 ax-i2m1 7725 ax-0lt1 7726 ax-1rid 7727 ax-0id 7728 ax-rnegex 7729 ax-precex 7730 ax-cnre 7731 ax-pre-ltirr 7732 ax-pre-ltwlin 7733 ax-pre-lttrn 7734 ax-pre-apti 7735 ax-pre-ltadd 7736 ax-pre-mulgt0 7737 ax-pre-mulext 7738 ax-arch 7739 ax-caucvg 7740

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-nel 2404 df-ral 2421 df-rex 2422 df-reu 2423 df-rmo 2424 df-rab 2425 df-v 2688 df-sbc 2910 df-csb 3004 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-if 3475 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-iun 3815 df-disj 3907 df-br 3930 df-opab 3990 df-mpt 3991 df-tr 4027 df-id 4215 df-po 4218 df-iso 4219 df-iord 4288 df-on 4290 df-ilim 4291 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-res 4551 df-ima 4552 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-f1 5128 df-fo 5129 df-f1o 5130 df-fv 5131 df-isom 5132 df-riota 5730 df-ov 5777 df-oprab 5778 df-mpo 5779 df-1st 6038 df-2nd 6039 df-recs 6202 df-irdg 6267 df-frec 6288 df-1o 6313 df-oadd 6317 df-er 6429 df-en 6635 df-dom 6636 df-fin 6637 df-sup 6871 df-pnf 7802 df-mnf 7803 df-xr 7804 df-ltxr 7805 df-le 7806 df-sub 7935 df-neg 7936 df-reap 8337 df-ap 8344 df-div 8433 df-inn 8721 df-2 8779 df-3 8780 df-4 8781 df-n0 8978 df-z 9055 df-uz 9327 df-q 9412 df-rp 9442 df-ico 9677 df-fz 9791 df-fzo 9920 df-seqfrec 10219 df-exp 10293 df-fac 10472 df-bc 10494 df-ihash 10522 df-cj 10614 df-re 10615 df-im 10616 df-rsqrt 10770 df-abs 10771 df-clim 11048 df-sumdc 11123 df-ef 11354 df-sin 11356 df-cos 11357

This theorem is referenced by: (None)

W3C validator