Step | Hyp | Ref
| Expression |
1 | | elq 8333 |
. . . 4
⊢ (B ∈ ℚ ↔
∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)) |
2 | 1 | biimpi 113 |
. . 3
⊢ (B ∈ ℚ →
∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)) |
3 | 2 | adantl 262 |
. 2
⊢
((A ∈ ℚ ∧
B ∈
ℚ) → ∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)) |
4 | | simplll 485 |
. . . . . 6
⊢
((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) → A ∈
ℚ) |
5 | | elq 8333 |
. . . . . 6
⊢ (A ∈ ℚ ↔
∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)) |
6 | 4, 5 | sylib 127 |
. . . . 5
⊢
((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) → ∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)) |
7 | | simplrl 487 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → x
∈ ℤ) |
8 | 7 | zcnd 8137 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → x
∈ ℂ) |
9 | | simprl 483 |
. . . . . . . . . . . . . . . 16
⊢
(((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → z ∈
ℤ) |
10 | 9 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → z
∈ ℤ) |
11 | 10 | zcnd 8137 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → z
∈ ℂ) |
12 | | simprr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → w ∈
ℕ) |
13 | 12 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → w
∈ ℕ) |
14 | 13 | nncnd 7709 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → w
∈ ℂ) |
15 | | nnap0 7724 |
. . . . . . . . . . . . . . 15
⊢ (w ∈ ℕ →
w # 0) |
16 | 13, 15 | syl 14 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → w #
0) |
17 | 11, 14, 16 | divclapd 7547 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (z /
w) ∈
ℂ) |
18 | | simplrr 488 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → y
∈ ℕ) |
19 | 18 | nncnd 7709 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → y
∈ ℂ) |
20 | 17, 19 | mulcld 6845 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((z /
w) · y) ∈
ℂ) |
21 | | nnap0 7724 |
. . . . . . . . . . . . . 14
⊢ (y ∈ ℕ →
y # 0) |
22 | 18, 21 | syl 14 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → y #
0) |
23 | 19, 22 | recclapd 7539 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (1 / y) ∈
ℂ) |
24 | 19, 22 | recap0d 7540 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (1 / y) # 0) |
25 | | apmul1 7546 |
. . . . . . . . . . . 12
⊢
((x ∈ ℂ ∧
((z / w) · y)
∈ ℂ ∧
((1 / y) ∈ ℂ ∧ (1 /
y) # 0)) → (x # ((z /
w) · y) ↔ (x
· (1 / y)) # (((z / w) ·
y) · (1 / y)))) |
26 | 8, 20, 23, 24, 25 | syl112anc 1138 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x #
((z / w) · y)
↔ (x · (1 / y)) # (((z /
w) · y) · (1 / y)))) |
27 | 8, 19, 22 | divrecapd 7550 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x /
y) = (x
· (1 / y))) |
28 | 27 | eqcomd 2042 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x
· (1 / y)) = (x / y)) |
29 | 17, 19, 23 | mulassd 6848 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (((z
/ w) · y) · (1 / y)) = ((z /
w) · (y · (1 / y)))) |
30 | 19, 22 | recidapd 7541 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (y
· (1 / y)) = 1) |
31 | 30 | oveq2d 5471 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((z /
w) · (y · (1 / y))) = ((z /
w) · 1)) |
32 | 17 | mulid1d 6842 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((z /
w) · 1) = (z / w)) |
33 | 29, 31, 32 | 3eqtrd 2073 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (((z
/ w) · y) · (1 / y)) = (z /
w)) |
34 | 28, 33 | breq12d 3768 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· (1 / y)) # (((z / w) ·
y) · (1 / y)) ↔ (x /
y) # (z
/ w))) |
35 | 26, 34 | bitrd 177 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x #
((z / w) · y)
↔ (x / y) # (z /
w))) |
36 | 13 | nnzd 8135 |
. . . . . . . . . . . . . . 15
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → w
∈ ℤ) |
37 | 7, 36 | zmulcld 8142 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x
· w) ∈ ℤ) |
38 | 37 | zcnd 8137 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x
· w) ∈ ℂ) |
39 | 18 | nnzd 8135 |
. . . . . . . . . . . . . . 15
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → y
∈ ℤ) |
40 | 39, 10 | zmulcld 8142 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (y
· z) ∈ ℤ) |
41 | 40 | zcnd 8137 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (y
· z) ∈ ℂ) |
42 | 14, 16 | recclapd 7539 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (1 / w) ∈
ℂ) |
43 | 14, 16 | recap0d 7540 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (1 / w) # 0) |
44 | | apmul1 7546 |
. . . . . . . . . . . . 13
⊢
(((x · w) ∈ ℂ ∧ (y ·
z) ∈
ℂ ∧ ((1 / w) ∈ ℂ ∧ (1 / w) # 0))
→ ((x · w) # (y ·
z) ↔ ((x · w)
· (1 / w)) # ((y · z)
· (1 / w)))) |
45 | 38, 41, 42, 43, 44 | syl112anc 1138 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) # (y · z)
↔ ((x · w) · (1 / w)) # ((y
· z) · (1 / w)))) |
46 | 8, 14, 42 | mulassd 6848 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) · (1 / w)) = (x
· (w · (1 / w)))) |
47 | 14, 16 | recidapd 7541 |
. . . . . . . . . . . . . . 15
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (w
· (1 / w)) = 1) |
48 | 47 | oveq2d 5471 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x
· (w · (1 / w))) = (x
· 1)) |
49 | 8 | mulid1d 6842 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x
· 1) = x) |
50 | 46, 48, 49 | 3eqtrd 2073 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) · (1 / w)) = x) |
51 | 50 | breq1d 3765 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (((x
· w) · (1 / w)) # ((y
· z) · (1 / w)) ↔ x #
((y · z) · (1 / w)))) |
52 | 45, 51 | bitrd 177 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) # (y · z)
↔ x # ((y · z)
· (1 / w)))) |
53 | 19, 11, 42 | mulassd 6848 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((y
· z) · (1 / w)) = (y
· (z · (1 / w)))) |
54 | 11, 14, 16 | divrecapd 7550 |
. . . . . . . . . . . . . 14
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (z /
w) = (z
· (1 / w))) |
55 | 54 | oveq2d 5471 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (y
· (z / w)) = (y
· (z · (1 / w)))) |
56 | 19, 17 | mulcomd 6846 |
. . . . . . . . . . . . 13
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (y
· (z / w)) = ((z /
w) · y)) |
57 | 53, 55, 56 | 3eqtr2d 2075 |
. . . . . . . . . . . 12
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((y
· z) · (1 / w)) = ((z /
w) · y)) |
58 | 57 | breq2d 3767 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (x #
((y · z) · (1 / w)) ↔ x #
((z / w) · y))) |
59 | 52, 58 | bitrd 177 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) # (y · z)
↔ x # ((z / w) ·
y))) |
60 | | simpr 103 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → A =
(x / y)) |
61 | | simpllr 486 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → B =
(z / w)) |
62 | 60, 61 | breq12d 3768 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (A #
B ↔ (x / y) #
(z / w))) |
63 | 35, 59, 62 | 3bitr4d 209 |
. . . . . . . . 9
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) # (y · z)
↔ A # B)) |
64 | | zapne 8091 |
. . . . . . . . . 10
⊢
(((x · w) ∈ ℤ ∧ (y ·
z) ∈
ℤ) → ((x · w) # (y ·
z) ↔ (x · w)
≠ (y · z))) |
65 | 37, 40, 64 | syl2anc 391 |
. . . . . . . . 9
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) # (y · z)
↔ (x · w) ≠ (y
· z))) |
66 | 63, 65 | bitr3d 179 |
. . . . . . . 8
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (A #
B ↔ (x · w)
≠ (y · z))) |
67 | 63 | notbid 591 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (¬ (x · w) #
(y · z) ↔ ¬ A # B)) |
68 | | apti 7406 |
. . . . . . . . . . 11
⊢
(((x · w) ∈ ℂ ∧ (y ·
z) ∈
ℂ) → ((x · w) = (y ·
z) ↔ ¬ (x · w) #
(y · z))) |
69 | 38, 41, 68 | syl2anc 391 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) = (y · z)
↔ ¬ (x · w) # (y ·
z))) |
70 | | qcn 8345 |
. . . . . . . . . . . . 13
⊢ (A ∈ ℚ →
A ∈
ℂ) |
71 | 70 | ad2antrr 457 |
. . . . . . . . . . . 12
⊢
(((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → A ∈
ℂ) |
72 | 71 | ad3antrrr 461 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → A
∈ ℂ) |
73 | 61, 17 | eqeltrd 2111 |
. . . . . . . . . . 11
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → B
∈ ℂ) |
74 | | apti 7406 |
. . . . . . . . . . 11
⊢
((A ∈ ℂ ∧
B ∈
ℂ) → (A = B ↔ ¬ A
# B)) |
75 | 72, 73, 74 | syl2anc 391 |
. . . . . . . . . 10
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (A =
B ↔ ¬ A # B)) |
76 | 67, 69, 75 | 3bitr4d 209 |
. . . . . . . . 9
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) = (y · z)
↔ A = B)) |
77 | 76 | necon3bid 2240 |
. . . . . . . 8
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → ((x
· w) ≠ (y · z)
↔ A ≠ B)) |
78 | 66, 77 | bitrd 177 |
. . . . . . 7
⊢
((((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
∧ A =
(x / y)) → (A #
B ↔ A ≠ B)) |
79 | 78 | ex 108 |
. . . . . 6
⊢
(((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) ∧
(x ∈
ℤ ∧ y ∈ ℕ))
→ (A = (x / y) →
(A # B
↔ A ≠ B))) |
80 | 79 | rexlimdvva 2434 |
. . . . 5
⊢
((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) → (∃x ∈ ℤ ∃y ∈ ℕ A =
(x / y)
→ (A # B ↔ A ≠
B))) |
81 | 6, 80 | mpd 13 |
. . . 4
⊢
((((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) ∧
B = (z
/ w)) → (A # B ↔
A ≠ B)) |
82 | 81 | ex 108 |
. . 3
⊢
(((A ∈ ℚ ∧
B ∈
ℚ) ∧ (z ∈ ℤ ∧ w ∈ ℕ)) → (B = (z /
w) → (A # B ↔
A ≠ B))) |
83 | 82 | rexlimdvva 2434 |
. 2
⊢
((A ∈ ℚ ∧
B ∈
ℚ) → (∃z ∈ ℤ ∃w ∈ ℕ B =
(z / w)
→ (A # B ↔ A ≠
B))) |
84 | 3, 83 | mpd 13 |
1
⊢
((A ∈ ℚ ∧
B ∈
ℚ) → (A # B ↔ A ≠
B)) |