Metamath Proof Explorer


Theorem pthdlem2

Description: Lemma 2 for pthd . (Contributed by Alexander van der Vekens, 11-Nov-2017) (Revised by AV, 10-Feb-2021)

Ref Expression
Hypotheses pthd.p φPWordV
pthd.r R=P1
pthd.s φi0..^Pj1..^RijPiPj
Assertion pthdlem2 φP0RP1..^R=

Proof

Step Hyp Ref Expression
1 pthd.p φPWordV
2 pthd.r R=P1
3 pthd.s φi0..^Pj1..^RijPiPj
4 lencl PWordVP0
5 df-ne P0¬P=0
6 elnnne0 PP0P0
7 6 simplbi2 P0P0P
8 5 7 syl5bir P0¬P=0P
9 1 4 8 3syl φ¬P=0P
10 eqid 0=0
11 10 orci 0=00=R
12 1 2 3 pthdlem2lem φP0=00=RP0P1..^R
13 11 12 mp3an3 φPP0P1..^R
14 eqid R=R
15 14 olci R=0R=R
16 1 2 3 pthdlem2lem φPR=0R=RPRP1..^R
17 15 16 mp3an3 φPPRP1..^R
18 wrdffz PWordVP:0P1V
19 1 18 syl φP:0P1V
20 19 adantr φPP:0P1V
21 2 oveq2i 0R=0P1
22 21 feq2i P:0RVP:0P1V
23 20 22 sylibr φPP:0RV
24 nnm1nn0 PP10
25 2 24 eqeltrid PR0
26 25 adantl φPR0
27 fvinim0ffz P:0RVR0P0RP1..^R=P0P1..^RPRP1..^R
28 23 26 27 syl2anc φPP0RP1..^R=P0P1..^RPRP1..^R
29 13 17 28 mpbir2and φPP0RP1..^R=
30 29 ex φPP0RP1..^R=
31 9 30 syld φ¬P=0P0RP1..^R=
32 oveq1 P=0P1=01
33 2 32 eqtrid P=0R=01
34 33 oveq2d P=01..^R=1..^01
35 0le2 02
36 1p1e2 1+1=2
37 35 36 breqtrri 01+1
38 0re 0
39 1re 1
40 38 39 39 lesubadd2i 01101+1
41 37 40 mpbir 011
42 1z 1
43 0z 0
44 peano2zm 001
45 43 44 ax-mp 01
46 fzon 1010111..^01=
47 42 45 46 mp2an 0111..^01=
48 41 47 mpbi 1..^01=
49 34 48 eqtrdi P=01..^R=
50 49 imaeq2d P=0P1..^R=P
51 ima0 P=
52 50 51 eqtrdi P=0P1..^R=
53 52 ineq2d P=0P0RP1..^R=P0R
54 in0 P0R=
55 53 54 eqtrdi P=0P0RP1..^R=
56 31 55 pm2.61d2 φP0RP1..^R=