![]() |
Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > i2linesd | Structured version Visualization version GIF version |
Description: Solve for the intersection of two lines expressed in Y = MX+B form (note that the lines cannot be vertical). Here we use deduction form. We just solve for X, since Y can be trivially found by using X. This is an example of how to use the algebra helpers. Notice that because this proof uses algebra helpers, the main steps of the proof are higher level and easier to follow by a human reader. (Contributed by David A. Wheeler, 15-Oct-2018.) |
Ref | Expression |
---|---|
i2linesd.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
i2linesd.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
i2linesd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
i2linesd.4 | ⊢ (𝜑 → 𝐷 ∈ ℂ) |
i2linesd.5 | ⊢ (𝜑 → 𝑋 ∈ ℂ) |
i2linesd.6 | ⊢ (𝜑 → 𝑌 = ((𝐴 · 𝑋) + 𝐵)) |
i2linesd.7 | ⊢ (𝜑 → 𝑌 = ((𝐶 · 𝑋) + 𝐷)) |
i2linesd.8 | ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0) |
Ref | Expression |
---|---|
i2linesd | ⊢ (𝜑 → 𝑋 = ((𝐷 − 𝐵) / (𝐴 − 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | i2linesd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | i2linesd.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
3 | 1, 2 | subcld 10792 | . 2 ⊢ (𝜑 → (𝐴 − 𝐶) ∈ ℂ) |
4 | i2linesd.5 | . 2 ⊢ (𝜑 → 𝑋 ∈ ℂ) | |
5 | i2linesd.8 | . 2 ⊢ (𝜑 → (𝐴 − 𝐶) ≠ 0) | |
6 | 2, 4 | mulcld 10454 | . . . 4 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ) |
7 | i2linesd.4 | . . . . 5 ⊢ (𝜑 → 𝐷 ∈ ℂ) | |
8 | i2linesd.2 | . . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
9 | 7, 8 | subcld 10792 | . . . 4 ⊢ (𝜑 → (𝐷 − 𝐵) ∈ ℂ) |
10 | 1, 4 | mulcld 10454 | . . . . . 6 ⊢ (𝜑 → (𝐴 · 𝑋) ∈ ℂ) |
11 | i2linesd.6 | . . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐴 · 𝑋) + 𝐵)) | |
12 | i2linesd.7 | . . . . . . 7 ⊢ (𝜑 → 𝑌 = ((𝐶 · 𝑋) + 𝐷)) | |
13 | 11, 12 | eqtr3d 2810 | . . . . . 6 ⊢ (𝜑 → ((𝐴 · 𝑋) + 𝐵) = ((𝐶 · 𝑋) + 𝐷)) |
14 | 10, 8, 13 | mvlraddd 10845 | . . . . 5 ⊢ (𝜑 → (𝐴 · 𝑋) = (((𝐶 · 𝑋) + 𝐷) − 𝐵)) |
15 | 6, 7, 8, 14 | assraddsubd 10849 | . . . 4 ⊢ (𝜑 → (𝐴 · 𝑋) = ((𝐶 · 𝑋) + (𝐷 − 𝐵))) |
16 | 6, 9, 15 | mvrladdd 10848 | . . 3 ⊢ (𝜑 → ((𝐴 · 𝑋) − (𝐶 · 𝑋)) = (𝐷 − 𝐵)) |
17 | 1, 4, 2, 16 | joinlmulsubmuld 44242 | . 2 ⊢ (𝜑 → ((𝐴 − 𝐶) · 𝑋) = (𝐷 − 𝐵)) |
18 | 3, 4, 5, 17 | mvllmuld 11267 | 1 ⊢ (𝜑 → 𝑋 = ((𝐷 − 𝐵) / (𝐴 − 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ≠ wne 2961 (class class class)co 6970 ℂcc 10327 0cc0 10329 + caddc 10332 · cmul 10334 − cmin 10664 / cdiv 11092 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5306 df-po 5320 df-so 5321 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-er 8083 df-en 8301 df-dom 8302 df-sdom 8303 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-div 11093 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |