Description: Lemma 1 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | clwlkclwwlklem2a1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lencl | |
|
2 | nn0cn | |
|
3 | peano2cnm | |
|
4 | 3 | subid1d | |
5 | 4 | oveq1d | |
6 | sub1m1 | |
|
7 | 5 6 | eqtrd | |
8 | 1 2 7 | 3syl | |
9 | 8 | adantr | |
10 | 9 | oveq2d | |
11 | 10 | raleqdv | |
12 | 11 | biimpcd | |
13 | 12 | adantr | |
14 | 13 | adantl | |
15 | 14 | impcom | |
16 | lsw | |
|
17 | 2m1e1 | |
|
18 | 17 | a1i | |
19 | 18 | eqcomd | |
20 | 19 | oveq2d | |
21 | 1 2 | syl | |
22 | 2cnd | |
|
23 | 1cnd | |
|
24 | 21 22 23 | subsubd | |
25 | 20 24 | eqtrd | |
26 | 25 | fveq2d | |
27 | 16 26 | eqtrd | |
28 | 27 | adantr | |
29 | 28 | adantr | |
30 | eqeq1 | |
|
31 | 30 | adantl | |
32 | 29 31 | mpbid | |
33 | 32 | preq2d | |
34 | 33 | eleq1d | |
35 | 34 | biimpd | |
36 | 35 | ex | |
37 | 36 | com13 | |
38 | 37 | adantl | |
39 | 38 | impcom | |
40 | 39 | impcom | |
41 | ovexd | |
|
42 | fveq2 | |
|
43 | fvoveq1 | |
|
44 | 42 43 | preq12d | |
45 | 44 | eleq1d | |
46 | 45 | ralunsn | |
47 | 41 46 | syl | |
48 | 15 40 47 | mpbir2and | |
49 | 1e2m1 | |
|
50 | 49 | a1i | |
51 | 50 | oveq2d | |
52 | 51 24 | eqtrd | |
53 | 52 | oveq2d | |
54 | 53 | adantr | |
55 | nn0re | |
|
56 | 2re | |
|
57 | 56 | a1i | |
58 | 55 57 | subge0d | |
59 | 58 | biimprd | |
60 | nn0z | |
|
61 | 2z | |
|
62 | 61 | a1i | |
63 | 60 62 | zsubcld | |
64 | 59 63 | jctild | |
65 | 1 64 | syl | |
66 | 65 | imp | |
67 | elnn0z | |
|
68 | 66 67 | sylibr | |
69 | elnn0uz | |
|
70 | 68 69 | sylib | |
71 | fzosplitsn | |
|
72 | 70 71 | syl | |
73 | 54 72 | eqtrd | |
74 | 73 | adantr | |
75 | 74 | raleqdv | |
76 | 48 75 | mpbird | |
77 | 76 | ex | |