MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  flodddiv4 Structured version   Visualization version   GIF version

Theorem flodddiv4 15472
Description: The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.)
Assertion
Ref Expression
flodddiv4 ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)))

Proof of Theorem flodddiv4
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 oveq1 6885 . . . 4 (𝑁 = ((2 · 𝑀) + 1) → (𝑁 / 4) = (((2 · 𝑀) + 1) / 4))
2 2cnd 11391 . . . . . . 7 (𝑀 ∈ ℤ → 2 ∈ ℂ)
3 zcn 11671 . . . . . . 7 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
42, 3mulcld 10349 . . . . . 6 (𝑀 ∈ ℤ → (2 · 𝑀) ∈ ℂ)
5 1cnd 10323 . . . . . 6 (𝑀 ∈ ℤ → 1 ∈ ℂ)
6 4cn 11399 . . . . . . . 8 4 ∈ ℂ
7 4ne0 11428 . . . . . . . 8 4 ≠ 0
86, 7pm3.2i 463 . . . . . . 7 (4 ∈ ℂ ∧ 4 ≠ 0)
98a1i 11 . . . . . 6 (𝑀 ∈ ℤ → (4 ∈ ℂ ∧ 4 ≠ 0))
10 divdir 11002 . . . . . 6 (((2 · 𝑀) ∈ ℂ ∧ 1 ∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → (((2 · 𝑀) + 1) / 4) = (((2 · 𝑀) / 4) + (1 / 4)))
114, 5, 9, 10syl3anc 1491 . . . . 5 (𝑀 ∈ ℤ → (((2 · 𝑀) + 1) / 4) = (((2 · 𝑀) / 4) + (1 / 4)))
12 2t2e4 11484 . . . . . . . . . 10 (2 · 2) = 4
1312eqcomi 2808 . . . . . . . . 9 4 = (2 · 2)
1413a1i 11 . . . . . . . 8 (𝑀 ∈ ℤ → 4 = (2 · 2))
1514oveq2d 6894 . . . . . . 7 (𝑀 ∈ ℤ → ((2 · 𝑀) / 4) = ((2 · 𝑀) / (2 · 2)))
16 2ne0 11424 . . . . . . . . 9 2 ≠ 0
1716a1i 11 . . . . . . . 8 (𝑀 ∈ ℤ → 2 ≠ 0)
183, 2, 2, 17, 17divcan5d 11119 . . . . . . 7 (𝑀 ∈ ℤ → ((2 · 𝑀) / (2 · 2)) = (𝑀 / 2))
1915, 18eqtrd 2833 . . . . . 6 (𝑀 ∈ ℤ → ((2 · 𝑀) / 4) = (𝑀 / 2))
2019oveq1d 6893 . . . . 5 (𝑀 ∈ ℤ → (((2 · 𝑀) / 4) + (1 / 4)) = ((𝑀 / 2) + (1 / 4)))
2111, 20eqtrd 2833 . . . 4 (𝑀 ∈ ℤ → (((2 · 𝑀) + 1) / 4) = ((𝑀 / 2) + (1 / 4)))
221, 21sylan9eqr 2855 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (𝑁 / 4) = ((𝑀 / 2) + (1 / 4)))
2322fveq2d 6415 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = (⌊‘((𝑀 / 2) + (1 / 4))))
24 iftrue 4283 . . . . . . 7 (2 ∥ 𝑀 → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2))
2524adantr 473 . . . . . 6 ((2 ∥ 𝑀𝑀 ∈ ℤ) → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (𝑀 / 2))
26 1re 10328 . . . . . . . . 9 1 ∈ ℝ
27 0le1 10843 . . . . . . . . 9 0 ≤ 1
28 4re 11398 . . . . . . . . 9 4 ∈ ℝ
29 4pos 11427 . . . . . . . . 9 0 < 4
30 divge0 11184 . . . . . . . . 9 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ (4 ∈ ℝ ∧ 0 < 4)) → 0 ≤ (1 / 4))
3126, 27, 28, 29, 30mp4an 685 . . . . . . . 8 0 ≤ (1 / 4)
32 1lt4 11496 . . . . . . . . 9 1 < 4
33 recgt1 11211 . . . . . . . . . 10 ((4 ∈ ℝ ∧ 0 < 4) → (1 < 4 ↔ (1 / 4) < 1))
3428, 29, 33mp2an 684 . . . . . . . . 9 (1 < 4 ↔ (1 / 4) < 1)
3532, 34mpbi 222 . . . . . . . 8 (1 / 4) < 1
3631, 35pm3.2i 463 . . . . . . 7 (0 ≤ (1 / 4) ∧ (1 / 4) < 1)
37 2z 11699 . . . . . . . . . . 11 2 ∈ ℤ
3837a1i 11 . . . . . . . . . 10 (𝑀 ∈ ℤ → 2 ∈ ℤ)
39 id 22 . . . . . . . . . 10 (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
40 dvdsval2 15322 . . . . . . . . . 10 ((2 ∈ ℤ ∧ 2 ≠ 0 ∧ 𝑀 ∈ ℤ) → (2 ∥ 𝑀 ↔ (𝑀 / 2) ∈ ℤ))
4138, 17, 39, 40syl3anc 1491 . . . . . . . . 9 (𝑀 ∈ ℤ → (2 ∥ 𝑀 ↔ (𝑀 / 2) ∈ ℤ))
4241biimpac 471 . . . . . . . 8 ((2 ∥ 𝑀𝑀 ∈ ℤ) → (𝑀 / 2) ∈ ℤ)
43 4nn 11397 . . . . . . . . 9 4 ∈ ℕ
44 nnrecre 11355 . . . . . . . . 9 (4 ∈ ℕ → (1 / 4) ∈ ℝ)
4543, 44ax-mp 5 . . . . . . . 8 (1 / 4) ∈ ℝ
46 flbi2 12873 . . . . . . . 8 (((𝑀 / 2) ∈ ℤ ∧ (1 / 4) ∈ ℝ) → ((⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2) ↔ (0 ≤ (1 / 4) ∧ (1 / 4) < 1)))
4742, 45, 46sylancl 581 . . . . . . 7 ((2 ∥ 𝑀𝑀 ∈ ℤ) → ((⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2) ↔ (0 ≤ (1 / 4) ∧ (1 / 4) < 1)))
4836, 47mpbiri 250 . . . . . 6 ((2 ∥ 𝑀𝑀 ∈ ℤ) → (⌊‘((𝑀 / 2) + (1 / 4))) = (𝑀 / 2))
4925, 48eqtr4d 2836 . . . . 5 ((2 ∥ 𝑀𝑀 ∈ ℤ) → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 / 4))))
50 iffalse 4286 . . . . . . 7 (¬ 2 ∥ 𝑀 → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2))
5150adantr 473 . . . . . 6 ((¬ 2 ∥ 𝑀𝑀 ∈ ℤ) → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = ((𝑀 − 1) / 2))
52 odd2np1 15401 . . . . . . . 8 (𝑀 ∈ ℤ → (¬ 2 ∥ 𝑀 ↔ ∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = 𝑀))
53 ax-1cn 10282 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℂ
54 2cnne0 11530 . . . . . . . . . . . . . . . . . . . . 21 (2 ∈ ℂ ∧ 2 ≠ 0)
55 divcan5 11019 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 / 2))
5653, 54, 54, 55mp3an 1586 . . . . . . . . . . . . . . . . . . . 20 ((2 · 1) / (2 · 2)) = (1 / 2)
57 2t1e2 11483 . . . . . . . . . . . . . . . . . . . . 21 (2 · 1) = 2
5857, 12oveq12i 6890 . . . . . . . . . . . . . . . . . . . 20 ((2 · 1) / (2 · 2)) = (2 / 4)
5956, 58eqtr3i 2823 . . . . . . . . . . . . . . . . . . 19 (1 / 2) = (2 / 4)
6059oveq1i 6888 . . . . . . . . . . . . . . . . . 18 ((1 / 2) + (1 / 4)) = ((2 / 4) + (1 / 4))
61 2cn 11388 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℂ
6261, 53, 6, 7divdiri 11074 . . . . . . . . . . . . . . . . . 18 ((2 + 1) / 4) = ((2 / 4) + (1 / 4))
63 2p1e3 11462 . . . . . . . . . . . . . . . . . . 19 (2 + 1) = 3
6463oveq1i 6888 . . . . . . . . . . . . . . . . . 18 ((2 + 1) / 4) = (3 / 4)
6560, 62, 643eqtr2i 2827 . . . . . . . . . . . . . . . . 17 ((1 / 2) + (1 / 4)) = (3 / 4)
6665a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → ((1 / 2) + (1 / 4)) = (3 / 4))
6766oveq2d 6894 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → (𝑥 + ((1 / 2) + (1 / 4))) = (𝑥 + (3 / 4)))
6867fveq2d 6415 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = (⌊‘(𝑥 + (3 / 4))))
69 3re 11393 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
70 0re 10330 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
71 3pos 11425 . . . . . . . . . . . . . . . . . 18 0 < 3
7270, 69, 71ltleii 10450 . . . . . . . . . . . . . . . . 17 0 ≤ 3
73 divge0 11184 . . . . . . . . . . . . . . . . 17 (((3 ∈ ℝ ∧ 0 ≤ 3) ∧ (4 ∈ ℝ ∧ 0 < 4)) → 0 ≤ (3 / 4))
7469, 72, 28, 29, 73mp4an 685 . . . . . . . . . . . . . . . 16 0 ≤ (3 / 4)
75 3lt4 11494 . . . . . . . . . . . . . . . . 17 3 < 4
76 nnrp 12087 . . . . . . . . . . . . . . . . . . 19 (4 ∈ ℕ → 4 ∈ ℝ+)
7743, 76ax-mp 5 . . . . . . . . . . . . . . . . . 18 4 ∈ ℝ+
78 divlt1lt 12144 . . . . . . . . . . . . . . . . . 18 ((3 ∈ ℝ ∧ 4 ∈ ℝ+) → ((3 / 4) < 1 ↔ 3 < 4))
7969, 77, 78mp2an 684 . . . . . . . . . . . . . . . . 17 ((3 / 4) < 1 ↔ 3 < 4)
8075, 79mpbir 223 . . . . . . . . . . . . . . . 16 (3 / 4) < 1
8174, 80pm3.2i 463 . . . . . . . . . . . . . . 15 (0 ≤ (3 / 4) ∧ (3 / 4) < 1)
8269, 28, 7redivcli 11084 . . . . . . . . . . . . . . . 16 (3 / 4) ∈ ℝ
83 flbi2 12873 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℤ ∧ (3 / 4) ∈ ℝ) → ((⌊‘(𝑥 + (3 / 4))) = 𝑥 ↔ (0 ≤ (3 / 4) ∧ (3 / 4) < 1)))
8482, 83mpan2 683 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → ((⌊‘(𝑥 + (3 / 4))) = 𝑥 ↔ (0 ≤ (3 / 4) ∧ (3 / 4) < 1)))
8581, 84mpbiri 250 . . . . . . . . . . . . . 14 (𝑥 ∈ ℤ → (⌊‘(𝑥 + (3 / 4))) = 𝑥)
8668, 85eqtrd 2833 . . . . . . . . . . . . 13 (𝑥 ∈ ℤ → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = 𝑥)
8786adantr 473 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))) = 𝑥)
88 oveq1 6885 . . . . . . . . . . . . . . . . 17 (𝑀 = ((2 · 𝑥) + 1) → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2))
8988eqcoms 2807 . . . . . . . . . . . . . . . 16 (((2 · 𝑥) + 1) = 𝑀 → (𝑀 / 2) = (((2 · 𝑥) + 1) / 2))
9037a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℤ → 2 ∈ ℤ)
91 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℤ → 𝑥 ∈ ℤ)
9290, 91zmulcld 11778 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℤ)
9392zcnd 11773 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
94 1cnd 10323 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → 1 ∈ ℂ)
9554a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → (2 ∈ ℂ ∧ 2 ≠ 0))
96 divdir 11002 . . . . . . . . . . . . . . . . . 18 (((2 · 𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((2 · 𝑥) + 1) / 2) = (((2 · 𝑥) / 2) + (1 / 2)))
9793, 94, 95, 96syl3anc 1491 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → (((2 · 𝑥) + 1) / 2) = (((2 · 𝑥) / 2) + (1 / 2)))
98 zcn 11671 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
99 2cnd 11391 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → 2 ∈ ℂ)
10016a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℤ → 2 ≠ 0)
10198, 99, 100divcan3d 11098 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℤ → ((2 · 𝑥) / 2) = 𝑥)
102101oveq1d 6893 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℤ → (((2 · 𝑥) / 2) + (1 / 2)) = (𝑥 + (1 / 2)))
10397, 102eqtrd 2833 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → (((2 · 𝑥) + 1) / 2) = (𝑥 + (1 / 2)))
10489, 103sylan9eqr 2855 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → (𝑀 / 2) = (𝑥 + (1 / 2)))
105104oveq1d 6893 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = ((𝑥 + (1 / 2)) + (1 / 4)))
106 halfcn 11535 . . . . . . . . . . . . . . . . 17 (1 / 2) ∈ ℂ
107106a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → (1 / 2) ∈ ℂ)
1086, 7reccli 11047 . . . . . . . . . . . . . . . . 17 (1 / 4) ∈ ℂ
109108a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℤ → (1 / 4) ∈ ℂ)
11098, 107, 109addassd 10351 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4))))
111110adantr 473 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑥 + (1 / 2)) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4))))
112105, 111eqtrd 2833 . . . . . . . . . . . . 13 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑀 / 2) + (1 / 4)) = (𝑥 + ((1 / 2) + (1 / 4))))
113112fveq2d 6415 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → (⌊‘((𝑀 / 2) + (1 / 4))) = (⌊‘(𝑥 + ((1 / 2) + (1 / 4)))))
114 oveq1 6885 . . . . . . . . . . . . . . . 16 (𝑀 = ((2 · 𝑥) + 1) → (𝑀 − 1) = (((2 · 𝑥) + 1) − 1))
115114eqcoms 2807 . . . . . . . . . . . . . . 15 (((2 · 𝑥) + 1) = 𝑀 → (𝑀 − 1) = (((2 · 𝑥) + 1) − 1))
116 pncan1 10746 . . . . . . . . . . . . . . . 16 ((2 · 𝑥) ∈ ℂ → (((2 · 𝑥) + 1) − 1) = (2 · 𝑥))
11793, 116syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℤ → (((2 · 𝑥) + 1) − 1) = (2 · 𝑥))
118115, 117sylan9eqr 2855 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → (𝑀 − 1) = (2 · 𝑥))
119118oveq1d 6893 . . . . . . . . . . . . 13 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = ((2 · 𝑥) / 2))
120101adantr 473 . . . . . . . . . . . . 13 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((2 · 𝑥) / 2) = 𝑥)
121119, 120eqtrd 2833 . . . . . . . . . . . 12 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = 𝑥)
12287, 113, 1213eqtr4rd 2844 . . . . . . . . . . 11 ((𝑥 ∈ ℤ ∧ ((2 · 𝑥) + 1) = 𝑀) → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4))))
123122ex 402 . . . . . . . . . 10 (𝑥 ∈ ℤ → (((2 · 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4)))))
124123adantl 474 . . . . . . . . 9 ((𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4)))))
125124rexlimdva 3212 . . . . . . . 8 (𝑀 ∈ ℤ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4)))))
12652, 125sylbid 232 . . . . . . 7 (𝑀 ∈ ℤ → (¬ 2 ∥ 𝑀 → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4)))))
127126impcom 397 . . . . . 6 ((¬ 2 ∥ 𝑀𝑀 ∈ ℤ) → ((𝑀 − 1) / 2) = (⌊‘((𝑀 / 2) + (1 / 4))))
12851, 127eqtrd 2833 . . . . 5 ((¬ 2 ∥ 𝑀𝑀 ∈ ℤ) → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 / 4))))
12949, 128pm2.61ian 847 . . . 4 (𝑀 ∈ ℤ → if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)) = (⌊‘((𝑀 / 2) + (1 / 4))))
130129eqcomd 2805 . . 3 (𝑀 ∈ ℤ → (⌊‘((𝑀 / 2) + (1 / 4))) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)))
131130adantr 473 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘((𝑀 / 2) + (1 / 4))) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)))
13223, 131eqtrd 2833 1 ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  wne 2971  wrex 3090  ifcif 4277   class class class wbr 4843  cfv 6101  (class class class)co 6878  cc 10222  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229   < clt 10363  cle 10364  cmin 10556   / cdiv 10976  cn 11312  2c2 11368  3c3 11369  4c4 11370  cz 11666  +crp 12074  cfl 12846  cdvds 15319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-un 7183  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3387  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-iun 4712  df-br 4844  df-opab 4906  df-mpt 4923  df-tr 4946  df-id 5220  df-eprel 5225  df-po 5233  df-so 5234  df-fr 5271  df-we 5273  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-pred 5898  df-ord 5944  df-on 5945  df-lim 5946  df-suc 5947  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6839  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-om 7300  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-er 7982  df-en 8196  df-dom 8197  df-sdom 8198  df-sup 8590  df-inf 8591  df-pnf 10365  df-mnf 10366  df-xr 10367  df-ltxr 10368  df-le 10369  df-sub 10558  df-neg 10559  df-div 10977  df-nn 11313  df-2 11376  df-3 11377  df-4 11378  df-n0 11581  df-z 11667  df-uz 11931  df-rp 12075  df-fl 12848  df-dvds 15320
This theorem is referenced by:  2lgslem1c  25470
  Copyright terms: Public domain W3C validator