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 ∥ ( 𝐻 − 𝐹 ) ) ) |