relexpaddg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > relexpaddg		Structured version Visualization version Unicode version

Theorem relexpaddg 13193

Description: Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020.)

**Assertion**
Ref	Expression
relexpaddg	$/\$ $/\$ $/\$

**Proof of Theorem relexpaddg**
Step	Hyp	Ref	Expression
1		elnn0 10895	. . 3 $\/$
2		elnn0 10895	. . . . . . 7 $\/$
3		relexpaddnn 13191	. . . . . . . . . . 11 $/\$ $/\$
4	3	a1d 25	. . . . . . . . . 10 $/\$ $/\$
5	4	3exp 1230	. . . . . . . . 9
6	5	com12 31	. . . . . . . 8
7		elnn1uz2 11258	. . . . . . . . . 10 $\/$
8		coires1 5360	. . . . . . . . . . . . . 14
9		simpll 768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
10		simplr 770	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
11	9, 10	oveq12d 6326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
12		1p0e1 10744	. . . . . . . . . . . . . . . . . 18
13	11, 12	syl6eq 2521	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
14		simprr 774	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
15	13, 14	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
16	9	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
17		simprl 772	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
18		relexp1g 13166	. . . . . . . . . . . . . . . . . . 19
19	17, 18	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
20	16, 19	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
21	20	releqd 4924	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
22	15, 21	mpbird 240	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
23		1nn 10642	. . . . . . . . . . . . . . . . . 18
24	9, 23	syl6eqel 2557	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
25		relexpnndm 13181	. . . . . . . . . . . . . . . . 17 $/\$
26	24, 17, 25	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
27		ssun1 3588	. . . . . . . . . . . . . . . 16
28	26, 27	syl6ss 3430	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
29		relssres 5148	. . . . . . . . . . . . . . 15 $/\$
30	22, 28, 29	syl2anc 673	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
31	8, 30	syl5eq 2517	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
32	10	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33		relexp0g 13162	. . . . . . . . . . . . . . . 16
34	17, 33	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
35	32, 34	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
36	35	coeq2d 5002	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
37	10	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
38		ax-1cn 9615	. . . . . . . . . . . . . . . . 17
39	9, 38	syl6eqel 2557	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
40	39	addid1d 9851	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
41	37, 40	eqtrd 2505	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
42	41	oveq2d 6324	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
43	31, 36, 42	3eqtr4d 2515	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
44	43	exp43 623	. . . . . . . . . . 11
45		simp1 1030	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
46		simp3 1032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
47		relexpuzrel 13192	. . . . . . . . . . . . . . . . 17 $/\$
48	45, 46, 47	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
49		eluz2nn 11221	. . . . . . . . . . . . . . . . . . 19
50	45, 49	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
51	50, 46, 25	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
52	51, 27	syl6ss 3430	. . . . . . . . . . . . . . . 16 $/\$ $/\$
53	48, 52, 29	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
54	8, 53	syl5eq 2517	. . . . . . . . . . . . . 14 $/\$ $/\$
55		simp2 1031	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
56	55	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
57	46, 33	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$
58	56, 57	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$
59	58	coeq2d 5002	. . . . . . . . . . . . . 14 $/\$ $/\$
60	55	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61		eluzelcn 11194	. . . . . . . . . . . . . . . . . 18
62	45, 61	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
63	62	addid1d 9851	. . . . . . . . . . . . . . . 16 $/\$ $/\$
64	60, 63	eqtrd 2505	. . . . . . . . . . . . . . 15 $/\$ $/\$
65	64	oveq2d 6324	. . . . . . . . . . . . . 14 $/\$ $/\$
66	54, 59, 65	3eqtr4d 2515	. . . . . . . . . . . . 13 $/\$ $/\$
67	66	a1d 25	. . . . . . . . . . . 12 $/\$ $/\$
68	67	3exp 1230	. . . . . . . . . . 11
69	44, 68	jaoi 386	. . . . . . . . . 10 $\/$
70	7, 69	sylbi 200	. . . . . . . . 9
71	70	com12 31	. . . . . . . 8
72	6, 71	jaoi 386	. . . . . . 7 $\/$
73	2, 72	sylbi 200	. . . . . 6
74	73	com12 31	. . . . 5
75	74	3impd 1247	. . . 4 $/\$ $/\$
76		elnn1uz2 11258	. . . . . . . . 9 $\/$
77		coires1 5360	. . . . . . . . . . . . . . 15
78		relcnv 5213	. . . . . . . . . . . . . . . . 17
79		ssun1 3588	. . . . . . . . . . . . . . . . 17
80	78, 79	pm3.2i 462	. . . . . . . . . . . . . . . 16 $/\$
81		relssres 5148	. . . . . . . . . . . . . . . 16 $/\$
82	80, 81	mp1i 13	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
83	77, 82	syl5eq 2517	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
84		cnvco 5025	. . . . . . . . . . . . . . 15
85		simplr 770	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
86		1nn0 10909	. . . . . . . . . . . . . . . . . . 19
87	85, 86	syl6eqel 2557	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
88		simprl 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
89		relexpcnv 13175	. . . . . . . . . . . . . . . . . 18 $/\$
90	87, 88, 89	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
91	85	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
92		cnvexg 6758	. . . . . . . . . . . . . . . . . . 19
93	88, 92	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
94		relexp1g 13166	. . . . . . . . . . . . . . . . . 18
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
96	90, 91, 95	3eqtrd 2509	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
97		simpll 768	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
98		0nn0 10908	. . . . . . . . . . . . . . . . . . 19
99	97, 98	syl6eqel 2557	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
100		relexpcnv 13175	. . . . . . . . . . . . . . . . . 18 $/\$
101	99, 88, 100	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
102	97	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
103		relexp0g 13162	. . . . . . . . . . . . . . . . . 18
104	93, 103	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	101, 102, 104	3eqtrd 2509	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	96, 105	coeq12d 5004	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107	84, 106	syl5eq 2517	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
108	99, 87	nn0addcld 10953	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
109		relexpcnv 13175	. . . . . . . . . . . . . . . 16 $/\$
110	108, 88, 109	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
111	97, 85	oveq12d 6326	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
112		0p1e1 10743	. . . . . . . . . . . . . . . . 17
113	111, 112	syl6eq 2521	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
114	113	oveq2d 6324	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
115	110, 114, 95	3eqtrd 2509	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
116	83, 107, 115	3eqtr4d 2515	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
117		relco 5340	. . . . . . . . . . . . . 14
118		simprr 774	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	113, 118	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	113	oveq2d 6324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
121	88, 18	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
122	120, 121	eqtrd 2505	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
123	122	releqd 4924	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
124	119, 123	mpbird 240	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
125		cnveqb 5298	. . . . . . . . . . . . . 14 $/\$
126	117, 124, 125	sylancr 676	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
127	116, 126	mpbird 240	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
128	127	exp43 623	. . . . . . . . . . 11
129	128	com12 31	. . . . . . . . . 10
130		coires1 5360	. . . . . . . . . . . . . . . . 17
131		simp2 1031	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
132		simp3 1032	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
133	132, 92	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
134		relexpuzrel 13192	. . . . . . . . . . . . . . . . . . 19 $/\$
135	131, 133, 134	syl2anc 673	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
136		eluz2nn 11221	. . . . . . . . . . . . . . . . . . . . 21
137	131, 136	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
138		relexpnndm 13181	. . . . . . . . . . . . . . . . . . . 20 $/\$
139	137, 133, 138	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
140	139, 79	syl6ss 3430	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		relssres 5148	. . . . . . . . . . . . . . . . . 18 $/\$
142	135, 140, 141	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
143	130, 142	syl5eq 2517	. . . . . . . . . . . . . . . 16 $/\$ $/\$
144		simp1 1030	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
145	144	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
146	133, 103	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
147	145, 146	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
148	147	coeq2d 5002	. . . . . . . . . . . . . . . 16 $/\$ $/\$
149	144	oveq1d 6323	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
150		eluzelcn 11194	. . . . . . . . . . . . . . . . . . . 20
151	131, 150	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
152	151	addid2d 9852	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153	149, 152	eqtrd 2505	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
154	153	oveq2d 6324	. . . . . . . . . . . . . . . 16 $/\$ $/\$
155	143, 148, 154	3eqtr4d 2515	. . . . . . . . . . . . . . 15 $/\$ $/\$
156		nnnn0 10900	. . . . . . . . . . . . . . . . . . 19
157	131, 136, 156	3syl 18	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
158	157, 132, 89	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
159	144, 98	syl6eqel 2557	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
160	159, 132, 100	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
161	158, 160	coeq12d 5004	. . . . . . . . . . . . . . . 16 $/\$ $/\$
162	84, 161	syl5eq 2517	. . . . . . . . . . . . . . 15 $/\$ $/\$
163	159, 157	nn0addcld 10953	. . . . . . . . . . . . . . . 16 $/\$ $/\$
164	163, 132, 109	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
165	155, 162, 164	3eqtr4d 2515	. . . . . . . . . . . . . 14 $/\$ $/\$
166	159	nn0cnd 10951	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
167	151, 166	addcomd 9853	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168		uzaddcl 11238	. . . . . . . . . . . . . . . . . 18 $/\$
169	131, 159, 168	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
170	167, 169	eqeltrrd 2550	. . . . . . . . . . . . . . . 16 $/\$ $/\$
171		relexpuzrel 13192	. . . . . . . . . . . . . . . 16 $/\$
172	170, 132, 171	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
173	117, 172, 125	sylancr 676	. . . . . . . . . . . . . 14 $/\$ $/\$
174	165, 173	mpbird 240	. . . . . . . . . . . . 13 $/\$ $/\$
175	174	a1d 25	. . . . . . . . . . . 12 $/\$ $/\$
176	175	3exp 1230	. . . . . . . . . . 11
177	176	com12 31	. . . . . . . . . 10
178	129, 177	jaoi 386	. . . . . . . . 9 $\/$
179	76, 178	sylbi 200	. . . . . . . 8
180		coires1 5360	. . . . . . . . . . . . 13
181		simp3 1032	. . . . . . . . . . . . . . 15 $/\$ $/\$
182		relexp0rel 13177	. . . . . . . . . . . . . . 15
183	181, 182	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
184	181, 33	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
185	184	dmeqd 5042	. . . . . . . . . . . . . . . 16 $/\$ $/\$
186		dmresi 5166	. . . . . . . . . . . . . . . 16
187	185, 186	syl6eq 2521	. . . . . . . . . . . . . . 15 $/\$ $/\$
188		eqimss 3470	. . . . . . . . . . . . . . 15
189	187, 188	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
190		relssres 5148	. . . . . . . . . . . . . 14 $/\$
191	183, 189, 190	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$
192	180, 191	syl5eq 2517	. . . . . . . . . . . 12 $/\$ $/\$
193		simp1 1030	. . . . . . . . . . . . . 14 $/\$ $/\$
194	193	oveq2d 6324	. . . . . . . . . . . . 13 $/\$ $/\$
195		simp2 1031	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	195	oveq2d 6324	. . . . . . . . . . . . . 14 $/\$ $/\$
197	196, 184	eqtrd 2505	. . . . . . . . . . . . 13 $/\$ $/\$
198	194, 197	coeq12d 5004	. . . . . . . . . . . 12 $/\$ $/\$
199	193, 195	oveq12d 6326	. . . . . . . . . . . . . 14 $/\$ $/\$
200		00id 9826	. . . . . . . . . . . . . 14
201	199, 200	syl6eq 2521	. . . . . . . . . . . . 13 $/\$ $/\$
202	201	oveq2d 6324	. . . . . . . . . . . 12 $/\$ $/\$
203	192, 198, 202	3eqtr4d 2515	. . . . . . . . . . 11 $/\$ $/\$
204	203	a1d 25	. . . . . . . . . 10 $/\$ $/\$
205	204	3exp 1230	. . . . . . . . 9
206	205	com12 31	. . . . . . . 8
207	179, 206	jaoi 386	. . . . . . 7 $\/$
208	2, 207	sylbi 200	. . . . . 6
209	208	com12 31	. . . . 5
210	209	3impd 1247	. . . 4 $/\$ $/\$
211	75, 210	jaoi 386	. . 3 $\/$ $/\$ $/\$
212	1, 211	sylbi 200	. 2 $/\$ $/\$
213	212	imp 436	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

cvv 3031

cun 3388

wss 3390

cid 4749

ccnv 4838

cdm 4839

crn 4840

cres 4841

ccom 4843

wrel 4844

cfv 5589 (class class class)co 6308

cc 9555

cc0 9557

c1 9558

caddc 9560

cn 10631

c2 10681

cn0 10893

cuz 11182

crelexp 13160

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-n0 10894 df-z 10962 df-uz 11183 df-seq 12252 df-relexp 13161

This theorem is referenced by: relexpaddd 13194 relexpnul 36341

W3C validator