Proof of Theorem fldiv4p1lem1div2
Step | Hyp | Ref
| Expression |
1 | | 1le1 10534 |
. . . 4
⊢ 1 ≤
1 |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑁 = 3 → 1 ≤
1) |
3 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑁 = 3 → (𝑁 / 4) = (3 / 4)) |
4 | 3 | fveq2d 6107 |
. . . . . 6
⊢ (𝑁 = 3 →
(⌊‘(𝑁 / 4)) =
(⌊‘(3 / 4))) |
5 | | 3lt4 11074 |
. . . . . . 7
⊢ 3 <
4 |
6 | | 3nn0 11187 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
7 | | 4nn 11064 |
. . . . . . . 8
⊢ 4 ∈
ℕ |
8 | | divfl0 12487 |
. . . . . . . 8
⊢ ((3
∈ ℕ0 ∧ 4 ∈ ℕ) → (3 < 4 ↔
(⌊‘(3 / 4)) = 0)) |
9 | 6, 7, 8 | mp2an 704 |
. . . . . . 7
⊢ (3 < 4
↔ (⌊‘(3 / 4)) = 0) |
10 | 5, 9 | mpbi 219 |
. . . . . 6
⊢
(⌊‘(3 / 4)) = 0 |
11 | 4, 10 | syl6eq 2660 |
. . . . 5
⊢ (𝑁 = 3 →
(⌊‘(𝑁 / 4)) =
0) |
12 | 11 | oveq1d 6564 |
. . . 4
⊢ (𝑁 = 3 →
((⌊‘(𝑁 / 4)) +
1) = (0 + 1)) |
13 | | 0p1e1 11009 |
. . . 4
⊢ (0 + 1) =
1 |
14 | 12, 13 | syl6eq 2660 |
. . 3
⊢ (𝑁 = 3 →
((⌊‘(𝑁 / 4)) +
1) = 1) |
15 | | oveq1 6556 |
. . . . . 6
⊢ (𝑁 = 3 → (𝑁 − 1) = (3 −
1)) |
16 | | 3m1e2 11014 |
. . . . . 6
⊢ (3
− 1) = 2 |
17 | 15, 16 | syl6eq 2660 |
. . . . 5
⊢ (𝑁 = 3 → (𝑁 − 1) = 2) |
18 | 17 | oveq1d 6564 |
. . . 4
⊢ (𝑁 = 3 → ((𝑁 − 1) / 2) = (2 / 2)) |
19 | | 2div2e1 11027 |
. . . 4
⊢ (2 / 2) =
1 |
20 | 18, 19 | syl6eq 2660 |
. . 3
⊢ (𝑁 = 3 → ((𝑁 − 1) / 2) = 1) |
21 | 2, 14, 20 | 3brtr4d 4615 |
. 2
⊢ (𝑁 = 3 →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 − 1) /
2)) |
22 | | uzp1 11597 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘5) → (𝑁 = 5 ∨ 𝑁 ∈ (ℤ≥‘(5 +
1)))) |
23 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
24 | 23 | leidi 10441 |
. . . . . 6
⊢ 2 ≤
2 |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝑁 = 5 → 2 ≤
2) |
26 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑁 = 5 → (𝑁 / 4) = (5 / 4)) |
27 | 26 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑁 = 5 →
(⌊‘(𝑁 / 4)) =
(⌊‘(5 / 4))) |
28 | | df-5 10959 |
. . . . . . . . . . . 12
⊢ 5 = (4 +
1) |
29 | 28 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (5 / 4) =
((4 + 1) / 4) |
30 | | 4cn 10975 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
31 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
32 | | 4ne0 10994 |
. . . . . . . . . . . . 13
⊢ 4 ≠
0 |
33 | 30, 31, 30, 32 | divdiri 10661 |
. . . . . . . . . . . 12
⊢ ((4 + 1)
/ 4) = ((4 / 4) + (1 / 4)) |
34 | 30, 32 | dividi 10637 |
. . . . . . . . . . . . 13
⊢ (4 / 4) =
1 |
35 | 34 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ ((4 / 4)
+ (1 / 4)) = (1 + (1 / 4)) |
36 | 33, 35 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ((4 + 1)
/ 4) = (1 + (1 / 4)) |
37 | 29, 36 | eqtri 2632 |
. . . . . . . . . 10
⊢ (5 / 4) =
(1 + (1 / 4)) |
38 | 37 | fveq2i 6106 |
. . . . . . . . 9
⊢
(⌊‘(5 / 4)) = (⌊‘(1 + (1 / 4))) |
39 | | 1re 9918 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
40 | | 0le1 10430 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
41 | | 4re 10974 |
. . . . . . . . . . 11
⊢ 4 ∈
ℝ |
42 | | 4pos 10993 |
. . . . . . . . . . 11
⊢ 0 <
4 |
43 | | divge0 10771 |
. . . . . . . . . . 11
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (4 ∈ ℝ ∧ 0 < 4)) →
0 ≤ (1 / 4)) |
44 | 39, 40, 41, 42, 43 | mp4an 705 |
. . . . . . . . . 10
⊢ 0 ≤ (1
/ 4) |
45 | | 1lt4 11076 |
. . . . . . . . . . 11
⊢ 1 <
4 |
46 | | recgt1 10798 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) <
1)) |
47 | 41, 42, 46 | mp2an 704 |
. . . . . . . . . . 11
⊢ (1 < 4
↔ (1 / 4) < 1) |
48 | 45, 47 | mpbi 219 |
. . . . . . . . . 10
⊢ (1 / 4)
< 1 |
49 | | 1z 11284 |
. . . . . . . . . . 11
⊢ 1 ∈
ℤ |
50 | 41, 32 | rereccli 10669 |
. . . . . . . . . . 11
⊢ (1 / 4)
∈ ℝ |
51 | | flbi2 12480 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ (1 / 4) ∈ ℝ) → ((⌊‘(1 + (1 /
4))) = 1 ↔ (0 ≤ (1 / 4) ∧ (1 / 4) < 1))) |
52 | 49, 50, 51 | mp2an 704 |
. . . . . . . . . 10
⊢
((⌊‘(1 + (1 / 4))) = 1 ↔ (0 ≤ (1 / 4) ∧ (1 / 4)
< 1)) |
53 | 44, 48, 52 | mpbir2an 957 |
. . . . . . . . 9
⊢
(⌊‘(1 + (1 / 4))) = 1 |
54 | 38, 53 | eqtri 2632 |
. . . . . . . 8
⊢
(⌊‘(5 / 4)) = 1 |
55 | 27, 54 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑁 = 5 →
(⌊‘(𝑁 / 4)) =
1) |
56 | 55 | oveq1d 6564 |
. . . . . 6
⊢ (𝑁 = 5 →
((⌊‘(𝑁 / 4)) +
1) = (1 + 1)) |
57 | | 1p1e2 11011 |
. . . . . 6
⊢ (1 + 1) =
2 |
58 | 56, 57 | syl6eq 2660 |
. . . . 5
⊢ (𝑁 = 5 →
((⌊‘(𝑁 / 4)) +
1) = 2) |
59 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑁 = 5 → (𝑁 − 1) = (5 −
1)) |
60 | 30, 31, 28 | mvrraddi 10177 |
. . . . . . . 8
⊢ (5
− 1) = 4 |
61 | 59, 60 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑁 = 5 → (𝑁 − 1) = 4) |
62 | 61 | oveq1d 6564 |
. . . . . 6
⊢ (𝑁 = 5 → ((𝑁 − 1) / 2) = (4 / 2)) |
63 | | 4d2e2 11061 |
. . . . . 6
⊢ (4 / 2) =
2 |
64 | 62, 63 | syl6eq 2660 |
. . . . 5
⊢ (𝑁 = 5 → ((𝑁 − 1) / 2) = 2) |
65 | 25, 58, 64 | 3brtr4d 4615 |
. . . 4
⊢ (𝑁 = 5 →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 − 1) /
2)) |
66 | | eluz2 11569 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘6) ↔ (6 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 6 ≤
𝑁)) |
67 | | zre 11258 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
68 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℝ) |
69 | 41 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → 4 ∈
ℝ) |
70 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → 4 ≠
0) |
71 | 68, 69, 70 | redivcld 10732 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → (𝑁 / 4) ∈
ℝ) |
72 | | flle 12462 |
. . . . . . . . . . 11
⊢ ((𝑁 / 4) ∈ ℝ →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) |
73 | 67, 71, 72 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) |
74 | 73 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
(⌊‘(𝑁 / 4))
≤ (𝑁 /
4)) |
75 | 71 | flcld 12461 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℤ) |
76 | 75 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ →
(⌊‘(𝑁 / 4))
∈ ℝ) |
77 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → 1 ∈
ℝ) |
78 | 76, 71, 77 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ 1 ∈ ℝ)) |
79 | 67, 78 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ 1 ∈ ℝ)) |
80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
((⌊‘(𝑁 / 4))
∈ ℝ ∧ (𝑁 /
4) ∈ ℝ ∧ 1 ∈ ℝ)) |
81 | | leadd1 10375 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑁
/ 4)) ∈ ℝ ∧ (𝑁 / 4) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((⌊‘(𝑁 /
4)) ≤ (𝑁 / 4) ↔
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 / 4) +
1))) |
82 | 80, 81 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
((⌊‘(𝑁 / 4))
≤ (𝑁 / 4) ↔
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 / 4) +
1))) |
83 | 74, 82 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 / 4) +
1)) |
84 | | div4p1lem1div2 11164 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 6 ≤
𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) /
2)) |
85 | 67, 84 | sylan 487 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) /
2)) |
86 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑁 /
4)) ∈ ℝ → ((⌊‘(𝑁 / 4)) + 1) ∈ ℝ) |
87 | 76, 86 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ →
((⌊‘(𝑁 / 4)) +
1) ∈ ℝ) |
88 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢ ((𝑁 / 4) ∈ ℝ →
((𝑁 / 4) + 1) ∈
ℝ) |
89 | 71, 88 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → ((𝑁 / 4) + 1) ∈
ℝ) |
90 | | peano2rem 10227 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) ∈
ℝ) |
91 | 90 | rehalfcld 11156 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℝ → ((𝑁 − 1) / 2) ∈
ℝ) |
92 | 87, 89, 91 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ →
(((⌊‘(𝑁 / 4)) +
1) ∈ ℝ ∧ ((𝑁
/ 4) + 1) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈
ℝ)) |
93 | 67, 92 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(((⌊‘(𝑁 / 4)) +
1) ∈ ℝ ∧ ((𝑁
/ 4) + 1) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈
ℝ)) |
94 | 93 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
(((⌊‘(𝑁 / 4)) +
1) ∈ ℝ ∧ ((𝑁
/ 4) + 1) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈
ℝ)) |
95 | | letr 10010 |
. . . . . . . . 9
⊢
((((⌊‘(𝑁
/ 4)) + 1) ∈ ℝ ∧ ((𝑁 / 4) + 1) ∈ ℝ ∧ ((𝑁 − 1) / 2) ∈ ℝ)
→ ((((⌊‘(𝑁
/ 4)) + 1) ≤ ((𝑁 / 4) +
1) ∧ ((𝑁 / 4) + 1) ≤
((𝑁 − 1) / 2)) →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 − 1) /
2))) |
96 | 94, 95 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
((((⌊‘(𝑁 / 4))
+ 1) ≤ ((𝑁 / 4) + 1)
∧ ((𝑁 / 4) + 1) ≤
((𝑁 − 1) / 2)) →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 − 1) /
2))) |
97 | 83, 85, 96 | mp2and 711 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 6 ≤
𝑁) →
((⌊‘(𝑁 / 4)) +
1) ≤ ((𝑁 − 1) /
2)) |
98 | 97 | 3adant1 1072 |
. . . . . 6
⊢ ((6
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 6 ≤ 𝑁) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2)) |
99 | 66, 98 | sylbi 206 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘6) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2)) |
100 | | 5p1e6 11032 |
. . . . . 6
⊢ (5 + 1) =
6 |
101 | 100 | fveq2i 6106 |
. . . . 5
⊢
(ℤ≥‘(5 + 1)) =
(ℤ≥‘6) |
102 | 99, 101 | eleq2s 2706 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘(5 + 1)) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) /
2)) |
103 | 65, 102 | jaoi 393 |
. . 3
⊢ ((𝑁 = 5 ∨ 𝑁 ∈ (ℤ≥‘(5 +
1))) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2)) |
104 | 22, 103 | syl 17 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘5) → ((⌊‘(𝑁 / 4)) + 1) ≤ ((𝑁 − 1) / 2)) |
105 | 21, 104 | jaoi 393 |
1
⊢ ((𝑁 = 3 ∨ 𝑁 ∈ (ℤ≥‘5))
→ ((⌊‘(𝑁 /
4)) + 1) ≤ ((𝑁 −
1) / 2)) |