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

Theorem wlkdvspthlem 21643
Description: Lemma for wlkdvspth 21644. (Contributed by Alexander van der Vekens, 27-Oct-2017.)
Assertion
Ref Expression
wlkdvspthlem
Distinct variable groups:   ,   ,   P,
Allowed substitution hint:   ( )

Proof of Theorem wlkdvspthlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wrdf 11788 . . . 4
213ad2ant1 979 . . 3
3 fveq2 5779 . . . . . . . . . . . . . . . . . . 19
43fveq2d 5783 . . . . . . . . . . . . . . . . . 18
5 fveq2 5779 . . . . . . . . . . . . . . . . . . 19
6 oveq1 6140 . . . . . . . . . . . . . . . . . . . 20
76fveq2d 5783 . . . . . . . . . . . . . . . . . . 19
85, 7preq12d 3923 . . . . . . . . . . . . . . . . . 18
94, 8eqeq12d 2461 . . . . . . . . . . . . . . . . 17
109rspcva 3063 . . . . . . . . . . . . . . . 16
11 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . 22
1211fveq2d 5783 . . . . . . . . . . . . . . . . . . . . 21
13 fveq2 5779 . . . . . . . . . . . . . . . . . . . . . 22
14 oveq1 6140 . . . . . . . . . . . . . . . . . . . . . . 23
1514fveq2d 5783 . . . . . . . . . . . . . . . . . . . . . 22
1613, 15preq12d 3923 . . . . . . . . . . . . . . . . . . . . 21
1712, 16eqeq12d 2461 . . . . . . . . . . . . . . . . . . . 20
1817rspcva 3063 . . . . . . . . . . . . . . . . . . 19
19 pm3.2 436 . . . . . . . . . . . . . . . . . . 19
2018, 19syl 16 . . . . . . . . . . . . . . . . . 18
2120ex 425 . . . . . . . . . . . . . . . . 17
2221com3r 76 . . . . . . . . . . . . . . . 16
2310, 22syl 16 . . . . . . . . . . . . . . 15
2423impancom 429 . . . . . . . . . . . . . 14
2524com3r 76 . . . . . . . . . . . . 13
2625pm2.43a 48 . . . . . . . . . . . 12
2726impcom 421 . . . . . . . . . . 11
28 fveq2 5779 . . . . . . . . . . . . . 14
29 eqtr2 2465 . . . . . . . . . . . . . . . . . . . 20
3029ex 425 . . . . . . . . . . . . . . . . . . 19
3130eqcoms 2450 . . . . . . . . . . . . . . . . . 18
32 eqtr2 2465 . . . . . . . . . . . . . . . . . . 19
3332ex 425 . . . . . . . . . . . . . . . . . 18
3431, 33syl6com 34 . . . . . . . . . . . . . . . . 17
3534com23 75 . . . . . . . . . . . . . . . 16
3635imp 420 . . . . . . . . . . . . . . 15
37 elfzofz 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
38 elfzofz 11209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3937, 38anim12i 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4039anim2i 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
4140ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
42 f1fveq 6060 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4341, 42syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4443notbid 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4544biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . 25
46 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
47 fzofzp1 11244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48 fzofzp1 11244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4947, 48anim12i 551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5049adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
51 f1fveq 6060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
5246, 50, 51syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
53 elfzoelz 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5453zcnd 10431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5554ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
56 elfzoelz 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
5756zcnd 10431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
5857adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
5958adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
60 ax-1cn 9103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
6160a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
6255, 59, 61addcan2d 9325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
6352, 62bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6463notbid 287 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
65 pm3.2 436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6664, 65syl6bir 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6766com13 77 . . . . . . . . . . . . . . . . . . . . . . . . 25
6845, 67syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
69 fvex 5789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
70 fvex 5789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71 fvex 5789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
72 fvex 5789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7369, 70, 71, 72preq12b 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
74 pm2.24 104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7574eqcoms 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
76 pm2.24 104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7776eqcoms 2450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7875, 77im2anan9r 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
79 ax-1 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8078, 79jaoi 370 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8173, 80sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8237, 48anim12ci 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83 f1fveq 6060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
8482, 83sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
8584biimpd 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8685ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8747, 38anim12ci 552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
88 f1fveq 6060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
8987, 88sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
9089ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
9190biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
92 oveq1 6140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9392eqeq1d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
9493adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
9560a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
9654, 95, 953jca 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9796ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
98 addass 9132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
9998eqeq1d 2455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
10097, 99syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
101 1p1e2 10149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
102101oveq2i 6144 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
103102eqeq1i 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
104 zcn 10342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
105 2cn 10125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
106104, 105jctir 526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
107 addcl 9127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
108106, 107syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
109108, 104, 1043jca 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
110 subcan2 9381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
111110bicomd 194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
11253, 109, 1113syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
113 pncan2 9367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
11453, 106, 1133syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
11554subidd 9454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
116114, 115eqeq12d 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
117112, 116bitrd 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
118103, 117syl5bb 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
119118ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
12094, 100, 1193bitrd 272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
121 2ne0 10138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
122 df-ne 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
123 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
124122, 123sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
125121, 124ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
126120, 125syl6bi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
127126ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
128127ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
12991, 128mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
130129expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131130com13 77 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
13286, 131syl6 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
133132pm2.43a 48 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134133com13 77 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
135134imp 420 . . . . . . . . . . . . . . . . . . . . . . . . . 26
13681, 135syl6com 34 . . . . . . . . . . . . . . . . . . . . . . . . 25
137136com23 75 . . . . . . . . . . . . . . . . . . . . . . . 24
13868, 137syl8 68 . . . . . . . . . . . . . . . . . . . . . . 23
139138ex 425 . . . . . . . . . . . . . . . . . . . . . 22
140139pm2.43a 48 . . . . . . . . . . . . . . . . . . . . 21
141140com14 85 . . . . . . . . . . . . . . . . . . . 20
142141pm2.43a 48 . . . . . . . . . . . . . . . . . . 19
143142pm2.43i 46 . . . . . . . . . . . . . . . . . 18
144143ex 425 . . . . . . . . . . . . . . . . 17
145144com23 75 . . . . . . . . . . . . . . . 16
146145com14 85 . . . . . . . . . . . . . . 15
14736, 146syl6com 34 . . . . . . . . . . . . . 14