Metamath Proof Explorer


Theorem signslema

Description: Computational part of ~? signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018)

Ref Expression
Hypotheses signslema.1 φE0
signslema.2 φF0
signslema.3 φG0
signslema.4 φH0
signslema.5 φE<G¬2GE
signslema.6 φH-G-FE02
Assertion signslema φF<H¬2HF

Proof

Step Hyp Ref Expression
1 signslema.1 φE0
2 signslema.2 φF0
3 signslema.3 φG0
4 signslema.4 φH0
5 signslema.5 φE<G¬2GE
6 signslema.6 φH-G-FE02
7 5 simpld φE<G
8 7 adantr φH-F-GE=0E<G
9 4 nn0cnd φH
10 2 nn0cnd φF
11 9 10 subcld φHF
12 3 nn0cnd φG
13 1 nn0cnd φE
14 12 13 subcld φGE
15 11 14 subeq0ad φH-F-GE=0HF=GE
16 15 biimpa φH-F-GE=0HF=GE
17 16 breq2d φH-F-GE=00<HF0<GE
18 2 nn0red φF
19 4 nn0red φH
20 18 19 posdifd φF<H0<HF
21 20 adantr φH-F-GE=0F<H0<HF
22 1 nn0red φE
23 3 nn0red φG
24 22 23 posdifd φE<G0<GE
25 24 adantr φH-F-GE=0E<G0<GE
26 17 21 25 3bitr4rd φH-F-GE=0E<GF<H
27 8 26 mpbid φH-F-GE=0F<H
28 0red φH-F-GE=20
29 23 22 resubcld φGE
30 29 adantr φH-F-GE=2GE
31 19 18 resubcld φHF
32 31 adantr φH-F-GE=2HF
33 7 adantr φH-F-GE=2E<G
34 24 adantr φH-F-GE=2E<G0<GE
35 33 34 mpbid φH-F-GE=20<GE
36 2pos 0<2
37 breq2 H-F-GE=20<H-F-GE0<2
38 36 37 mpbiri H-F-GE=20<H-F-GE
39 29 31 posdifd φGE<HF0<H-F-GE
40 39 biimpar φ0<H-F-GEGE<HF
41 38 40 sylan2 φH-F-GE=2GE<HF
42 28 30 32 35 41 lttrd φH-F-GE=20<HF
43 20 adantr φH-F-GE=2F<H0<HF
44 42 43 mpbird φH-F-GE=2F<H
45 9 12 10 13 sub4d φH-G-FE=H-F-GE
46 45 6 eqeltrrd φH-F-GE02
47 ovex H-F-GEV
48 47 elpr H-F-GE02H-F-GE=0H-F-GE=2
49 46 48 sylib φH-F-GE=0H-F-GE=2
50 27 44 49 mpjaodan φF<H
51 5 simprd φ¬2GE
52 51 adantr φH-F-GE=0¬2GE
53 16 breq2d φH-F-GE=02HF2GE
54 52 53 mtbird φH-F-GE=0¬2HF
55 2z 2
56 3 nn0zd φG
57 1 nn0zd φE
58 56 57 zsubcld φGE
59 dvdsaddr 2GE2GE2G-E+2
60 55 58 59 sylancr φ2GE2G-E+2
61 51 60 mtbid φ¬2G-E+2
62 61 adantr φH-F-GE=2¬2G-E+2
63 2cnd φ2
64 11 14 63 subaddd φH-F-GE=2G-E+2=HF
65 64 biimpa φH-F-GE=2G-E+2=HF
66 65 breq2d φH-F-GE=22G-E+22HF
67 62 66 mtbid φH-F-GE=2¬2HF
68 54 67 49 mpjaodan φ¬2HF
69 50 68 jca φF<H¬2HF