demoivreALT - Intuitionistic Logic Explorer

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

Theorem demoivreALT 12170

Description: Alternate proof of demoivre 12169. 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 5970	. . . . 5
2		oveq1 5969	. . . . . . 7
3	2	fveq2d 5598	. . . . . 6
4	2	fveq2d 5598	. . . . . . 7
5	4	oveq2d 5978	. . . . . 6
6	3, 5	oveq12d 5980	. . . . 5
7	1, 6	eqeq12d 2221	. . . 4
8	7	imbi2d 230	. . 3
9		oveq2 5970	. . . . 5
10		oveq1 5969	. . . . . . 7
11	10	fveq2d 5598	. . . . . 6
12	10	fveq2d 5598	. . . . . . 7
13	12	oveq2d 5978	. . . . . 6
14	11, 13	oveq12d 5980	. . . . 5
15	9, 14	eqeq12d 2221	. . . 4
16	15	imbi2d 230	. . 3
17		oveq2 5970	. . . . 5
18		oveq1 5969	. . . . . . 7
19	18	fveq2d 5598	. . . . . 6
20	18	fveq2d 5598	. . . . . . 7
21	20	oveq2d 5978	. . . . . 6
22	19, 21	oveq12d 5980	. . . . 5
23	17, 22	eqeq12d 2221	. . . 4
24	23	imbi2d 230	. . 3
25		oveq2 5970	. . . . 5
26		oveq1 5969	. . . . . . 7
27	26	fveq2d 5598	. . . . . 6
28	26	fveq2d 5598	. . . . . . 7
29	28	oveq2d 5978	. . . . . 6
30	27, 29	oveq12d 5980	. . . . 5
31	25, 30	eqeq12d 2221	. . . 4
32	31	imbi2d 230	. . 3
33		coscl 12103	. . . . . 6
34		ax-icn 8050	. . . . . . 7
35		sincl 12102	. . . . . . 7
36		mulcl 8082	. . . . . . 7 $/\$
37	34, 35, 36	sylancr 414	. . . . . 6
38		addcl 8080	. . . . . 6 $/\$
39	33, 37, 38	syl2anc 411	. . . . 5
40		exp0 10720	. . . . 5
41	39, 40	syl 14	. . . 4
42		mul02 8489	. . . . . . . 8
43	42	fveq2d 5598	. . . . . . 7
44		cos0 12126	. . . . . . 7
45	43, 44	eqtrdi 2255	. . . . . 6
46	42	fveq2d 5598	. . . . . . . . 9
47		sin0 12125	. . . . . . . . 9
48	46, 47	eqtrdi 2255	. . . . . . . 8
49	48	oveq2d 5978	. . . . . . 7
50	34	mul01i 8493	. . . . . . 7
51	49, 50	eqtrdi 2255	. . . . . 6
52	45, 51	oveq12d 5980	. . . . 5
53		ax-1cn 8048	. . . . . 6
54	53	addridi 8244	. . . . 5
55	52, 54	eqtrdi 2255	. . . 4
56	41, 55	eqtr4d 2242	. . 3
57		expp1 10723	. . . . . . . . 9 $/\$
58	39, 57	sylan 283	. . . . . . . 8 $/\$
59	58	ancoms 268	. . . . . . 7 $/\$
60	59	adantr 276	. . . . . 6 $/\$ $/\$
61		oveq1 5969	. . . . . . 7
62	61	adantl 277	. . . . . 6 $/\$ $/\$
63		nn0cn 9335	. . . . . . . . . . . . 13
64		mulcl 8082	. . . . . . . . . . . . 13 $/\$
65	63, 64	sylan 283	. . . . . . . . . . . 12 $/\$
66		sinadd 12132	. . . . . . . . . . . 12 $/\$
67	65, 66	sylancom 420	. . . . . . . . . . 11 $/\$
68	33	adantl 277	. . . . . . . . . . . . 13 $/\$
69		sincl 12102	. . . . . . . . . . . . . 14
70	65, 69	syl 14	. . . . . . . . . . . . 13 $/\$
71		mulcom 8084	. . . . . . . . . . . . 13 $/\$
72	68, 70, 71	syl2anc 411	. . . . . . . . . . . 12 $/\$
73	72	oveq1d 5977	. . . . . . . . . . 11 $/\$
74		mulcl 8082	. . . . . . . . . . . . 13 $/\$
75	68, 70, 74	syl2anc 411	. . . . . . . . . . . 12 $/\$
76		coscl 12103	. . . . . . . . . . . . . 14
77	65, 76	syl 14	. . . . . . . . . . . . 13 $/\$
78	35	adantl 277	. . . . . . . . . . . . 13 $/\$
79		mulcl 8082	. . . . . . . . . . . . 13 $/\$
80	77, 78, 79	syl2anc 411	. . . . . . . . . . . 12 $/\$
81		addcom 8239	. . . . . . . . . . . 12 $/\$
82	75, 80, 81	syl2anc 411	. . . . . . . . . . 11 $/\$
83	67, 73, 82	3eqtr2d 2245	. . . . . . . . . 10 $/\$
84	83	oveq2d 5978	. . . . . . . . 9 $/\$
85	84	oveq2d 5978	. . . . . . . 8 $/\$
86		adddir 8093	. . . . . . . . . . . . 13 $/\$ $/\$
87		mullid 8100	. . . . . . . . . . . . . . 15
88	87	oveq2d 5978	. . . . . . . . . . . . . 14
89	88	3ad2ant3 1023	. . . . . . . . . . . . 13 $/\$ $/\$
90	86, 89	eqtrd 2239	. . . . . . . . . . . 12 $/\$ $/\$
91	63, 90	syl3an1 1283	. . . . . . . . . . 11 $/\$ $/\$
92	53, 91	mp3an2 1338	. . . . . . . . . 10 $/\$
93	92	fveq2d 5598	. . . . . . . . 9 $/\$
94	92	fveq2d 5598	. . . . . . . . . 10 $/\$
95	94	oveq2d 5978	. . . . . . . . 9 $/\$
96	93, 95	oveq12d 5980	. . . . . . . 8 $/\$
97		mulcl 8082	. . . . . . . . . . . . . 14 $/\$
98	34, 97	mpan 424	. . . . . . . . . . . . 13
99	65, 69, 98	3syl 17	. . . . . . . . . . . 12 $/\$
100	33, 37	jca 306	. . . . . . . . . . . . 13 $/\$
101	100	adantl 277	. . . . . . . . . . . 12 $/\$ $/\$
102		muladd 8486	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
103	77, 99, 101, 102	syl21anc 1249	. . . . . . . . . . 11 $/\$
104	78, 34	jctil 312	. . . . . . . . . . . . . 14 $/\$ $/\$
105	70, 34	jctil 312	. . . . . . . . . . . . . 14 $/\$ $/\$
106		mul4 8234	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107		ixi 8686	. . . . . . . . . . . . . . . 16
108	107	oveq1i 5972	. . . . . . . . . . . . . . 15
109	106, 108	eqtrdi 2255	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
110	104, 105, 109	syl2anc 411	. . . . . . . . . . . . 13 $/\$
111	110	oveq2d 5978	. . . . . . . . . . . 12 $/\$
112	111	oveq1d 5977	. . . . . . . . . . 11 $/\$
113		mul12 8231	. . . . . . . . . . . . . . . 16 $/\$ $/\$
114	34, 113	mp3an2 1338	. . . . . . . . . . . . . . 15 $/\$
115	77, 78, 114	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
116		mul12 8231	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117	34, 116	mp3an2 1338	. . . . . . . . . . . . . . 15 $/\$
118	68, 70, 117	syl2anc 411	. . . . . . . . . . . . . 14 $/\$
119	115, 118	oveq12d 5980	. . . . . . . . . . . . 13 $/\$
120		adddi 8087	. . . . . . . . . . . . . . 15 $/\$ $/\$
121	34, 120	mp3an1 1337	. . . . . . . . . . . . . 14 $/\$
122	80, 75, 121	syl2anc 411	. . . . . . . . . . . . 13 $/\$
123	119, 122	eqtr4d 2242	. . . . . . . . . . . 12 $/\$
124	123	oveq2d 5978	. . . . . . . . . . 11 $/\$
125	103, 112, 124	3eqtrd 2243	. . . . . . . . . 10 $/\$
126		mulcl 8082	. . . . . . . . . . . . . 14 $/\$
127	78, 70, 126	syl2anc 411	. . . . . . . . . . . . 13 $/\$
128		mulm1 8502	. . . . . . . . . . . . 13
129	127, 128	syl 14	. . . . . . . . . . . 12 $/\$
130	129	oveq2d 5978	. . . . . . . . . . 11 $/\$
131	130	oveq1d 5977	. . . . . . . . . 10 $/\$
132		mulcl 8082	. . . . . . . . . . . . 13 $/\$
133	77, 68, 132	syl2anc 411	. . . . . . . . . . . 12 $/\$
134		negsub 8350	. . . . . . . . . . . 12 $/\$
135	133, 127, 134	syl2anc 411	. . . . . . . . . . 11 $/\$
136	135	oveq1d 5977	. . . . . . . . . 10 $/\$
137	125, 131, 136	3eqtrd 2243	. . . . . . . . 9 $/\$
138		cosadd 12133	. . . . . . . . . . . 12 $/\$
139	65, 138	sylancom 420	. . . . . . . . . . 11 $/\$
140		mulcom 8084	. . . . . . . . . . . . 13 $/\$
141	70, 78, 140	syl2anc 411	. . . . . . . . . . . 12 $/\$
142	141	oveq2d 5978	. . . . . . . . . . 11 $/\$
143	139, 142	eqtrd 2239	. . . . . . . . . 10 $/\$
144	143	oveq1d 5977	. . . . . . . . 9 $/\$
145	137, 144	eqtr4d 2242	. . . . . . . 8 $/\$
146	85, 96, 145	3eqtr4rd 2250	. . . . . . 7 $/\$
147	146	adantr 276	. . . . . 6 $/\$ $/\$
148	60, 62, 147	3eqtrd 2243	. . . . 5 $/\$ $/\$
149	148	exp31 364	. . . 4
150	149	a2d 26	. . 3
151	8, 16, 24, 32, 56, 150	nn0ind 9517	. 2
152	151	impcom 125	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $/\$ w3a 981

wceq 1373

wcel 2177

cfv 5285 (class class class)co 5962

cc 7953

cc0 7955

c1 7956

ci 7957

caddc 7958

cmul 7960

cmin 8273

cneg 8274

cn0 9325

cexp 10715

csin 12040

ccos 12041

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4170 ax-sep 4173 ax-nul 4181 ax-pow 4229 ax-pr 4264 ax-un 4493 ax-setind 4598 ax-iinf 4649 ax-cnex 8046 ax-resscn 8047 ax-1cn 8048 ax-1re 8049 ax-icn 8050 ax-addcl 8051 ax-addrcl 8052 ax-mulcl 8053 ax-mulrcl 8054 ax-addcom 8055 ax-mulcom 8056 ax-addass 8057 ax-mulass 8058 ax-distr 8059 ax-i2m1 8060 ax-0lt1 8061 ax-1rid 8062 ax-0id 8063 ax-rnegex 8064 ax-precex 8065 ax-cnre 8066 ax-pre-ltirr 8067 ax-pre-ltwlin 8068 ax-pre-lttrn 8069 ax-pre-apti 8070 ax-pre-ltadd 8071 ax-pre-mulgt0 8072 ax-pre-mulext 8073 ax-arch 8074 ax-caucvg 8075

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-if 3576 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3860 df-int 3895 df-iun 3938 df-disj 4031 df-br 4055 df-opab 4117 df-mpt 4118 df-tr 4154 df-id 4353 df-po 4356 df-iso 4357 df-iord 4426 df-on 4428 df-ilim 4429 df-suc 4431 df-iom 4652 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-ima 4701 df-iota 5246 df-fun 5287 df-fn 5288 df-f 5289 df-f1 5290 df-fo 5291 df-f1o 5292 df-fv 5293 df-isom 5294 df-riota 5917 df-ov 5965 df-oprab 5966 df-mpo 5967 df-1st 6244 df-2nd 6245 df-recs 6409 df-irdg 6474 df-frec 6495 df-1o 6520 df-oadd 6524 df-er 6638 df-en 6846 df-dom 6847 df-fin 6848 df-sup 7107 df-pnf 8139 df-mnf 8140 df-xr 8141 df-ltxr 8142 df-le 8143 df-sub 8275 df-neg 8276 df-reap 8678 df-ap 8685 df-div 8776 df-inn 9067 df-2 9125 df-3 9126 df-4 9127 df-n0 9326 df-z 9403 df-uz 9679 df-q 9771 df-rp 9806 df-ico 10046 df-fz 10161 df-fzo 10295 df-seqfrec 10625 df-exp 10716 df-fac 10903 df-bc 10925 df-ihash 10953 df-cj 11238 df-re 11239 df-im 11240 df-rsqrt 11394 df-abs 11395 df-clim 11675 df-sumdc 11750 df-ef 12044 df-sin 12046 df-cos 12047

This theorem is referenced by: (None)

W3C validator