Theorem line2ylem 48877

Description: Lemma for line2y 48881. This proof is based on counterexamples for the following cases: 1. 𝐶 ≠ 0: p = (0,0) (LHS of biconditional is false, RHS is true); 2. 𝐶 = 0 ∧ 𝐵 ≠ 0: p = (1,-A/B) (LHS of biconditional is true, RHS is false); 3. 𝐴 = 𝐵 = 𝐶 = 0: p = (1,1) (LHS of biconditional is true, RHS is false). (Contributed by AV, 4-Feb-2023.)

Hypotheses

Ref	Expression
line2ylem.i	⊢ 𝐼 = {1, 2}
line2ylem.p	⊢ 𝑃 = (ℝ ↑m 𝐼)

Assertion

Ref	Expression
line2ylem	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Distinct variable groups:   𝐴,𝑝   𝐵,𝑝   𝐶,𝑝   𝑃,𝑝

Allowed substitution hint:   𝐼(𝑝)

Proof of Theorem line2ylem

Step	Hyp	Ref	Expression
1		ianor 983	. . . . 5 ⊢ (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) ↔ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0))
2		df-ne 2930	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
3		0re 11121	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
4		line2ylem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = {1, 2}
5		line2ylem.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (ℝ ↑m 𝐼)
6	4, 5	prelrrx2 48839	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃)
7	3, 3, 6	mp2an 692	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃
8		eqneqall 2940	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 ≠ 0 → ¬ 0 = 0))
9	8	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 → ¬ 0 = 0))
10		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ 0 = 0
11	10	pm2.24i 150	. . . . . . . . . . . . . . 15 ⊢ (¬ 0 = 0 → 𝐶 = 0)
12	9, 11	impbid1 225	. . . . . . . . . . . . . 14 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 ↔ ¬ 0 = 0))
13	12	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (𝐶 = 0 ↔ ¬ 0 = 0))
14		xor3 382	. . . . . . . . . . . . 13 ⊢ (¬ (𝐶 = 0 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ ¬ 0 = 0))
15	13, 14	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (𝐶 = 0 ↔ 0 = 0))
16		simp1 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
17	16	recnd 11147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
18	17	mul01d 11319	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 0) = 0)
19		simp2 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
20	19	recnd 11147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
21	20	mul01d 11319	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 0) = 0)
22	18, 21	oveq12d 7370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = (0 + 0))
23		00id 11295	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 0) = 0
24	22, 23	eqtrdi 2784	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = 0)
25	24	eqeq1d 2735	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 𝐶))
26		eqcom 2740	. . . . . . . . . . . . . . 15 ⊢ (0 = 𝐶 ↔ 𝐶 = 0)
27	25, 26	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
28	27	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 𝐶 = 0))
29	28	bibi1d 343	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ((((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0) ↔ (𝐶 = 0 ↔ 0 = 0)))
30	15, 29	mtbird 325	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0))
31		fveq1 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1))
32		1ex 11115	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ V
33		c0ex 11113	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ V
34		1ne2 12335	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≠ 2
35		fvpr1g 7130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0)
36	32, 33, 34, 35	mp3an 1463	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0
37	31, 36	eqtrdi 2784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = 0)
38	37	oveq2d 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 0))
39		fveq1 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2))
40		2ex 12209	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ V
41		fvpr2g 7131	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ V ∧ 0 ∈ V ∧ 1 ≠ 2) → ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0)
42	40, 33, 34, 41	mp3an 1463	. . . . . . . . . . . . . . . . . 18 ⊢ ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0
43	39, 42	eqtrdi 2784	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = 0)
44	43	oveq2d 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 0))
45	38, 44	oveq12d 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 0) + (𝐵 · 0)))
46	45	eqeq1d 2735	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 0) + (𝐵 · 0)) = 𝐶))
47	37	eqeq1d 2735	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝑝‘1) = 0 ↔ 0 = 0))
48	46, 47	bibi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
49	48	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)))
50	49	rspcev 3573	. . . . . . . . . . 11 ⊢ (({⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
51	7, 30, 50	sylancr 587	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐶 ≠ 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
52	51	expcom 413	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
53	2, 52	sylbir 235	. . . . . . . 8 ⊢ (¬ 𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
54		notnotb 315	. . . . . . . . . 10 ⊢ (𝐶 = 0 ↔ ¬ ¬ 𝐶 = 0)
55		ianor 983	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ↔ (¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0))
56		df-ne 2930	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
57		1red 11120	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 1 ∈ ℝ)
58	16	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐴 ∈ ℝ)
59	58	renegcld 11551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℝ)
60	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℝ)
61		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ≠ 0)
62	59, 60, 61	redivcld 11956	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (-𝐴 / 𝐵) ∈ ℝ)
63	4, 5	prelrrx2 48839	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ (-𝐴 / 𝐵) ∈ ℝ) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
64	57, 62, 63	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
65		ax-1ne0 11082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
66	65	neii 2931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ¬ 1 = 0
67	10, 66	2th 264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 = 0 ↔ ¬ 1 = 0)
68		xor3 382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (0 = 0 ↔ 1 = 0) ↔ (0 = 0 ↔ ¬ 1 = 0))
69	67, 68	mpbir 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ (0 = 0 ↔ 1 = 0)
70	17	mulridd 11136	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 1) = 𝐴)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 · 1) = 𝐴)
72	17	negcld 11466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℂ)
74	20	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℂ)
75	73, 74, 61	divcan2d 11906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐵 · (-𝐴 / 𝐵)) = -𝐴)
76	71, 75	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = (𝐴 + -𝐴))
77	17	negidd 11469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + -𝐴) = 0)
78	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 + -𝐴) = 0)
79	76, 78	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 0)
80		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐶 = 0)
81	79, 80	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 0 = 0))
82	81	bibi1d 343	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
83	69, 82	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0))
84		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1))
85		fvpr1g 7130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1)
86	32, 32, 34, 85	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1) = 1
87	84, 86	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = 1)
88	87	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
89		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2))
90		ovex 7385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (-𝐴 / 𝐵) ∈ V
91		fvpr2g 7131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ (-𝐴 / 𝐵) ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵))
92	40, 90, 34, 91	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2) = (-𝐴 / 𝐵)
93	89, 92	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = (-𝐴 / 𝐵))
94	93	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · (-𝐴 / 𝐵)))
95	88, 94	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))))
96	95	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶))
97	87	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
98	96, 97	bibi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
99	98	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)))
100	99	rspcev 3573	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
101	64, 83, 100	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
102	101	expcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ≠ 0 ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
103	102	ex 412	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
104	56, 103	sylbir 235	. . . . . . . . . . . . . 14 ⊢ (¬ 𝐵 = 0 → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
105		notnotb 315	. . . . . . . . . . . . . . 15 ⊢ (𝐵 = 0 ↔ ¬ ¬ 𝐵 = 0)
106		nne 2933	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝐴 ≠ 0 ↔ 𝐴 = 0)
107	106	bicomi 224	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 ↔ ¬ 𝐴 ≠ 0)
108		1re 11119	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
109	4, 5	prelrrx2 48839	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ) → {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃)
110	108, 108, 109	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃
111		oveq1 7359	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = 0 → (𝐴 · 1) = (0 · 1))
112	111	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = (0 · 1))
113		ax-1cn 11071	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
114	113	mul02i 11309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 · 1) = 0
115	112, 114	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = 0)
116		oveq1 7359	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 = 0 → (𝐵 · 1) = (0 · 1))
117	116	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = (0 · 1))
118	117, 114	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = 0)
119	115, 118	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = (0 + 0))
120	119, 23	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = 0)
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 = 0 → 𝐶 = 0)
122	120, 121	eqeqan12d 2747	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 0 = 0))
123	122	bibi1d 343	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0) ↔ (0 = 0 ↔ 1 = 0)))
124	69, 123	mtbiri 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0))
125		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, 1⟩}‘1))
126		fvpr1g 7130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((1 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1)
127	32, 32, 34, 126	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘1) = 1
128	125, 127	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = 1)
129	128	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
130		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, 1⟩}‘2))
131		fvpr2g 7131	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ V ∧ 1 ∈ V ∧ 1 ≠ 2) → ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1)
132	40, 32, 34, 131	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨1, 1⟩, ⟨2, 1⟩}‘2) = 1
133	130, 132	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = 1)
134	133	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 1))
135	129, 134	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · 1)))
136	135	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · 1)) = 𝐶))
137	128	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝑝‘1) = 0 ↔ 1 = 0))
138	136, 137	bibi12d 345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
139	138	notbid 318	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)))
140	139	rspcev 3573	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃 ∧ ¬ (((𝐴 · 1) + (𝐵 · 1)) = 𝐶 ↔ 1 = 0)) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
141	110, 124, 140	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
142	141	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵 = 0 ∧ 𝐴 = 0) ∧ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
143	142	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
144	105, 107, 143	syl2anbr 599	. . . . . . . . . . . . . 14 ⊢ ((¬ ¬ 𝐵 = 0 ∧ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
145	104, 144	jaoi3 1060	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
146	145	orcoms 872	. . . . . . . . . . . 12 ⊢ ((¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
147	55, 146	sylbi 217	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
148	147	com12 32	. . . . . . . . . 10 ⊢ (𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
149	54, 148	sylbir 235	. . . . . . . . 9 ⊢ (¬ ¬ 𝐶 = 0 → (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
150	149	imp 406	. . . . . . . 8 ⊢ ((¬ ¬ 𝐶 = 0 ∧ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
151	53, 150	jaoi3 1060	. . . . . . 7 ⊢ ((¬ 𝐶 = 0 ∨ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
152	151	orcoms 872	. . . . . 6 ⊢ ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
153	152	com12 32	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
154	1, 153	biimtrid 242	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
155		rexnal 3085	. . . 4 ⊢ (∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) ↔ ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))
156	154, 155	imbitrdi 251	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) → ¬ ∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
157	156	con4d 115	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0)))
158		df-3an 1088	. 2 ⊢ ((𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0) ↔ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0))
159	157, 158	imbitrrdi 252	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (∀𝑝 ∈ 𝑃 (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0) → (𝐴 ≠ 0 ∧ 𝐵 = 0 ∧ 𝐶 = 0)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  Vcvv 3437  {cpr 4577  ⟨cop 4581  ‘cfv 6486  (class class class)co 7352   ↑_m cmap 8756  ℂcc 11011  ℝcr 11012  0cc0 11013  1c1 11014   + caddc 11016   · cmul 11018  -cneg 11352   / cdiv 11781  2c2 12187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-map 8758  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-div 11782  df-2 12195

This theorem is referenced by:  line2y  48881