Metamath Proof Explorer

Theorem fourierdlem35

Description: There is a single point in ( A (,] B ) that's distant from X a multiple integer of T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem35.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem35.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem35.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
fourierdlem35.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem35.5 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
fourierdlem35.i ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
fourierdlem35.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
fourierdlem35.iel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
fourierdlem35.jel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
Assertion fourierdlem35 ( 𝜑 → 𝐼 = 𝐽 )

Proof

Step Hyp Ref Expression
1 fourierdlem35.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fourierdlem35.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 fourierdlem35.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 fourierdlem35.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
5 fourierdlem35.5 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6 fourierdlem35.i ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
7 fourierdlem35.j ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
8 fourierdlem35.iel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
9 fourierdlem35.jel ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
10 neqne ⊢ ( ¬ 𝐼 = 𝐽 → 𝐼 ≠ 𝐽 )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐴 ∈ ℝ )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐵 ∈ ℝ )
13 3 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐴 < 𝐵 )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝑋 ∈ ℝ )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐼 ∈ ℤ )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐽 ∈ ℤ )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐼 < 𝐽 )
18 iocssicc ⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
19 18 8 sselid ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
21 18 9 sselid ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
23 11 12 13 4 14 15 16 17 20 22 fourierdlem6 ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐽 = ( 𝐼 + 1 ) )
24 23 orcd ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
25 24 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ 𝐼 < 𝐽 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
26 simpll ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → 𝜑 )
27 7 zred ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
28 26 27 syl ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → 𝐽 ∈ ℝ )
29 6 zred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
30 26 29 syl ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → 𝐼 ∈ ℝ )
31 id ⊢ ( 𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽 )
32 31 necomd ⊢ ( 𝐼 ≠ 𝐽 → 𝐽 ≠ 𝐼 )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → 𝐽 ≠ 𝐼 )
34 simpr ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → ¬ 𝐼 < 𝐽 )
35 28 30 33 34 lttri5d ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → 𝐽 < 𝐼 )
36 1 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐴 ∈ ℝ )
37 2 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐵 ∈ ℝ )
38 3 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐴 < 𝐵 )
39 5 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝑋 ∈ ℝ )
40 7 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐽 ∈ ℤ )
41 6 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐼 ∈ ℤ )
42 simpr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐽 < 𝐼 )
43 21 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
44 19 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
45 36 37 38 4 39 40 41 42 43 44 fourierdlem6 ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐼 = ( 𝐽 + 1 ) )
46 45 olcd ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
47 26 35 46 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) ∧ ¬ 𝐼 < 𝐽 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
48 25 47 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐼 ≠ 𝐽 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
49 10 48 sylan2 ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝐽 ) → ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
50 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
51 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
52 iocleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ≤ 𝐵 )
53 50 51 9 52 syl3anc ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ≤ 𝐵 )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ≤ 𝐵 )
55 1 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝐴 ∈ ℝ )
56 2 1 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
57 4 56 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
58 29 57 remulcld ⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℝ )
59 5 58 readdcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ℝ )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ℝ )
61 57 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝑇 ∈ ℝ )
62 iocgtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
63 50 51 8 62 syl3anc ⊢ ( 𝜑 → 𝐴 < ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝐴 < ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
65 55 60 61 64 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝐴 + 𝑇 ) < ( ( 𝑋 + ( 𝐼 · 𝑇 ) ) + 𝑇 ) )
66 4 eqcomi ⊢ ( 𝐵 − 𝐴 ) = 𝑇
67 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
68 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
69 57 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
70 67 68 69 subaddd ⊢ ( 𝜑 → ( ( 𝐵 − 𝐴 ) = 𝑇 ↔ ( 𝐴 + 𝑇 ) = 𝐵 ) )
71 66 70 mpbii ⊢ ( 𝜑 → ( 𝐴 + 𝑇 ) = 𝐵 )
72 71 eqcomd ⊢ ( 𝜑 → 𝐵 = ( 𝐴 + 𝑇 ) )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝐵 = ( 𝐴 + 𝑇 ) )
74 5 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
75 58 recnd ⊢ ( 𝜑 → ( 𝐼 · 𝑇 ) ∈ ℂ )
76 74 75 69 addassd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐼 · 𝑇 ) ) + 𝑇 ) = ( 𝑋 + ( ( 𝐼 · 𝑇 ) + 𝑇 ) ) )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( ( 𝑋 + ( 𝐼 · 𝑇 ) ) + 𝑇 ) = ( 𝑋 + ( ( 𝐼 · 𝑇 ) + 𝑇 ) ) )
78 29 recnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
79 78 69 adddirp1d ⊢ ( 𝜑 → ( ( 𝐼 + 1 ) · 𝑇 ) = ( ( 𝐼 · 𝑇 ) + 𝑇 ) )
80 79 eqcomd ⊢ ( 𝜑 → ( ( 𝐼 · 𝑇 ) + 𝑇 ) = ( ( 𝐼 + 1 ) · 𝑇 ) )
81 80 oveq2d ⊢ ( 𝜑 → ( 𝑋 + ( ( 𝐼 · 𝑇 ) + 𝑇 ) ) = ( 𝑋 + ( ( 𝐼 + 1 ) · 𝑇 ) ) )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( ( 𝐼 · 𝑇 ) + 𝑇 ) ) = ( 𝑋 + ( ( 𝐼 + 1 ) · 𝑇 ) ) )
83 oveq1 ⊢ ( 𝐽 = ( 𝐼 + 1 ) → ( 𝐽 · 𝑇 ) = ( ( 𝐼 + 1 ) · 𝑇 ) )
84 83 eqcomd ⊢ ( 𝐽 = ( 𝐼 + 1 ) → ( ( 𝐼 + 1 ) · 𝑇 ) = ( 𝐽 · 𝑇 ) )
85 84 oveq2d ⊢ ( 𝐽 = ( 𝐼 + 1 ) → ( 𝑋 + ( ( 𝐼 + 1 ) · 𝑇 ) ) = ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
86 85 adantl ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( ( 𝐼 + 1 ) · 𝑇 ) ) = ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
87 77 82 86 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) = ( ( 𝑋 + ( 𝐼 · 𝑇 ) ) + 𝑇 ) )
88 65 73 87 3brtr4d ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝐵 < ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
89 2 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → 𝐵 ∈ ℝ )
90 27 57 remulcld ⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℝ )
91 5 90 readdcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ℝ )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ℝ )
93 89 92 ltnled ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ( 𝐵 < ( 𝑋 + ( 𝐽 · 𝑇 ) ) ↔ ¬ ( 𝑋 + ( 𝐽 · 𝑇 ) ) ≤ 𝐵 ) )
94 88 93 mpbid ⊢ ( ( 𝜑 ∧ 𝐽 = ( 𝐼 + 1 ) ) → ¬ ( 𝑋 + ( 𝐽 · 𝑇 ) ) ≤ 𝐵 )
95 54 94 pm2.65da ⊢ ( 𝜑 → ¬ 𝐽 = ( 𝐼 + 1 ) )
96 iocleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ≤ 𝐵 )
97 50 51 8 96 syl3anc ⊢ ( 𝜑 → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ≤ 𝐵 )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ≤ 𝐵 )
99 1 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝐴 ∈ ℝ )
100 91 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ℝ )
101 57 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝑇 ∈ ℝ )
102 iocgtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑋 + ( 𝐽 · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ) → 𝐴 < ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
103 50 51 9 102 syl3anc ⊢ ( 𝜑 → 𝐴 < ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
104 103 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝐴 < ( 𝑋 + ( 𝐽 · 𝑇 ) ) )
105 99 100 101 104 ltadd1dd ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝐴 + 𝑇 ) < ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) + 𝑇 ) )
106 72 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝐵 = ( 𝐴 + 𝑇 ) )
107 90 recnd ⊢ ( 𝜑 → ( 𝐽 · 𝑇 ) ∈ ℂ )
108 74 107 69 addassd ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) + 𝑇 ) = ( 𝑋 + ( ( 𝐽 · 𝑇 ) + 𝑇 ) ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) + 𝑇 ) = ( 𝑋 + ( ( 𝐽 · 𝑇 ) + 𝑇 ) ) )
110 27 recnd ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
111 110 69 adddirp1d ⊢ ( 𝜑 → ( ( 𝐽 + 1 ) · 𝑇 ) = ( ( 𝐽 · 𝑇 ) + 𝑇 ) )
112 111 eqcomd ⊢ ( 𝜑 → ( ( 𝐽 · 𝑇 ) + 𝑇 ) = ( ( 𝐽 + 1 ) · 𝑇 ) )
113 112 oveq2d ⊢ ( 𝜑 → ( 𝑋 + ( ( 𝐽 · 𝑇 ) + 𝑇 ) ) = ( 𝑋 + ( ( 𝐽 + 1 ) · 𝑇 ) ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( ( 𝐽 · 𝑇 ) + 𝑇 ) ) = ( 𝑋 + ( ( 𝐽 + 1 ) · 𝑇 ) ) )
115 oveq1 ⊢ ( 𝐼 = ( 𝐽 + 1 ) → ( 𝐼 · 𝑇 ) = ( ( 𝐽 + 1 ) · 𝑇 ) )
116 115 eqcomd ⊢ ( 𝐼 = ( 𝐽 + 1 ) → ( ( 𝐽 + 1 ) · 𝑇 ) = ( 𝐼 · 𝑇 ) )
117 116 oveq2d ⊢ ( 𝐼 = ( 𝐽 + 1 ) → ( 𝑋 + ( ( 𝐽 + 1 ) · 𝑇 ) ) = ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( ( 𝐽 + 1 ) · 𝑇 ) ) = ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
119 109 114 118 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) = ( ( 𝑋 + ( 𝐽 · 𝑇 ) ) + 𝑇 ) )
120 105 106 119 3brtr4d ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝐵 < ( 𝑋 + ( 𝐼 · 𝑇 ) ) )
121 2 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → 𝐵 ∈ ℝ )
122 59 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝑋 + ( 𝐼 · 𝑇 ) ) ∈ ℝ )
123 121 122 ltnled ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ( 𝐵 < ( 𝑋 + ( 𝐼 · 𝑇 ) ) ↔ ¬ ( 𝑋 + ( 𝐼 · 𝑇 ) ) ≤ 𝐵 ) )
124 120 123 mpbid ⊢ ( ( 𝜑 ∧ 𝐼 = ( 𝐽 + 1 ) ) → ¬ ( 𝑋 + ( 𝐼 · 𝑇 ) ) ≤ 𝐵 )
125 98 124 pm2.65da ⊢ ( 𝜑 → ¬ 𝐼 = ( 𝐽 + 1 ) )
126 95 125 jca ⊢ ( 𝜑 → ( ¬ 𝐽 = ( 𝐼 + 1 ) ∧ ¬ 𝐼 = ( 𝐽 + 1 ) ) )
127 126 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝐽 ) → ( ¬ 𝐽 = ( 𝐼 + 1 ) ∧ ¬ 𝐼 = ( 𝐽 + 1 ) ) )
128 pm4.56 ⊢ ( ( ¬ 𝐽 = ( 𝐼 + 1 ) ∧ ¬ 𝐼 = ( 𝐽 + 1 ) ) ↔ ¬ ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
129 127 128 sylib ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝐽 ) → ¬ ( 𝐽 = ( 𝐼 + 1 ) ∨ 𝐼 = ( 𝐽 + 1 ) ) )
130 49 129 condan ⊢ ( 𝜑 → 𝐼 = 𝐽 )