Theorem signslema

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

	Ref	Expression
Hypotheses	signslema.1	$$⊢\phi \to E\in {\mathbb{N}}_0$$
	signslema.2	$$⊢\phi \to F\in {\mathbb{N}}_0$$
	signslema.3	$$⊢\phi \to G\in {\mathbb{N}}_0$$
	signslema.4	$$⊢\phi \to H\in {\mathbb{N}}_0$$
	signslema.5	$$⊢\phi \to \left(E<G\wedge \neg 2\parallel \left(G-E\right)\right)$$
	signslema.6	$$⊢\phi \to H-G-\left(F-E\right)\in \left\{0,2\right\}$$
Assertion	signslema	$$⊢\phi \to \left(F<H\wedge \neg 2\parallel \left(H-F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		signslema.1	$$⊢\phi \to E\in {\mathbb{N}}_0$$
2		signslema.2	$$⊢\phi \to F\in {\mathbb{N}}_0$$
3		signslema.3	$$⊢\phi \to G\in {\mathbb{N}}_0$$
4		signslema.4	$$⊢\phi \to H\in {\mathbb{N}}_0$$
5		signslema.5	$$⊢\phi \to \left(E<G\wedge \neg 2\parallel \left(G-E\right)\right)$$
6		signslema.6	$$⊢\phi \to H-G-\left(F-E\right)\in \left\{0,2\right\}$$
7	5	simpld	$$⊢\phi \to E<G$$
8	7	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to E<G$$
9	4	nn0cnd	$$⊢\phi \to H\in ℂ$$
10	2	nn0cnd	$$⊢\phi \to F\in ℂ$$
11	9 10	subcld	$$⊢\phi \to H-F\in ℂ$$
12	3	nn0cnd	$$⊢\phi \to G\in ℂ$$
13	1	nn0cnd	$$⊢\phi \to E\in ℂ$$
14	12 13	subcld	$$⊢\phi \to G-E\in ℂ$$
15	11 14	subeq0ad	$$⊢\phi \to \left(H-F-\left(G-E\right)=0\leftrightarrow H-F=G-E\right)$$
16	15	biimpa	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to H-F=G-E$$
17	16	breq2d	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \left(0<H-F\leftrightarrow 0<G-E\right)$$
18	2	nn0red	$$⊢\phi \to F\in ℝ$$
19	4	nn0red	$$⊢\phi \to H\in ℝ$$
20	18 19	posdifd	$$⊢\phi \to \left(F<H\leftrightarrow 0<H-F\right)$$
21	20	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \left(F<H\leftrightarrow 0<H-F\right)$$
22	1	nn0red	$$⊢\phi \to E\in ℝ$$
23	3	nn0red	$$⊢\phi \to G\in ℝ$$
24	22 23	posdifd	$$⊢\phi \to \left(E<G\leftrightarrow 0<G-E\right)$$
25	24	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \left(E<G\leftrightarrow 0<G-E\right)$$
26	17 21 25	3bitr4rd	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \left(E<G\leftrightarrow F<H\right)$$
27	8 26	mpbid	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to F<H$$
28		0red	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to 0\in ℝ$$
29	23 22	resubcld	$$⊢\phi \to G-E\in ℝ$$
30	29	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to G-E\in ℝ$$
31	19 18	resubcld	$$⊢\phi \to H-F\in ℝ$$
32	31	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to H-F\in ℝ$$
33	7	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to E<G$$
34	24	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to \left(E<G\leftrightarrow 0<G-E\right)$$
35	33 34	mpbid	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to 0<G-E$$
36		2pos	$$⊢0<2$$
37		breq2	$$⊢H-F-\left(G-E\right)=2\to \left(0<H-F-\left(G-E\right)\leftrightarrow 0<2\right)$$
38	36 37	mpbiri	$$⊢H-F-\left(G-E\right)=2\to 0<H-F-\left(G-E\right)$$
39	29 31	posdifd	$$⊢\phi \to \left(G-E<H-F\leftrightarrow 0<H-F-\left(G-E\right)\right)$$
40	39	biimpar	$$⊢\left(\phi \wedge 0<H-F-\left(G-E\right)\right)\to G-E<H-F$$
41	38 40	sylan2	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to G-E<H-F$$
42	28 30 32 35 41	lttrd	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to 0<H-F$$
43	20	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to \left(F<H\leftrightarrow 0<H-F\right)$$
44	42 43	mpbird	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to F<H$$
45	9 12 10 13	sub4d	$$⊢\phi \to H-G-\left(F-E\right)=H-F-\left(G-E\right)$$
46	45 6	eqeltrrd	$$⊢\phi \to H-F-\left(G-E\right)\in \left\{0,2\right\}$$
47		ovex	$$⊢H-F-\left(G-E\right)\in \mathrm{V}$$
48	47	elpr	$$⊢H-F-\left(G-E\right)\in \left\{0,2\right\}\leftrightarrow \left(H-F-\left(G-E\right)=0\vee H-F-\left(G-E\right)=2\right)$$
49	46 48	sylib	$$⊢\phi \to \left(H-F-\left(G-E\right)=0\vee H-F-\left(G-E\right)=2\right)$$
50	27 44 49	mpjaodan	$$⊢\phi \to F<H$$
51	5	simprd	$$⊢\phi \to \neg 2\parallel \left(G-E\right)$$
52	51	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \neg 2\parallel \left(G-E\right)$$
53	16	breq2d	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \left(2\parallel \left(H-F\right)\leftrightarrow 2\parallel \left(G-E\right)\right)$$
54	52 53	mtbird	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=0\right)\to \neg 2\parallel \left(H-F\right)$$
55		2z	$$⊢2\in \mathbb{Z}$$
56	3	nn0zd	$$⊢\phi \to G\in \mathbb{Z}$$
57	1	nn0zd	$$⊢\phi \to E\in \mathbb{Z}$$
58	56 57	zsubcld	$$⊢\phi \to G-E\in \mathbb{Z}$$
59		dvdsaddr	$$⊢\left(2\in \mathbb{Z}\wedge G-E\in \mathbb{Z}\right)\to \left(2\parallel \left(G-E\right)\leftrightarrow 2\parallel \left(G-E+2\right)\right)$$
60	55 58 59	sylancr	$$⊢\phi \to \left(2\parallel \left(G-E\right)\leftrightarrow 2\parallel \left(G-E+2\right)\right)$$
61	51 60	mtbid	$$⊢\phi \to \neg 2\parallel \left(G-E+2\right)$$
62	61	adantr	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to \neg 2\parallel \left(G-E+2\right)$$
63		2cnd	$$⊢\phi \to 2\in ℂ$$
64	11 14 63	subaddd	$$⊢\phi \to \left(H-F-\left(G-E\right)=2\leftrightarrow G-E+2=H-F\right)$$
65	64	biimpa	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to G-E+2=H-F$$
66	65	breq2d	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to \left(2\parallel \left(G-E+2\right)\leftrightarrow 2\parallel \left(H-F\right)\right)$$
67	62 66	mtbid	$$⊢\left(\phi \wedge H-F-\left(G-E\right)=2\right)\to \neg 2\parallel \left(H-F\right)$$
68	54 67 49	mpjaodan	$$⊢\phi \to \neg 2\parallel \left(H-F\right)$$
69	50 68	jca	$$⊢\phi \to \left(F<H\wedge \neg 2\parallel \left(H-F\right)\right)$$