Metamath Proof Explorer


Theorem knoppndvlem19

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 17-Aug-2021)

Ref Expression
Hypotheses knoppndvlem19.a A=2 NJ2m
knoppndvlem19.b B=2 NJ2m+1
knoppndvlem19.j φJ0
knoppndvlem19.h φH
knoppndvlem19.n φN
Assertion knoppndvlem19 φmAHHB

Proof

Step Hyp Ref Expression
1 knoppndvlem19.a A=2 NJ2m
2 knoppndvlem19.b B=2 NJ2m+1
3 knoppndvlem19.j φJ0
4 knoppndvlem19.h φH
5 knoppndvlem19.n φN
6 2re 2
7 6 a1i φ2
8 5 nnred φN
9 7 8 remulcld φ2 N
10 2pos 0<2
11 10 a1i φ0<2
12 5 nngt0d φ0<N
13 7 8 11 12 mulgt0d φ0<2 N
14 13 gt0ne0d φ2 N0
15 3 nn0zd φJ
16 15 znegcld φJ
17 9 14 16 reexpclzd φ2 NJ
18 7 recnd φ2
19 8 recnd φN
20 18 19 14 mulne0bad φ20
21 17 7 20 redivcld φ2 NJ2
22 9 16 13 3jca φ2 NJ0<2 N
23 expgt0 2 NJ0<2 N0<2 NJ
24 22 23 syl φ0<2 NJ
25 17 7 24 11 divgt0d φ0<2 NJ2
26 25 gt0ne0d φ2 NJ20
27 4 21 26 redivcld φH2 NJ2
28 27 flcld φH2 NJ2
29 1 a1i m=H2 NJ2A=2 NJ2m
30 id m=H2 NJ2m=H2 NJ2
31 30 oveq2d m=H2 NJ22 NJ2m=2 NJ2H2 NJ2
32 29 31 eqtrd m=H2 NJ2A=2 NJ2H2 NJ2
33 32 breq1d m=H2 NJ2AH2 NJ2H2 NJ2H
34 2 a1i m=H2 NJ2B=2 NJ2m+1
35 30 oveq1d m=H2 NJ2m+1=H2 NJ2+1
36 35 oveq2d m=H2 NJ22 NJ2m+1=2 NJ2H2 NJ2+1
37 34 36 eqtrd m=H2 NJ2B=2 NJ2H2 NJ2+1
38 37 breq2d m=H2 NJ2HBH2 NJ2H2 NJ2+1
39 33 38 anbi12d m=H2 NJ2AHHB2 NJ2H2 NJ2HH2 NJ2H2 NJ2+1
40 39 adantl φm=H2 NJ2AHHB2 NJ2H2 NJ2HH2 NJ2H2 NJ2+1
41 28 zred φH2 NJ2
42 0red φ0
43 42 21 25 ltled φ02 NJ2
44 flle H2 NJ2H2 NJ2H2 NJ2
45 27 44 syl φH2 NJ2H2 NJ2
46 41 27 21 43 45 lemul2ad φ2 NJ2H2 NJ22 NJ2H2 NJ2
47 4 recnd φH
48 21 recnd φ2 NJ2
49 47 48 26 divcan2d φ2 NJ2H2 NJ2=H
50 46 49 breqtrd φ2 NJ2H2 NJ2H
51 49 eqcomd φH=2 NJ2H2 NJ2
52 peano2re H2 NJ2H2 NJ2+1
53 41 52 syl φH2 NJ2+1
54 fllep1 H2 NJ2H2 NJ2H2 NJ2+1
55 27 54 syl φH2 NJ2H2 NJ2+1
56 27 53 21 43 55 lemul2ad φ2 NJ2H2 NJ22 NJ2H2 NJ2+1
57 51 56 eqbrtrd φH2 NJ2H2 NJ2+1
58 50 57 jca φ2 NJ2H2 NJ2HH2 NJ2H2 NJ2+1
59 28 40 58 rspcedvd φmAHHB