Metamath Proof Explorer

Theorem signslema

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

Ref Expression
Hypotheses signslema.1 ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
signslema.2 ⊢ ( 𝜑 → 𝐹 ∈ ℕ0 )
signslema.3 ⊢ ( 𝜑 → 𝐺 ∈ ℕ0 )
signslema.4 ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
signslema.5 ⊢ ( 𝜑 → ( 𝐸 < 𝐺 ∧ ¬ 2 ∥ ( 𝐺 − 𝐸 ) ) )
signslema.6 ⊢ ( 𝜑 → ( ( 𝐻 − 𝐺 ) − ( 𝐹 − 𝐸 ) ) ∈ { 0 , 2 } )
Assertion signslema ( 𝜑 → ( 𝐹 < 𝐻 ∧ ¬ 2 ∥ ( 𝐻 − 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 signslema.1 ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
2 signslema.2 ⊢ ( 𝜑 → 𝐹 ∈ ℕ0 )
3 signslema.3 ⊢ ( 𝜑 → 𝐺 ∈ ℕ0 )
4 signslema.4 ⊢ ( 𝜑 → 𝐻 ∈ ℕ0 )
5 signslema.5 ⊢ ( 𝜑 → ( 𝐸 < 𝐺 ∧ ¬ 2 ∥ ( 𝐺 − 𝐸 ) ) )
6 signslema.6 ⊢ ( 𝜑 → ( ( 𝐻 − 𝐺 ) − ( 𝐹 − 𝐸 ) ) ∈ { 0 , 2 } )
7 5 simpld ⊢ ( 𝜑 → 𝐸 < 𝐺 )
8 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → 𝐸 < 𝐺 )
9 4 nn0cnd ⊢ ( 𝜑 → 𝐻 ∈ ℂ )
10 2 nn0cnd ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
11 9 10 subcld ⊢ ( 𝜑 → ( 𝐻 − 𝐹 ) ∈ ℂ )
12 3 nn0cnd ⊢ ( 𝜑 → 𝐺 ∈ ℂ )
13 1 nn0cnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
14 12 13 subcld ⊢ ( 𝜑 → ( 𝐺 − 𝐸 ) ∈ ℂ )
15 11 14 subeq0ad ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ↔ ( 𝐻 − 𝐹 ) = ( 𝐺 − 𝐸 ) ) )
16 15 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 𝐻 − 𝐹 ) = ( 𝐺 − 𝐸 ) )
17 16 breq2d ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 0 < ( 𝐻 − 𝐹 ) ↔ 0 < ( 𝐺 − 𝐸 ) ) )
18 2 nn0red ⊢ ( 𝜑 → 𝐹 ∈ ℝ )
19 4 nn0red ⊢ ( 𝜑 → 𝐻 ∈ ℝ )
20 18 19 posdifd ⊢ ( 𝜑 → ( 𝐹 < 𝐻 ↔ 0 < ( 𝐻 − 𝐹 ) ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 𝐹 < 𝐻 ↔ 0 < ( 𝐻 − 𝐹 ) ) )
22 1 nn0red ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
23 3 nn0red ⊢ ( 𝜑 → 𝐺 ∈ ℝ )
24 22 23 posdifd ⊢ ( 𝜑 → ( 𝐸 < 𝐺 ↔ 0 < ( 𝐺 − 𝐸 ) ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 𝐸 < 𝐺 ↔ 0 < ( 𝐺 − 𝐸 ) ) )
26 17 21 25 3bitr4rd ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 𝐸 < 𝐺 ↔ 𝐹 < 𝐻 ) )
27 8 26 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → 𝐹 < 𝐻 )
28 0red ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → 0 ∈ ℝ )
29 23 22 resubcld ⊢ ( 𝜑 → ( 𝐺 − 𝐸 ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 𝐺 − 𝐸 ) ∈ ℝ )
31 19 18 resubcld ⊢ ( 𝜑 → ( 𝐻 − 𝐹 ) ∈ ℝ )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 𝐻 − 𝐹 ) ∈ ℝ )
33 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → 𝐸 < 𝐺 )
34 24 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 𝐸 < 𝐺 ↔ 0 < ( 𝐺 − 𝐸 ) ) )
35 33 34 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → 0 < ( 𝐺 − 𝐸 ) )
36 2pos ⊢ 0 < 2
37 breq2 ⊢ ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 → ( 0 < ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ↔ 0 < 2 ) )
38 36 37 mpbiri ⊢ ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 → 0 < ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) )
39 29 31 posdifd ⊢ ( 𝜑 → ( ( 𝐺 − 𝐸 ) < ( 𝐻 − 𝐹 ) ↔ 0 < ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ) )
40 39 biimpar ⊢ ( ( 𝜑 ∧ 0 < ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ) → ( 𝐺 − 𝐸 ) < ( 𝐻 − 𝐹 ) )
41 38 40 sylan2 ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 𝐺 − 𝐸 ) < ( 𝐻 − 𝐹 ) )
42 28 30 32 35 41 lttrd ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → 0 < ( 𝐻 − 𝐹 ) )
43 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 𝐹 < 𝐻 ↔ 0 < ( 𝐻 − 𝐹 ) ) )
44 42 43 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → 𝐹 < 𝐻 )
45 9 12 10 13 sub4d ⊢ ( 𝜑 → ( ( 𝐻 − 𝐺 ) − ( 𝐹 − 𝐸 ) ) = ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) )
46 45 6 eqeltrrd ⊢ ( 𝜑 → ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ∈ { 0 , 2 } )
47 ovex ⊢ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ∈ V
48 47 elpr ⊢ ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) ∈ { 0 , 2 } ↔ ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ∨ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) )
49 46 48 sylib ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ∨ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) )
50 27 44 49 mpjaodan ⊢ ( 𝜑 → 𝐹 < 𝐻 )
51 5 simprd ⊢ ( 𝜑 → ¬ 2 ∥ ( 𝐺 − 𝐸 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ¬ 2 ∥ ( 𝐺 − 𝐸 ) )
53 16 breq2d ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ( 2 ∥ ( 𝐻 − 𝐹 ) ↔ 2 ∥ ( 𝐺 − 𝐸 ) ) )
54 52 53 mtbird ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 0 ) → ¬ 2 ∥ ( 𝐻 − 𝐹 ) )
55 2z ⊢ 2 ∈ ℤ
56 3 nn0zd ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
57 1 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
58 56 57 zsubcld ⊢ ( 𝜑 → ( 𝐺 − 𝐸 ) ∈ ℤ )
59 dvdsaddr ⊢ ( ( 2 ∈ ℤ ∧ ( 𝐺 − 𝐸 ) ∈ ℤ ) → ( 2 ∥ ( 𝐺 − 𝐸 ) ↔ 2 ∥ ( ( 𝐺 − 𝐸 ) + 2 ) ) )
60 55 58 59 sylancr ⊢ ( 𝜑 → ( 2 ∥ ( 𝐺 − 𝐸 ) ↔ 2 ∥ ( ( 𝐺 − 𝐸 ) + 2 ) ) )
61 51 60 mtbid ⊢ ( 𝜑 → ¬ 2 ∥ ( ( 𝐺 − 𝐸 ) + 2 ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ¬ 2 ∥ ( ( 𝐺 − 𝐸 ) + 2 ) )
63 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
64 11 14 63 subaddd ⊢ ( 𝜑 → ( ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ↔ ( ( 𝐺 − 𝐸 ) + 2 ) = ( 𝐻 − 𝐹 ) ) )
65 64 biimpa ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( ( 𝐺 − 𝐸 ) + 2 ) = ( 𝐻 − 𝐹 ) )
66 65 breq2d ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ( 2 ∥ ( ( 𝐺 − 𝐸 ) + 2 ) ↔ 2 ∥ ( 𝐻 − 𝐹 ) ) )
67 62 66 mtbid ⊢ ( ( 𝜑 ∧ ( ( 𝐻 − 𝐹 ) − ( 𝐺 − 𝐸 ) ) = 2 ) → ¬ 2 ∥ ( 𝐻 − 𝐹 ) )
68 54 67 49 mpjaodan ⊢ ( 𝜑 → ¬ 2 ∥ ( 𝐻 − 𝐹 ) )
69 50 68 jca ⊢ ( 𝜑 → ( 𝐹 < 𝐻 ∧ ¬ 2 ∥ ( 𝐻 − 𝐹 ) ) )