Step | Hyp | Ref
| Expression |
1 | | elq 9581 |
. . 3
⊢ (𝑄 ∈ ℚ ↔
∃𝑎 ∈ ℤ
∃𝑏 ∈ ℕ
𝑄 = (𝑎 / 𝑏)) |
2 | 1 | biimpi 119 |
. 2
⊢ (𝑄 ∈ ℚ →
∃𝑎 ∈ ℤ
∃𝑏 ∈ ℕ
𝑄 = (𝑎 / 𝑏)) |
3 | | simplrl 530 |
. . . . . . . . 9
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → 𝑎 ∈ ℤ) |
4 | 3 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑎 ∈ ℤ) |
5 | | simplrr 531 |
. . . . . . . . 9
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → 𝑏 ∈ ℕ) |
6 | 5 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑏 ∈ ℕ) |
7 | | znq 9583 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ) → (𝑎 / 𝑏) ∈ ℚ) |
8 | | qre 9584 |
. . . . . . . . 9
⊢ ((𝑎 / 𝑏) ∈ ℚ → (𝑎 / 𝑏) ∈ ℝ) |
9 | 7, 8 | syl 14 |
. . . . . . . 8
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ) → (𝑎 / 𝑏) ∈ ℝ) |
10 | 4, 6, 9 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (𝑎 / 𝑏) ∈ ℝ) |
11 | | sqrt2re 12117 |
. . . . . . . 8
⊢
(√‘2) ∈ ℝ |
12 | 11 | a1i 9 |
. . . . . . 7
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (√‘2) ∈
ℝ) |
13 | | 0red 7921 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 0 ∈
ℝ) |
14 | 4 | zcnd 9335 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑎 ∈ ℂ) |
15 | 6 | nncnd 8892 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑏 ∈ ℂ) |
16 | 6 | nnap0d 8924 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑏 # 0) |
17 | 14, 15, 16 | divrecapd 8710 |
. . . . . . . . 9
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (𝑎 / 𝑏) = (𝑎 · (1 / 𝑏))) |
18 | 4 | zred 9334 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑎 ∈ ℝ) |
19 | 6 | nnrecred 8925 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (1 / 𝑏) ∈ ℝ) |
20 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑎 ≤ 0) |
21 | | 1red 7935 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 1 ∈
ℝ) |
22 | 6 | nnrpd 9651 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 𝑏 ∈ ℝ+) |
23 | | 0le1 8400 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
24 | 23 | a1i 9 |
. . . . . . . . . . 11
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 0 ≤ 1) |
25 | 21, 22, 24 | divge0d 9694 |
. . . . . . . . . 10
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 0 ≤ (1 / 𝑏)) |
26 | | mulle0r 8860 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ ∧ (1 / 𝑏) ∈ ℝ) ∧ (𝑎 ≤ 0 ∧ 0 ≤ (1 / 𝑏))) → (𝑎 · (1 / 𝑏)) ≤ 0) |
27 | 18, 19, 20, 25, 26 | syl22anc 1234 |
. . . . . . . . 9
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (𝑎 · (1 / 𝑏)) ≤ 0) |
28 | 17, 27 | eqbrtrd 4011 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (𝑎 / 𝑏) ≤ 0) |
29 | | 2re 8948 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
30 | | 2pos 8969 |
. . . . . . . . . 10
⊢ 0 <
2 |
31 | 29, 30 | sqrtgt0ii 11095 |
. . . . . . . . 9
⊢ 0 <
(√‘2) |
32 | 31 | a1i 9 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → 0 <
(√‘2)) |
33 | 10, 13, 12, 28, 32 | lelttrd 8044 |
. . . . . . 7
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (𝑎 / 𝑏) < (√‘2)) |
34 | 10, 12, 33 | gtapd 8556 |
. . . . . 6
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 𝑎 ≤ 0) → (√‘2) # (𝑎 / 𝑏)) |
35 | 3 | adantr 274 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 0 < 𝑎) → 𝑎 ∈ ℤ) |
36 | | simpr 109 |
. . . . . . . 8
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 0 < 𝑎) → 0 < 𝑎) |
37 | | elnnz 9222 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 0 <
𝑎)) |
38 | 35, 36, 37 | sylanbrc 415 |
. . . . . . 7
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 0 < 𝑎) → 𝑎 ∈ ℕ) |
39 | 5 | adantr 274 |
. . . . . . 7
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 0 < 𝑎) → 𝑏 ∈ ℕ) |
40 | | sqrt2irraplemnn 12133 |
. . . . . . 7
⊢ ((𝑎 ∈ ℕ ∧ 𝑏 ∈ ℕ) →
(√‘2) # (𝑎 /
𝑏)) |
41 | 38, 39, 40 | syl2anc 409 |
. . . . . 6
⊢ ((((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) ∧ 0 < 𝑎) → (√‘2) # (𝑎 / 𝑏)) |
42 | | 0z 9223 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
43 | | zlelttric 9257 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑎 ≤ 0
∨ 0 < 𝑎)) |
44 | 42, 43 | mpan2 423 |
. . . . . . . 8
⊢ (𝑎 ∈ ℤ → (𝑎 ≤ 0 ∨ 0 < 𝑎)) |
45 | 44 | ad2antrl 487 |
. . . . . . 7
⊢ ((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) → (𝑎 ≤ 0 ∨ 0 < 𝑎)) |
46 | 45 | adantr 274 |
. . . . . 6
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → (𝑎 ≤ 0 ∨ 0 < 𝑎)) |
47 | 34, 41, 46 | mpjaodan 793 |
. . . . 5
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → (√‘2) # (𝑎 / 𝑏)) |
48 | | simpr 109 |
. . . . 5
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → 𝑄 = (𝑎 / 𝑏)) |
49 | 47, 48 | breqtrrd 4017 |
. . . 4
⊢ (((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) ∧ 𝑄 = (𝑎 / 𝑏)) → (√‘2) # 𝑄) |
50 | 49 | ex 114 |
. . 3
⊢ ((𝑄 ∈ ℚ ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℕ)) → (𝑄 = (𝑎 / 𝑏) → (√‘2) # 𝑄)) |
51 | 50 | rexlimdvva 2595 |
. 2
⊢ (𝑄 ∈ ℚ →
(∃𝑎 ∈ ℤ
∃𝑏 ∈ ℕ
𝑄 = (𝑎 / 𝑏) → (√‘2) # 𝑄)) |
52 | 2, 51 | mpd 13 |
1
⊢ (𝑄 ∈ ℚ →
(√‘2) # 𝑄) |