ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  apreap GIF version

Theorem apreap 8317
Description: Complex apartness and real apartness agree on the real numbers. (Contributed by Jim Kingdon, 31-Jan-2020.)
Assertion
Ref Expression
apreap ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵𝐴 # 𝐵))

Proof of Theorem apreap
Dummy variables 𝑟 𝑠 𝑡 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqeq1 2124 . . . . . . . 8 (𝑥 = 𝐴 → (𝑥 = (𝑟 + (i · 𝑠)) ↔ 𝐴 = (𝑟 + (i · 𝑠))))
21anbi1d 460 . . . . . . 7 (𝑥 = 𝐴 → ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ↔ (𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢)))))
32anbi1d 460 . . . . . 6 (𝑥 = 𝐴 → (((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
432rexbidv 2437 . . . . 5 (𝑥 = 𝐴 → (∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
542rexbidv 2437 . . . 4 (𝑥 = 𝐴 → (∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
6 eqeq1 2124 . . . . . . . 8 (𝑦 = 𝐵 → (𝑦 = (𝑡 + (i · 𝑢)) ↔ 𝐵 = (𝑡 + (i · 𝑢))))
76anbi2d 459 . . . . . . 7 (𝑦 = 𝐵 → ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ↔ (𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢)))))
87anbi1d 460 . . . . . 6 (𝑦 = 𝐵 → (((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
982rexbidv 2437 . . . . 5 (𝑦 = 𝐵 → (∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
1092rexbidv 2437 . . . 4 (𝑦 = 𝐵 → (∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
11 df-ap 8312 . . . 4 # = {⟨𝑥, 𝑦⟩ ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))}
125, 10, 11brabg 4161 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵 ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
13 simplll 507 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) → 𝐴 ∈ ℝ)
1413adantr 274 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝐴 ∈ ℝ)
15 simplrl 509 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) → 𝑟 ∈ ℝ)
1615adantr 274 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑟 ∈ ℝ)
17 simplrr 510 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) → 𝑠 ∈ ℝ)
1817adantr 274 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑠 ∈ ℝ)
19 simprll 511 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝐴 = (𝑟 + (i · 𝑠)))
20 rereim 8316 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝑟 ∈ ℝ) ∧ (𝑠 ∈ ℝ ∧ 𝐴 = (𝑟 + (i · 𝑠)))) → (𝑟 = 𝐴𝑠 = 0))
2114, 16, 18, 19, 20syl22anc 1202 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → (𝑟 = 𝐴𝑠 = 0))
2221simprd 113 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑠 = 0)
23 simpllr 508 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) → 𝐵 ∈ ℝ)
2423adantr 274 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝐵 ∈ ℝ)
25 simplrl 509 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑡 ∈ ℝ)
26 simplrr 510 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑢 ∈ ℝ)
27 simprlr 512 . . . . . . . . . . . 12 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝐵 = (𝑡 + (i · 𝑢)))
28 rereim 8316 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ 𝑡 ∈ ℝ) ∧ (𝑢 ∈ ℝ ∧ 𝐵 = (𝑡 + (i · 𝑢)))) → (𝑡 = 𝐵𝑢 = 0))
2924, 25, 26, 27, 28syl22anc 1202 . . . . . . . . . . 11 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → (𝑡 = 𝐵𝑢 = 0))
3029simprd 113 . . . . . . . . . 10 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑢 = 0)
3122, 30eqtr4d 2153 . . . . . . . . 9 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑠 = 𝑢)
32 reapti 8309 . . . . . . . . . 10 ((𝑠 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑠 = 𝑢 ↔ ¬ 𝑠 # 𝑢))
3318, 26, 32syl2anc 408 . . . . . . . . 9 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → (𝑠 = 𝑢 ↔ ¬ 𝑠 # 𝑢))
3431, 33mpbid 146 . . . . . . . 8 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → ¬ 𝑠 # 𝑢)
35 simprr 506 . . . . . . . 8 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → (𝑟 # 𝑡𝑠 # 𝑢))
3634, 35ecased 1312 . . . . . . 7 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑟 # 𝑡)
3721simpld 111 . . . . . . 7 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑟 = 𝐴)
3829simpld 111 . . . . . . 7 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝑡 = 𝐵)
3936, 37, 383brtr3d 3929 . . . . . 6 (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) ∧ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))) → 𝐴 # 𝐵)
4039ex 114 . . . . 5 ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) ∧ (𝑡 ∈ ℝ ∧ 𝑢 ∈ ℝ)) → (((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) → 𝐴 # 𝐵))
4140rexlimdvva 2534 . . . 4 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝑟 ∈ ℝ ∧ 𝑠 ∈ ℝ)) → (∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) → 𝐴 # 𝐵))
4241rexlimdvva 2534 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) → 𝐴 # 𝐵))
4312, 42sylbid 149 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵𝐴 # 𝐵))
44 ax-icn 7683 . . . . . . . 8 i ∈ ℂ
4544mul01i 8121 . . . . . . 7 (i · 0) = 0
4645oveq2i 5753 . . . . . 6 (𝐴 + (i · 0)) = (𝐴 + 0)
47 simp1 966 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐴 ∈ ℝ)
4847recnd 7762 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐴 ∈ ℂ)
4948addid1d 7879 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (𝐴 + 0) = 𝐴)
5046, 49syl5req 2163 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐴 = (𝐴 + (i · 0)))
5145oveq2i 5753 . . . . . 6 (𝐵 + (i · 0)) = (𝐵 + 0)
52 simp2 967 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐵 ∈ ℝ)
5352recnd 7762 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐵 ∈ ℂ)
5453addid1d 7879 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (𝐵 + 0) = 𝐵)
5551, 54syl5req 2163 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐵 = (𝐵 + (i · 0)))
56 olc 685 . . . . . . 7 (𝐴 # 𝐵 → (0 # 0 ∨ 𝐴 # 𝐵))
57563ad2ant3 989 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (0 # 0 ∨ 𝐴 # 𝐵))
5857orcomd 703 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (𝐴 # 𝐵 ∨ 0 # 0))
5950, 55, 58jca31 307 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0)))
60 0red 7735 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 0 ∈ ℝ)
61 simpr 109 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → 𝑢 = 0)
6261oveq2d 5758 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → (i · 𝑢) = (i · 0))
6362oveq2d 5758 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → (𝐵 + (i · 𝑢)) = (𝐵 + (i · 0)))
6463eqeq2d 2129 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → (𝐵 = (𝐵 + (i · 𝑢)) ↔ 𝐵 = (𝐵 + (i · 0))))
6564anbi2d 459 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ↔ (𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0)))))
6661breq2d 3911 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → (0 # 𝑢 ↔ 0 # 0))
6766orbi2d 764 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → ((𝐴 # 𝐵 ∨ 0 # 𝑢) ↔ (𝐴 # 𝐵 ∨ 0 # 0)))
6865, 67anbi12d 464 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑢 = 0) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ∧ (𝐴 # 𝐵 ∨ 0 # 𝑢)) ↔ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0))))
6960, 68rspcedv 2767 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0)) → ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ∧ (𝐴 # 𝐵 ∨ 0 # 𝑢))))
70 simpr 109 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → 𝑡 = 𝐵)
7170oveq1d 5757 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → (𝑡 + (i · 𝑢)) = (𝐵 + (i · 𝑢)))
7271eqeq2d 2129 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → (𝐵 = (𝑡 + (i · 𝑢)) ↔ 𝐵 = (𝐵 + (i · 𝑢))))
7372anbi2d 459 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ↔ (𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢)))))
7470breq2d 3911 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → (𝐴 # 𝑡𝐴 # 𝐵))
7574orbi1d 765 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → ((𝐴 # 𝑡 ∨ 0 # 𝑢) ↔ (𝐴 # 𝐵 ∨ 0 # 𝑢)))
7673, 75anbi12d 464 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢)) ↔ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ∧ (𝐴 # 𝐵 ∨ 0 # 𝑢))))
7776rexbidv 2415 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑡 = 𝐵) → (∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢)) ↔ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ∧ (𝐴 # 𝐵 ∨ 0 # 𝑢))))
7852, 77rspcedv 2767 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 𝑢))) ∧ (𝐴 # 𝐵 ∨ 0 # 𝑢)) → ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢))))
7969, 78syld 45 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0)) → ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢))))
80 simpr 109 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → 𝑠 = 0)
8180oveq2d 5758 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (i · 𝑠) = (i · 0))
8281oveq2d 5758 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (𝐴 + (i · 𝑠)) = (𝐴 + (i · 0)))
8382eqeq2d 2129 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (𝐴 = (𝐴 + (i · 𝑠)) ↔ 𝐴 = (𝐴 + (i · 0))))
8483anbi1d 460 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ↔ (𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢)))))
8580breq1d 3909 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (𝑠 # 𝑢 ↔ 0 # 𝑢))
8685orbi2d 764 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → ((𝐴 # 𝑡𝑠 # 𝑢) ↔ (𝐴 # 𝑡 ∨ 0 # 𝑢)))
8784, 86anbi12d 464 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢)) ↔ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢))))
88872rexbidv 2437 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑠 = 0) → (∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢))))
8960, 88rspcedv 2767 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡 ∨ 0 # 𝑢)) → ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢))))
90 simpr 109 . . . . . . . . . . . . 13 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → 𝑟 = 𝐴)
9190oveq1d 5757 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (𝑟 + (i · 𝑠)) = (𝐴 + (i · 𝑠)))
9291eqeq2d 2129 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (𝐴 = (𝑟 + (i · 𝑠)) ↔ 𝐴 = (𝐴 + (i · 𝑠))))
9392anbi1d 460 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ↔ (𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢)))))
9490breq1d 3909 . . . . . . . . . . 11 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (𝑟 # 𝑡𝐴 # 𝑡))
9594orbi1d 765 . . . . . . . . . 10 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → ((𝑟 # 𝑡𝑠 # 𝑢) ↔ (𝐴 # 𝑡𝑠 # 𝑢)))
9693, 95anbi12d 464 . . . . . . . . 9 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢))))
9796rexbidv 2415 . . . . . . . 8 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢))))
98972rexbidv 2437 . . . . . . 7 (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) ∧ 𝑟 = 𝐴) → (∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢)) ↔ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢))))
9947, 98rspcedv 2767 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝐴 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝐴 # 𝑡𝑠 # 𝑢)) → ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
10079, 89, 993syld 57 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0)) → ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
101123adant3 986 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (𝐴 # 𝐵 ↔ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝐴 = (𝑟 + (i · 𝑠)) ∧ 𝐵 = (𝑡 + (i · 𝑢))) ∧ (𝑟 # 𝑡𝑠 # 𝑢))))
102100, 101sylibrd 168 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → (((𝐴 = (𝐴 + (i · 0)) ∧ 𝐵 = (𝐵 + (i · 0))) ∧ (𝐴 # 𝐵 ∨ 0 # 0)) → 𝐴 # 𝐵))
10359, 102mpd 13 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 # 𝐵) → 𝐴 # 𝐵)
1041033expia 1168 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵𝐴 # 𝐵))
10543, 104impbid 128 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 # 𝐵𝐴 # 𝐵))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 682  w3a 947   = wceq 1316  wcel 1465  wrex 2394   class class class wbr 3899  (class class class)co 5742  cr 7587  0cc0 7588  ici 7590   + caddc 7591   · cmul 7593   # creap 8304   # cap 8311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rab 2402  df-v 2662  df-sbc 2883  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-id 4185  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-iota 5058  df-fun 5095  df-fv 5101  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-pnf 7770  df-mnf 7771  df-ltxr 7773  df-sub 7903  df-neg 7904  df-reap 8305  df-ap 8312
This theorem is referenced by:  reaplt  8318  apreim  8333  apirr  8335  apti  8352  recexap  8382  rerecclap  8458
  Copyright terms: Public domain W3C validator