Metamath Proof Explorer

Theorem line2xlem

Description: Lemma for line2x . This proof is based on counterexamples for the following cases: 1. M =/= ( C / B ) : p = (0,C/B) (LHS of biconditional is true, RHS is false); 2. A =/= 0 /\ M = ( C / B ) : p = (1,C/B) (LHS of biconditional is false, RHS is true). (Contributed by AV, 4-Feb-2023)

Ref Expression
Hypotheses line2.i ⊢ 𝐼 = ( 0 ..^ 2 )
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 }
line2x.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
line2x.y ⊢ 𝑌 = ⟨“ 1 𝑀 ”⟩
Assertion line2xlem ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 line2.i ⊢ 𝐼 = ( 0 ..^ 2 )
2 line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
3 line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
4 line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
5 line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 }
6 line2x.x ⊢ 𝑋 = ⟨“ 0 𝑀 ”⟩
7 line2x.y ⊢ 𝑌 = ⟨“ 1 𝑀 ”⟩
8 ianor ⊢ ( ¬ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ↔ ( ¬ 𝐴 = 0 ∨ ¬ 𝑀 = ( 𝐶 / 𝐵 ) ) )
9 df-ne ⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
10 df-ne ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ↔ ¬ 𝑀 = ( 𝐶 / 𝐵 ) )
11 9 10 orbi12i ⊢ ( ( 𝐴 ≠ 0 ∨ 𝑀 ≠ ( 𝐶 / 𝐵 ) ) ↔ ( ¬ 𝐴 = 0 ∨ ¬ 𝑀 = ( 𝐶 / 𝐵 ) ) )
12 8 11 bitr4i ⊢ ( ¬ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ↔ ( 𝐴 ≠ 0 ∨ 𝑀 ≠ ( 𝐶 / 𝐵 ) ) )
13 fveq1 ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) )
14 13 oveq2d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) )
15 fveq1 ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) )
16 15 oveq2d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) )
17 14 16 oveq12d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) )
18 17 eqeq1d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ) )
19 15 eqeq1d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( ( 𝑝 ‘ 1 ) = 𝑀 ↔ ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) )
20 18 19 bibi12d ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ( ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ) )
21 20 notbid ⊢ ( 𝑝 = ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ¬ ( ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ) )
22 0red ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → 0 ∈ ℝ )
23 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
24 23 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐶 ∈ ℝ )
25 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℝ )
26 25 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
27 26 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐵 ∈ ℝ )
28 simp2r ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ≠ 0 )
29 28 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐵 ≠ 0 )
30 24 27 29 redivcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
31 30 adantl ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
32 1 3 prelrrx2 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) → ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ∈ 𝑃 )
33 22 31 32 syl2anc ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ∈ 𝑃 )
34 id ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → 𝑀 ≠ ( 𝐶 / 𝐵 ) )
35 34 necomd ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ( 𝐶 / 𝐵 ) ≠ 𝑀 )
36 35 neneqd ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ¬ ( 𝐶 / 𝐵 ) = 𝑀 )
37 36 a1d ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ( 𝐶 = 𝐶 → ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
38 eqidd ⊢ ( ¬ ( 𝐶 / 𝐵 ) = 𝑀 → 𝐶 = 𝐶 )
39 37 38 impbid1 ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ( 𝐶 = 𝐶 ↔ ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
40 xor3 ⊢ ( ¬ ( 𝐶 = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ↔ ( 𝐶 = 𝐶 ↔ ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
41 39 40 sylibr ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ¬ ( 𝐶 = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
42 41 adantr ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ¬ ( 𝐶 = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
43 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 0 ∈ ℝ )
44 s2fv0 ⊢ ( 0 ∈ ℝ → ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) = 0 )
45 43 44 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) = 0 )
46 45 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) = ( 𝐴 · 0 ) )
47 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
48 47 mul01d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
49 48 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
50 49 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · 0 ) = 0 )
51 46 50 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) = 0 )
52 ovexd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ V )
53 s2fv1 ⊢ ( ( 𝐶 / 𝐵 ) ∈ V → ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = ( 𝐶 / 𝐵 ) )
54 52 53 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = ( 𝐶 / 𝐵 ) )
55 54 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) = ( 𝐵 · ( 𝐶 / 𝐵 ) ) )
56 23 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
57 56 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐶 ∈ ℂ )
58 25 recnd ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 𝐵 ∈ ℂ )
59 58 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
60 59 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → 𝐵 ∈ ℂ )
61 57 60 29 divcan2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐵 · ( 𝐶 / 𝐵 ) ) = 𝐶 )
62 55 61 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) = 𝐶 )
63 51 62 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = ( 0 + 𝐶 ) )
64 63 adantl ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = ( 0 + 𝐶 ) )
65 56 addlidd ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 0 + 𝐶 ) = 𝐶 )
66 65 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 0 + 𝐶 ) = 𝐶 )
67 66 adantl ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( 0 + 𝐶 ) = 𝐶 )
68 64 67 eqtrd ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 )
69 68 eqeq1d ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ 𝐶 = 𝐶 ) )
70 54 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
71 70 adantl ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
72 69 71 bibi12d ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ↔ ( 𝐶 = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ) )
73 42 72 mtbird ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ¬ ( ( ( 𝐴 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 0 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) )
74 21 33 73 rspcedvdw ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
75 74 ex ⊢ ( 𝑀 ≠ ( 𝐶 / 𝐵 ) → ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
76 nne ⊢ ( ¬ 𝑀 ≠ ( 𝐶 / 𝐵 ) ↔ 𝑀 = ( 𝐶 / 𝐵 ) )
77 fveq1 ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 0 ) = ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) )
78 77 oveq2d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝐴 · ( 𝑝 ‘ 0 ) ) = ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) )
79 fveq1 ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝑝 ‘ 1 ) = ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) )
80 79 oveq2d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( 𝐵 · ( 𝑝 ‘ 1 ) ) = ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) )
81 78 80 oveq12d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) )
82 81 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ) )
83 79 eqeq1d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( ( 𝑝 ‘ 1 ) = 𝑀 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) )
84 82 83 bibi12d ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ) )
85 84 notbid ⊢ ( 𝑝 = ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ → ( ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ¬ ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ) )
86 1red ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → 1 ∈ ℝ )
87 23 26 28 redivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
88 86 87 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 1 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) )
89 88 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 1 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) )
90 1 3 prelrrx2 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝐶 / 𝐵 ) ∈ ℝ ) → ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ∈ 𝑃 )
91 89 90 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ∈ 𝑃 )
92 91 adantl ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ∈ 𝑃 )
93 eqneqall ⊢ ( 𝐴 = 0 → ( 𝐴 ≠ 0 → ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
94 93 com12 ⊢ ( 𝐴 ≠ 0 → ( 𝐴 = 0 → ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
95 94 adantl ⊢ ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 = 0 → ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
96 pm2.24 ⊢ ( ( 𝐶 / 𝐵 ) = 𝑀 → ( ¬ ( 𝐶 / 𝐵 ) = 𝑀 → 𝐴 = 0 ) )
97 96 eqcoms ⊢ ( 𝑀 = ( 𝐶 / 𝐵 ) → ( ¬ ( 𝐶 / 𝐵 ) = 𝑀 → 𝐴 = 0 ) )
98 97 adantr ⊢ ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ( ¬ ( 𝐶 / 𝐵 ) = 𝑀 → 𝐴 = 0 ) )
99 95 98 impbid ⊢ ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 = 0 ↔ ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
100 xor3 ⊢ ( ¬ ( 𝐴 = 0 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ↔ ( 𝐴 = 0 ↔ ¬ ( 𝐶 / 𝐵 ) = 𝑀 ) )
101 99 100 sylibr ⊢ ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ¬ ( 𝐴 = 0 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
102 101 adantr ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ¬ ( 𝐴 = 0 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
103 simprl1 ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
104 103 recnd ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
105 24 adantl ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
106 105 recnd ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
107 104 106 addcomd ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( 𝐴 + 𝐶 ) = ( 𝐶 + 𝐴 ) )
108 107 eqeq1d ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 + 𝐴 ) = 𝐶 ) )
109 recn ⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
110 47 109 anim12ci ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
111 110 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
112 111 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
113 112 adantl ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) )
114 addid0 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝐶 + 𝐴 ) = 𝐶 ↔ 𝐴 = 0 ) )
115 113 114 syl ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐶 + 𝐴 ) = 𝐶 ↔ 𝐴 = 0 ) )
116 108 115 bitrd ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ 𝐴 = 0 ) )
117 116 bibi1d ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ↔ ( 𝐴 = 0 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ) )
118 102 117 mtbird ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ¬ ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
119 1re ⊢ 1 ∈ ℝ
120 s2fv0 ⊢ ( 1 ∈ ℝ → ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) = 1 )
121 119 120 mp1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) = 1 )
122 121 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) = ( 𝐴 · 1 ) )
123 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
124 123 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 · 1 ) = 𝐴 )
125 124 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · 1 ) = 𝐴 )
126 122 125 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) = 𝐴 )
127 s2fv1 ⊢ ( ( 𝐶 / 𝐵 ) ∈ V → ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = ( 𝐶 / 𝐵 ) )
128 52 127 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = ( 𝐶 / 𝐵 ) )
129 128 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) = ( 𝐵 · ( 𝐶 / 𝐵 ) ) )
130 129 61 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) = 𝐶 )
131 126 130 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = ( 𝐴 + 𝐶 ) )
132 131 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( 𝐴 + 𝐶 ) = 𝐶 ) )
133 128 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) )
134 132 133 bibi12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ↔ ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ) )
135 134 notbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ¬ ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ↔ ¬ ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ) )
136 135 adantl ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ( ¬ ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) ↔ ¬ ( ( 𝐴 + 𝐶 ) = 𝐶 ↔ ( 𝐶 / 𝐵 ) = 𝑀 ) ) )
137 118 136 mpbird ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ¬ ( ( ( 𝐴 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 0 ) ) + ( 𝐵 · ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) ) ) = 𝐶 ↔ ( ⟨“ 1 ( 𝐶 / 𝐵 ) ”⟩ ‘ 1 ) = 𝑀 ) )
138 85 92 137 rspcedvdw ⊢ ( ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) ∧ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
139 138 ex ⊢ ( ( 𝑀 = ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
140 76 139 sylanb ⊢ ( ( ¬ 𝑀 ≠ ( 𝐶 / 𝐵 ) ∧ 𝐴 ≠ 0 ) → ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
141 75 140 jaoi3 ⊢ ( ( 𝑀 ≠ ( 𝐶 / 𝐵 ) ∨ 𝐴 ≠ 0 ) → ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
142 141 orcoms ⊢ ( ( 𝐴 ≠ 0 ∨ 𝑀 ≠ ( 𝐶 / 𝐵 ) ) → ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
143 142 com12 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝑀 ≠ ( 𝐶 / 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
144 rexnal ⊢ ( ∃ 𝑝 ∈ 𝑃 ¬ ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ↔ ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) )
145 143 144 imbitrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ( 𝐴 ≠ 0 ∨ 𝑀 ≠ ( 𝐶 / 𝐵 ) ) → ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
146 12 145 biimtrid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ¬ ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) → ¬ ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) ) )
147 146 con4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 0 ) ) + ( 𝐵 · ( 𝑝 ‘ 1 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 1 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )