Theorem swrdswrdlem 12684

Description: Lemma for swrdswrd 12685. (Contributed by Alexander van der Vekens, 4-Apr-2018.)

Assertion

Ref	Expression
swrdswrdlem

Proof of Theorem swrdswrdlem

Step	Hyp	Ref	Expression
1		simpl1 999	. 2
2		elfz2 11708	. . . . . 6
3		elfz2nn0 11798	. . . . . . . . . . . 12
4		elfz2nn0 11798	. . . . . . . . . . . . . . . . 17
5		nn0addcl 10856	. . . . . . . . . . . . . . . . . . . . . . 23
6	5	adantrr 716	. . . . . . . . . . . . . . . . . . . . . 22
7	6	adantr 465	. . . . . . . . . . . . . . . . . . . . 21
8		elnn0z 10902	. . . . . . . . . . . . . . . . . . . . . . . . 25
9		0red 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
10		zre 10893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
11	10	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
12		zre 10893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
13	12	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
14		letr 9699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
15	9, 11, 13, 14	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
16		elnn0z 10902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
17		nn0addcl 10856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
18	17	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
19	16, 18	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
20	19	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
21	20	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
22	15, 21	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
23	22	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
24	23	com34 83	. . . . . . . . . . . . . . . . . . . . . . . . . 26
25	24	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . 25
26	8, 25	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . 24
27	26	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23
28	27	impcom 430	. . . . . . . . . . . . . . . . . . . . . 22
29	28	imp 429	. . . . . . . . . . . . . . . . . . . . 21
30		nn0re 10829	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24
32	31	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23
33	12	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24
34	33	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23
35		nn0re 10829	. . . . . . . . . . . . . . . . . . . . . . . 24
36	35	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23
37	32, 34, 36	leadd2d 10172	. . . . . . . . . . . . . . . . . . . . . 22
38	37	biimpa 484	. . . . . . . . . . . . . . . . . . . . 21
39	7, 29, 38	3jca 1176	. . . . . . . . . . . . . . . . . . . 20
40	39	exp31 604	. . . . . . . . . . . . . . . . . . 19
41	40	com23 78	. . . . . . . . . . . . . . . . . 18
42	41	3ad2ant1 1017	. . . . . . . . . . . . . . . . 17
43	4, 42	sylbi 195	. . . . . . . . . . . . . . . 16
44	43	3ad2ant3 1019	. . . . . . . . . . . . . . 15
45	44	com13 80	. . . . . . . . . . . . . 14
46	45	ex 434	. . . . . . . . . . . . 13
47	46	3ad2ant1 1017	. . . . . . . . . . . 12
48	3, 47	sylbi 195	. . . . . . . . . . 11
49	48	com13 80	. . . . . . . . . 10
50	49	adantr 465	. . . . . . . . 9
51	50	com12 31	. . . . . . . 8
52	51	3ad2ant3 1019	. . . . . . 7
53	52	imp 429	. . . . . 6
54	2, 53	sylbi 195	. . . . 5
55	54	impcom 430	. . . 4
56	55	impcom 430	. . 3
57		elfz2nn0 11798	. . 3
58	56, 57	sylibr 212	. 2
59		elfz2nn0 11798	. . . . . . . . . . . . . . . 16
60	28	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . 25
61	60	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24
62	61	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23
63	62	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22
64		simpr2 1003	. . . . . . . . . . . . . . . . . . . . . 22
65		nn0re 10829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
66	65, 35	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
67		nn0re 10829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
68	66, 67	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
69		simpllr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
70		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
71		simplll 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
72	69, 70, 71	leaddsub2d 10179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
73		readdcl 9596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
74	73	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
75	74	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
76	75	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
77	76	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
78		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
79	78	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
80		letr 9699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
81	80	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
82	77, 71, 79, 81	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
83	82	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
84	83	a1dd 46	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
85	84	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
86	72, 85	sylbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
87	86	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
88	68, 12, 87	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
89	88	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
90	89	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	90	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	91	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	94	3imp 1190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96	95	com15 93	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
97	96	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
98	15, 97	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
99	98	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
100	99	com35 90	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
101	100	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102	101	impd 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
103	102	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
104	103	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
105	8, 104	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
106	105	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25
107	106	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . 24
108	107	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23
109	108	imp 429	. . . . . . . . . . . . . . . . . . . . . 22
110	63, 64, 109	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21
111	110	exp41 610	. . . . . . . . . . . . . . . . . . . 20
112	111	com24 87	. . . . . . . . . . . . . . . . . . 19
113	112	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 18
114	4, 113	sylbi 195	. . . . . . . . . . . . . . . . 17
115	114	com12 31	. . . . . . . . . . . . . . . 16
116	59, 115	sylbi 195	. . . . . . . . . . . . . . 15
117	116	imp 429	. . . . . . . . . . . . . 14
118	117	3adant1 1014	. . . . . . . . . . . . 13
119	118	com13 80	. . . . . . . . . . . 12
120	119	ex 434	. . . . . . . . . . 11
121	120	3ad2ant1 1017	. . . . . . . . . 10
122	3, 121	sylbi 195	. . . . . . . . 9
123	122	com3l 81	. . . . . . . 8
124	123	3ad2ant3 1019	. . . . . . 7
125	124	imp 429	. . . . . 6
126	2, 125	sylbi 195	. . . . 5
127	126	impcom 430	. . . 4
128	127	impcom 430	. . 3
129		elfz2nn0 11798	. . 3
130	128, 129	sylibr 212	. 2
131	1, 58, 130	3jca 1176	1