Theorem line2ylem 48672

Description: Lemma for line2y 48676. 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 984	. . . . 5 ⊢ (¬ ((𝐴 ≠ 0 ∧ 𝐵 = 0) ∧ 𝐶 = 0) ↔ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ∨ ¬ 𝐶 = 0))
2		df-ne 2941	. . . . . . . . 9 ⊢ (𝐶 ≠ 0 ↔ ¬ 𝐶 = 0)
3		0re 11263	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
4		line2ylem.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = {1, 2}
5		line2ylem.p	. . . . . . . . . . . . 13 ⊢ 𝑃 = (ℝ ↑m 𝐼)
6	4, 5	prelrrx2 48634	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 0 ∈ ℝ) → {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃)
7	3, 3, 6	mp2an 692	. . . . . . . . . . 11 ⊢ {⟨1, 0⟩, ⟨2, 0⟩} ∈ 𝑃
8		eqneqall 2951	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 = 0 → (𝐶 ≠ 0 → ¬ 0 = 0))
9	8	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ≠ 0 → (𝐶 = 0 → ¬ 0 = 0))
10		eqid 2737	. . . . . . . . . . . . . . . 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 1137	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
17	16	recnd 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
18	17	mul01d 11460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 0) = 0)
19		simp2 1138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
20	19	recnd 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
21	20	mul01d 11460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 0) = 0)
22	18, 21	oveq12d 7449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = (0 + 0))
23		00id 11436	. . . . . . . . . . . . . . . . 17 ⊢ (0 + 0) = 0
24	22, 23	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 · 0) + (𝐵 · 0)) = 0)
25	24	eqeq1d 2739	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (((𝐴 · 0) + (𝐵 · 0)) = 𝐶 ↔ 0 = 𝐶))
26		eqcom 2744	. . . . . . . . . . . . . . 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 6905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1))
32		1ex 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ V
33		c0ex 11255	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ V
34		1ne2 12474	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≠ 2
35		fvpr1g 7210	. . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘1) = 0)
38	37	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 0))
39		fveq1 6905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2))
40		2ex 12343	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ V
41		fvpr2g 7211	. . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝑝‘2) = 0)
44	43	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 0))
45	38, 44	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 0) + (𝐵 · 0)))
46	45	eqeq1d 2739	. . . . . . . . . . . . . 14 ⊢ (𝑝 = {⟨1, 0⟩, ⟨2, 0⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 0) + (𝐵 · 0)) = 𝐶))
47	37	eqeq1d 2739	. . . . . . . . . . . . . 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 3622	. . . . . . . . . . 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 984	. . . . . . . . . . . 12 ⊢ (¬ (𝐴 ≠ 0 ∧ 𝐵 = 0) ↔ (¬ 𝐴 ≠ 0 ∨ ¬ 𝐵 = 0))
56		df-ne 2941	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ≠ 0 ↔ ¬ 𝐵 = 0)
57		1red 11262	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 1 ∈ ℝ)
58	16	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐴 ∈ ℝ)
59	58	renegcld 11690	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℝ)
60	19	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℝ)
61		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ≠ 0)
62	59, 60, 61	redivcld 12095	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (-𝐴 / 𝐵) ∈ ℝ)
63	4, 5	prelrrx2 48634	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ (-𝐴 / 𝐵) ∈ ℝ) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
64	57, 62, 63	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} ∈ 𝑃)
65		ax-1ne0 11224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ≠ 0
66	65	neii 2942	. . . . . . . . . . . . . . . . . . . . 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 11278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 · 1) = 𝐴)
71	70	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 · 1) = 𝐴)
72	17	negcld 11607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → -𝐴 ∈ ℂ)
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → -𝐴 ∈ ℂ)
74	20	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐵 ∈ ℂ)
75	73, 74, 61	divcan2d 12045	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐵 · (-𝐴 / 𝐵)) = -𝐴)
76	71, 75	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = (𝐴 + -𝐴))
77	17	negidd 11610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + -𝐴) = 0)
78	77	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → (𝐴 + -𝐴) = 0)
79	76, 78	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 0)
80		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ (𝐵 ≠ 0 ∧ 𝐶 = 0)) → 𝐶 = 0)
81	79, 80	eqeq12d 2753	. . . . . . . . . . . . . . . . . . . 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 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘1))
85		fvpr1g 7210	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘1) = 1)
88	87	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
89		fveq1 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩}‘2))
90		ovex 7464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (-𝐴 / 𝐵) ∈ V
91		fvpr2g 7211	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝑝‘2) = (-𝐴 / 𝐵))
94	93	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · (-𝐴 / 𝐵)))
95	88, 94	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))))
96	95	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, (-𝐴 / 𝐵)⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · (-𝐴 / 𝐵))) = 𝐶))
97	87	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 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 3622	. . . . . . . . . . . . . . . . . 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 2944	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝐴 ≠ 0 ↔ 𝐴 = 0)
107	106	bicomi 224	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 0 ↔ ¬ 𝐴 ≠ 0)
108		1re 11261	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
109	4, 5	prelrrx2 48634	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 1 ∈ ℝ) → {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃)
110	108, 108, 109	mp2an 692	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨1, 1⟩, ⟨2, 1⟩} ∈ 𝑃
111		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = 0 → (𝐴 · 1) = (0 · 1))
112	111	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = (0 · 1))
113		ax-1cn 11213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℂ
114	113	mul02i 11450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0 · 1) = 0
115	112, 114	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐴 · 1) = 0)
116		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐵 = 0 → (𝐵 · 1) = (0 · 1))
117	116	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = (0 · 1))
118	117, 114	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → (𝐵 · 1) = 0)
119	115, 118	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = (0 + 0))
120	119, 23	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵 = 0 ∧ 𝐴 = 0) → ((𝐴 · 1) + (𝐵 · 1)) = 0)
121		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 = 0 → 𝐶 = 0)
122	120, 121	eqeqan12d 2751	. . . . . . . . . . . . . . . . . . . 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 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = ({⟨1, 1⟩, ⟨2, 1⟩}‘1))
126		fvpr1g 7210	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘1) = 1)
129	128	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐴 · (𝑝‘1)) = (𝐴 · 1))
130		fveq1 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = ({⟨1, 1⟩, ⟨2, 1⟩}‘2))
131		fvpr2g 7211	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝑝‘2) = 1)
134	133	oveq2d 7447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (𝐵 · (𝑝‘2)) = (𝐵 · 1))
135	129, 134	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → ((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = ((𝐴 · 1) + (𝐵 · 1)))
136	135	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = {⟨1, 1⟩, ⟨2, 1⟩} → (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ ((𝐴 · 1) + (𝐵 · 1)) = 𝐶))
137	128	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . 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 3622	. . . . . . . . . . . . . . . . . 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 1061	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐵 = 0 ∨ ¬ 𝐴 ≠ 0) → (𝐶 = 0 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0))))
146	145	orcoms 873	. . . . . . . . . . . 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 1061	. . . . . . 7 ⊢ ((¬ 𝐶 = 0 ∨ ¬ (𝐴 ≠ 0 ∧ 𝐵 = 0)) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ∃𝑝 ∈ 𝑃 ¬ (((𝐴 · (𝑝‘1)) + (𝐵 · (𝑝‘2))) = 𝐶 ↔ (𝑝‘1) = 0)))
152	151	orcoms 873	. . . . . 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 3100	. . . 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 1089	. 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 848   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3480  {cpr 4628  ⟨cop 4632  ‘cfv 6561  (class class class)co 7431   ↑_m cmap 8866  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  -cneg 11493   / cdiv 11920  2c2 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-2 12329

This theorem is referenced by:  line2y  48676