Metamath Proof Explorer

Theorem climuni

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999) (Proof shortened by Mario Carneiro, 31-Jan-2014)

Ref Expression
Assertion climuni ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ) → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
3 1zzd ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 1 ∈ ℤ )
4 climcl ⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
5 4 3ad2ant1 ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ℂ )
6 climcl ⊢ ( 𝐹 ⇝ 𝐵 → 𝐵 ∈ ℂ )
7 6 3ad2ant2 ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ℂ )
8 5 7 subcld ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
9 simp3 ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
10 5 7 9 subne0d ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 − 𝐵 ) ≠ 0 )
11 8 10 absrpcld ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ+ )
12 11 rphalfcld ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ∈ ℝ+ )
13 eqidd ⊢ ( ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
14 simp1 ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 𝐹 ⇝ 𝐴 )
15 2 3 12 13 14 climi ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) )
16 simp2 ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → 𝐹 ⇝ 𝐵 )
17 2 3 12 13 16 climi ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) )
18 2 rexanuz2 ⊢ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) ↔ ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) )
19 15 17 18 sylanbrc ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) )
20 nnz ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℤ )
21 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
22 ne0i ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑗 ) ≠ ∅ )
23 r19.2z ⊢ ( ( ( ℤ≥ ‘ 𝑗 ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) )
24 23 ex ⊢ ( ( ℤ≥ ‘ 𝑗 ) ≠ ∅ → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) ) )
25 20 21 22 24 4syl ⊢ ( 𝑗 ∈ ℕ → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) ) )
26 simpr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
27 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → 𝐴 ∈ ℂ )
28 26 27 abssubd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) )
29 28 breq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ↔ ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) )
30 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → 𝐵 ∈ ℂ )
31 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
32 31 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
33 32 abscld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
34 abs3lem ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( abs ‘ ( 𝐴 − 𝐵 ) ) ) )
35 27 30 26 33 34 syl22anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( abs ‘ ( 𝐴 − 𝐵 ) ) ) )
36 33 ltnrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ¬ ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( abs ‘ ( 𝐴 − 𝐵 ) ) )
37 36 pm2.21d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − 𝐵 ) ) < ( abs ‘ ( 𝐴 − 𝐵 ) ) → ¬ 1 ∈ ℤ ) )
38 35 37 syld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) → ¬ 1 ∈ ℤ ) )
39 38 expd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( 𝐴 − ( 𝐹 ‘ 𝑘 ) ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) ) )
40 29 39 sylbid ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) ) )
41 40 impr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) → ¬ 1 ∈ ℤ ) )
42 41 adantld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) → ¬ 1 ∈ ℤ ) )
43 42 expimpd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
44 43 rexlimdvw ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
45 25 44 sylan9r ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑗 ∈ ℕ ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
46 45 rexlimdva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
47 5 7 46 syl2anc ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑗 ∈ ℕ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ∧ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − 𝐵 ) ) < ( ( abs ‘ ( 𝐴 − 𝐵 ) ) / 2 ) ) ) → ¬ 1 ∈ ℤ ) )
48 19 47 mpd ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ¬ 1 ∈ ℤ )
49 48 3expia ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ) → ( 𝐴 ≠ 𝐵 → ¬ 1 ∈ ℤ ) )
50 49 necon4ad ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ) → ( 1 ∈ ℤ → 𝐴 = 𝐵 ) )
51 1 50 mpi ⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ 𝐵 ) → 𝐴 = 𝐵 )