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 
|- I = ( 0 ..^ 2 )
line2.e 
|- E = ( RR^ ` I )
line2.p 
|- P = ( RR ^m I )
line2.l 
|- L = ( LineM ` E )
line2.g 
|- G = { p e. P | ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C }
line2x.x 
|- X = <" 0 M ">
line2x.y 
|- Y = <" 1 M ">
Assertion line2xlem 
|- ( ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) /\ C e. RR ) /\ M e. RR ) -> ( A. p e. P ( ( ( A x. ( p ` 0 ) ) + ( B x. ( p ` 1 ) ) ) = C <-> ( p ` 1 ) = M ) -> ( A = 0 /\ M = ( C / B ) ) ) )

Proof

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