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 ⊢ 𝐼 = { 1 , 2 }
line2.e ⊢ 𝐸 = ( ℝ^ ‘ 𝐼 )
line2.p ⊢ 𝑃 = ( ℝ ↑m 𝐼 )
line2.l ⊢ 𝐿 = ( LineM ‘ 𝐸 )
line2.g ⊢ 𝐺 = { 𝑝 ∈ 𝑃 ∣ ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 }
line2x.x ⊢ 𝑋 = { ⟨ 1 , 0 ⟩ , ⟨ 2 , 𝑀 ⟩ }
line2x.y ⊢ 𝑌 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 𝑀 ⟩ }
Assertion line2xlem ( ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ∧ 𝐶 ∈ ℝ ) ∧ 𝑀 ∈ ℝ ) → ( ∀ 𝑝 ∈ 𝑃 ( ( ( 𝐴 · ( 𝑝 ‘ 1 ) ) + ( 𝐵 · ( 𝑝 ‘ 2 ) ) ) = 𝐶 ↔ ( 𝑝 ‘ 2 ) = 𝑀 ) → ( 𝐴 = 0 ∧ 𝑀 = ( 𝐶 / 𝐵 ) ) ) )

Proof

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