Proof of Theorem divdivdivap
Step | Hyp | Ref
| Expression |
1 | | simprrl 491 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → 𝐷 ∈
ℂ) |
2 | | simprll 489 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → 𝐶 ∈
ℂ) |
3 | | simprlr 490 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → 𝐶 # 0) |
4 | | divclap 7439 |
. . . . . . 7
⊢ ((𝐷 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 # 0) → (𝐷 / 𝐶) ∈
ℂ) |
5 | 1, 2, 3, 4 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐷 / 𝐶) ∈
ℂ) |
6 | | simpll 481 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → A ∈
ℂ) |
7 | | simplrl 487 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → B ∈
ℂ) |
8 | | simplrr 488 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → B # 0) |
9 | | divclap 7439 |
. . . . . . 7
⊢
((A ∈ ℂ ∧
B ∈
ℂ ∧ B # 0) → (A
/ B) ∈
ℂ) |
10 | 6, 7, 8, 9 | syl3anc 1134 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (A / B) ∈ ℂ) |
11 | 5, 10 | mulcomd 6846 |
. . . . 5
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐷 / 𝐶) · (A / B)) =
((A / B) · (𝐷 / 𝐶))) |
12 | | simplr 482 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (B ∈ ℂ ∧ B #
0)) |
13 | | simprl 483 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐶 ∈ ℂ
∧ 𝐶 # 0)) |
14 | | divmuldivap 7470 |
. . . . . 6
⊢
(((A ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧
((B ∈
ℂ ∧ B # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0))) → ((A / B) ·
(𝐷 / 𝐶)) = ((A
· 𝐷) / (B · 𝐶))) |
15 | 6, 1, 12, 13, 14 | syl22anc 1135 |
. . . . 5
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((A / B) ·
(𝐷 / 𝐶)) = ((A
· 𝐷) / (B · 𝐶))) |
16 | 11, 15 | eqtrd 2069 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐷 / 𝐶) · (A / B)) =
((A · 𝐷) / (B
· 𝐶))) |
17 | 16 | oveq2d 5471 |
. . 3
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (A / B))) =
((𝐶 / 𝐷) · ((A · 𝐷) / (B
· 𝐶)))) |
18 | | simprr 484 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐷 ∈ ℂ
∧ 𝐷 # 0)) |
19 | | divmuldivap 7470 |
. . . . . . 7
⊢ (((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧
((𝐷 ∈ ℂ ∧ 𝐷 # 0) ∧ (𝐶 ∈ ℂ
∧ 𝐶 # 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = ((𝐶 · 𝐷) / (𝐷 · 𝐶))) |
20 | 2, 1, 18, 13, 19 | syl22anc 1135 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = ((𝐶 · 𝐷) / (𝐷 · 𝐶))) |
21 | 2, 1 | mulcomd 6846 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐶 · 𝐷) = (𝐷 · 𝐶)) |
22 | 21 | oveq1d 5470 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 · 𝐷) / (𝐷 · 𝐶)) = ((𝐷 · 𝐶) / (𝐷 · 𝐶))) |
23 | 1, 2 | mulcld 6845 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐷 · 𝐶) ∈
ℂ) |
24 | | simprrr 492 |
. . . . . . . . 9
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → 𝐷 # 0) |
25 | 1, 2, 24, 3 | mulap0d 7421 |
. . . . . . . 8
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐷 · 𝐶) # 0) |
26 | | dividap 7460 |
. . . . . . . 8
⊢ (((𝐷 · 𝐶) ∈
ℂ ∧ (𝐷 · 𝐶) # 0) → ((𝐷 · 𝐶) / (𝐷 · 𝐶)) = 1) |
27 | 23, 25, 26 | syl2anc 391 |
. . . . . . 7
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐷 · 𝐶) / (𝐷 · 𝐶)) = 1) |
28 | 22, 27 | eqtrd 2069 |
. . . . . 6
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 · 𝐷) / (𝐷 · 𝐶)) = 1) |
29 | 20, 28 | eqtrd 2069 |
. . . . 5
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 / 𝐷) · (𝐷 / 𝐶)) = 1) |
30 | 29 | oveq1d 5470 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (((𝐶 / 𝐷) · (𝐷 / 𝐶)) · (A / B)) = (1
· (A / B))) |
31 | | divclap 7439 |
. . . . . 6
⊢ ((𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐷 # 0) → (𝐶 / 𝐷) ∈
ℂ) |
32 | 2, 1, 24, 31 | syl3anc 1134 |
. . . . 5
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐶 / 𝐷) ∈
ℂ) |
33 | 32, 5, 10 | mulassd 6848 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (((𝐶 / 𝐷) · (𝐷 / 𝐶)) · (A / B)) =
((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (A / B)))) |
34 | 10 | mulid2d 6843 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (1 · (A / B)) =
(A / B)) |
35 | 30, 33, 34 | 3eqtr3d 2077 |
. . 3
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 / 𝐷) · ((𝐷 / 𝐶) · (A / B))) =
(A / B)) |
36 | 17, 35 | eqtr3d 2071 |
. 2
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((𝐶 / 𝐷) · ((A · 𝐷) / (B
· 𝐶))) = (A / B)) |
37 | 6, 1 | mulcld 6845 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (A · 𝐷) ∈
ℂ) |
38 | 7, 2 | mulcld 6845 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (B · 𝐶) ∈
ℂ) |
39 | | mulap0 7417 |
. . . . 5
⊢
(((B ∈ ℂ ∧
B # 0) ∧
(𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (B · 𝐶) # 0) |
40 | 39 | ad2ant2lr 479 |
. . . 4
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (B · 𝐶) # 0) |
41 | | divclap 7439 |
. . . 4
⊢
(((A · 𝐷) ∈
ℂ ∧ (B · 𝐶) ∈
ℂ ∧ (B · 𝐶) # 0) → ((A · 𝐷) / (B
· 𝐶)) ∈ ℂ) |
42 | 37, 38, 40, 41 | syl3anc 1134 |
. . 3
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((A · 𝐷) / (B
· 𝐶)) ∈ ℂ) |
43 | | divap0 7445 |
. . . 4
⊢ (((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0)) → (𝐶 / 𝐷) # 0) |
44 | 43 | adantl 262 |
. . 3
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (𝐶 / 𝐷) # 0) |
45 | | divmulap 7436 |
. . 3
⊢
(((A / B) ∈ ℂ ∧ ((A ·
𝐷) / (B · 𝐶)) ∈
ℂ ∧ ((𝐶 / 𝐷) ∈
ℂ ∧ (𝐶 / 𝐷) # 0)) → (((A / B) / (𝐶 / 𝐷)) = ((A
· 𝐷) / (B · 𝐶)) ↔ ((𝐶 / 𝐷) · ((A · 𝐷) / (B
· 𝐶))) = (A / B))) |
46 | 10, 42, 32, 44, 45 | syl112anc 1138 |
. 2
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → (((A / B) / (𝐶 / 𝐷)) = ((A
· 𝐷) / (B · 𝐶)) ↔ ((𝐶 / 𝐷) · ((A · 𝐷) / (B
· 𝐶))) = (A / B))) |
47 | 36, 46 | mpbird 156 |
1
⊢
(((A ∈ ℂ ∧
(B ∈
ℂ ∧ B # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ
∧ 𝐷 # 0))) → ((A / B) / (𝐶 / 𝐷)) = ((A
· 𝐷) / (B · 𝐶))) |