Metamath Proof Explorer

Theorem legtrid

Description: Trichotomy law for the less-than relationship. Proposition 5.10 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
legval.d ⊢ − = ( dist ‘ 𝐺 )
legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
Assertion legtrid ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 legval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 legval.d ⊢ − = ( dist ‘ 𝐺 )
3 legval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l ⊢ ≤ = ( ≤G ‘ 𝐺 )
5 legval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 legid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 legid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 legtrd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 legtrd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 5 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
11 6 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴 ∈ 𝑃 )
12 7 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ 𝑃 )
13 1 2 3 4 10 11 12 legid ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐴 − 𝐵 ) )
14 8 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐶 ∈ 𝑃 )
15 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
16 9 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐷 ∈ 𝑃 )
17 1 2 3 10 11 12 14 15 16 tgldim0cgr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) )
18 13 17 breqtrd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) )
19 18 orcd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) )
20 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐺 ∈ TarskiG )
21 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → 𝑥 ∈ 𝑃 )
22 21 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝑥 ∈ 𝑃 )
23 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐴 ∈ 𝑃 )
24 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐵 ∈ 𝑃 )
25 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝑦 ∈ 𝑃 )
26 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐴 ≠ 𝑥 )
27 26 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝑥 ≠ 𝐴 )
28 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) )
29 1 2 3 20 24 23 22 28 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝑥 𝐼 𝐵 ) )
30 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) )
31 1 3 20 22 23 24 25 27 29 30 tgbtwnconn2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) )
32 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) )
33 31 32 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ) → ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) )
34 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → 𝐺 ∈ TarskiG )
35 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → 𝐴 ∈ 𝑃 )
36 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → 𝐶 ∈ 𝑃 )
37 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → 𝐷 ∈ 𝑃 )
38 1 2 3 34 21 35 36 37 axtgsegcon ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝐴 ∈ ( 𝑥 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) )
39 33 38 reximddv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) )
40 39 adantllr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) )
41 5 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐺 ∈ TarskiG )
42 7 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐵 ∈ 𝑃 )
43 6 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐴 ∈ 𝑃 )
44 simpr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
45 1 2 3 41 42 43 44 tgbtwndiff ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝐴 ∈ ( 𝐵 𝐼 𝑥 ) ∧ 𝐴 ≠ 𝑥 ) )
46 40 45 r19.29a ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) )
47 andir ⊢ ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) )
48 eqcom ⊢ ( ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ↔ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) )
49 48 anbi2i ⊢ ( ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ↔ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) )
50 49 orbi2i ⊢ ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
51 47 50 bitri ⊢ ( ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ↔ ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
52 51 rexbii ⊢ ( ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ↔ ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
53 r19.43 ⊢ ( ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) ↔ ( ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
54 52 53 bitri ⊢ ( ∃ 𝑦 ∈ 𝑃 ( ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∨ 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ↔ ( ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
55 46 54 sylib ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
56 1 2 3 4 5 6 7 8 9 legov2 ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ) )
57 1 2 3 4 5 8 9 6 7 legov ⊢ ( 𝜑 → ( ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) )
58 56 57 orbi12d ⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) ↔ ( ∃ 𝑦 ∈ 𝑃 ( 𝐵 ∈ ( 𝐴 𝐼 𝑦 ) ∧ ( 𝐴 − 𝑦 ) = ( 𝐶 − 𝐷 ) ) ∨ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐴 𝐼 𝐵 ) ∧ ( 𝐶 − 𝐷 ) = ( 𝐴 − 𝑦 ) ) ) ) )
60 55 59 mpbird ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) )
61 1 6 tgldimor ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
62 19 60 61 mpjaodan ⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∨ ( 𝐶 − 𝐷 ) ≤ ( 𝐴 − 𝐵 ) ) )