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

Theorem pilem2 24105
 Description: Lemma for pire 24109, pigt2lt4 24107 and sinpi 24108. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by AV, 14-Sep-2020.)
Hypotheses
Ref Expression
pilem.1 (𝜑𝐴 ∈ (2(,)4))
pilem.2 (𝜑𝐵 ∈ ℝ+)
pilem.3 (𝜑 → (sin‘𝐴) = 0)
pilem.4 (𝜑 → (sin‘𝐵) = 0)
pilem.5 (𝜑 → π < 𝐴)
Assertion
Ref Expression
pilem2 (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)

Proof of Theorem pilem2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-pi 14723 . . . 4 π = inf((ℝ+ ∩ (sin “ {0})), ℝ, < )
2 inss1 3816 . . . . . . 7 (ℝ+ ∩ (sin “ {0})) ⊆ ℝ+
3 rpssre 11787 . . . . . . 7 + ⊆ ℝ
42, 3sstri 3597 . . . . . 6 (ℝ+ ∩ (sin “ {0})) ⊆ ℝ
54a1i 11 . . . . 5 (𝜑 → (ℝ+ ∩ (sin “ {0})) ⊆ ℝ)
6 0re 9985 . . . . . . 7 0 ∈ ℝ
72sseli 3584 . . . . . . . . 9 (𝑦 ∈ (ℝ+ ∩ (sin “ {0})) → 𝑦 ∈ ℝ+)
87rpge0d 11820 . . . . . . . 8 (𝑦 ∈ (ℝ+ ∩ (sin “ {0})) → 0 ≤ 𝑦)
98rgen 2922 . . . . . . 7 𝑦 ∈ (ℝ+ ∩ (sin “ {0}))0 ≤ 𝑦
10 breq1 4621 . . . . . . . . 9 (𝑥 = 0 → (𝑥𝑦 ↔ 0 ≤ 𝑦))
1110ralbidv 2985 . . . . . . . 8 (𝑥 = 0 → (∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦 ↔ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))0 ≤ 𝑦))
1211rspcev 3300 . . . . . . 7 ((0 ∈ ℝ ∧ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦)
136, 9, 12mp2an 707 . . . . . 6 𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦
1413a1i 11 . . . . 5 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦)
15 2re 11035 . . . . . . . . 9 2 ∈ ℝ
16 pilem.2 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ+)
1716rpred 11816 . . . . . . . . 9 (𝜑𝐵 ∈ ℝ)
18 remulcl 9966 . . . . . . . . 9 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (2 · 𝐵) ∈ ℝ)
1915, 17, 18sylancr 694 . . . . . . . 8 (𝜑 → (2 · 𝐵) ∈ ℝ)
20 pilem.1 . . . . . . . . 9 (𝜑𝐴 ∈ (2(,)4))
21 elioore 12144 . . . . . . . . 9 (𝐴 ∈ (2(,)4) → 𝐴 ∈ ℝ)
2220, 21syl 17 . . . . . . . 8 (𝜑𝐴 ∈ ℝ)
2319, 22resubcld 10403 . . . . . . 7 (𝜑 → ((2 · 𝐵) − 𝐴) ∈ ℝ)
24 4re 11042 . . . . . . . . . 10 4 ∈ ℝ
2524a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
26 eliooord 12172 . . . . . . . . . . 11 (𝐴 ∈ (2(,)4) → (2 < 𝐴𝐴 < 4))
2720, 26syl 17 . . . . . . . . . 10 (𝜑 → (2 < 𝐴𝐴 < 4))
2827simprd 479 . . . . . . . . 9 (𝜑𝐴 < 4)
29 2t2e4 11122 . . . . . . . . . 10 (2 · 2) = 4
3015a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℝ)
31 0red 9986 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
32 2pos 11057 . . . . . . . . . . . . . . . . . 18 0 < 2
3332a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 2)
3427simpld 475 . . . . . . . . . . . . . . . . 17 (𝜑 → 2 < 𝐴)
3531, 30, 22, 33, 34lttrd 10143 . . . . . . . . . . . . . . . 16 (𝜑 → 0 < 𝐴)
3622, 35elrpd 11813 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ+)
37 pilem.3 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘𝐴) = 0)
38 pilem1 24104 . . . . . . . . . . . . . . 15 (𝐴 ∈ (ℝ+ ∩ (sin “ {0})) ↔ (𝐴 ∈ ℝ+ ∧ (sin‘𝐴) = 0))
3936, 37, 38sylanbrc 697 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (ℝ+ ∩ (sin “ {0})))
40 ne0i 3902 . . . . . . . . . . . . . 14 (𝐴 ∈ (ℝ+ ∩ (sin “ {0})) → (ℝ+ ∩ (sin “ {0})) ≠ ∅)
4139, 40syl 17 . . . . . . . . . . . . 13 (𝜑 → (ℝ+ ∩ (sin “ {0})) ≠ ∅)
42 infrecl 10950 . . . . . . . . . . . . . 14 (((ℝ+ ∩ (sin “ {0})) ⊆ ℝ ∧ (ℝ+ ∩ (sin “ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦) → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ∈ ℝ)
434, 13, 42mp3an13 1412 . . . . . . . . . . . . 13 ((ℝ+ ∩ (sin “ {0})) ≠ ∅ → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ∈ ℝ)
4441, 43syl 17 . . . . . . . . . . . 12 (𝜑 → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ∈ ℝ)
45 pilem1 24104 . . . . . . . . . . . . . . 15 (𝑥 ∈ (ℝ+ ∩ (sin “ {0})) ↔ (𝑥 ∈ ℝ+ ∧ (sin‘𝑥) = 0))
46 rpre 11783 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
4746adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
48 letric 10082 . . . . . . . . . . . . . . . . . . . 20 ((2 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (2 ≤ 𝑥𝑥 ≤ 2))
4915, 47, 48sylancr 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ+) → (2 ≤ 𝑥𝑥 ≤ 2))
5049ord 392 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (¬ 2 ≤ 𝑥𝑥 ≤ 2))
5146ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ∈ ℝ)
52 rpgt0 11788 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ+ → 0 < 𝑥)
5352ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 0 < 𝑥)
54 simpr 477 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ≤ 2)
55 0xr 10031 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
56 elioc2 12175 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ 2 ∈ ℝ) → (𝑥 ∈ (0(,]2) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥𝑥 ≤ 2)))
5755, 15, 56mp2an 707 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (0(,]2) ↔ (𝑥 ∈ ℝ ∧ 0 < 𝑥𝑥 ≤ 2))
5851, 53, 54, 57syl3anbrc 1244 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 𝑥 ∈ (0(,]2))
59 sin02gt0 14842 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (0(,]2) → 0 < (sin‘𝑥))
6058, 59syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → 0 < (sin‘𝑥))
6160gt0ne0d 10537 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑥 ≤ 2) → (sin‘𝑥) ≠ 0)
6261ex 450 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ ℝ+) → (𝑥 ≤ 2 → (sin‘𝑥) ≠ 0))
6350, 62syld 47 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ ℝ+) → (¬ 2 ≤ 𝑥 → (sin‘𝑥) ≠ 0))
6463necon4bd 2816 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ ℝ+) → ((sin‘𝑥) = 0 → 2 ≤ 𝑥))
6564expimpd 628 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑥 ∈ ℝ+ ∧ (sin‘𝑥) = 0) → 2 ≤ 𝑥))
6645, 65syl5bi 232 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (ℝ+ ∩ (sin “ {0})) → 2 ≤ 𝑥))
6766ralrimiv 2964 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥 ∈ (ℝ+ ∩ (sin “ {0}))2 ≤ 𝑥)
68 infregelb 10952 . . . . . . . . . . . . . 14 ((((ℝ+ ∩ (sin “ {0})) ⊆ ℝ ∧ (ℝ+ ∩ (sin “ {0})) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦) ∧ 2 ∈ ℝ) → (2 ≤ inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ↔ ∀𝑥 ∈ (ℝ+ ∩ (sin “ {0}))2 ≤ 𝑥))
695, 41, 14, 30, 68syl31anc 1326 . . . . . . . . . . . . 13 (𝜑 → (2 ≤ inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ↔ ∀𝑥 ∈ (ℝ+ ∩ (sin “ {0}))2 ≤ 𝑥))
7067, 69mpbird 247 . . . . . . . . . . . 12 (𝜑 → 2 ≤ inf((ℝ+ ∩ (sin “ {0})), ℝ, < ))
71 pilem.4 . . . . . . . . . . . . . 14 (𝜑 → (sin‘𝐵) = 0)
72 pilem1 24104 . . . . . . . . . . . . . 14 (𝐵 ∈ (ℝ+ ∩ (sin “ {0})) ↔ (𝐵 ∈ ℝ+ ∧ (sin‘𝐵) = 0))
7316, 71, 72sylanbrc 697 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (ℝ+ ∩ (sin “ {0})))
74 infrelb 10953 . . . . . . . . . . . . 13 (((ℝ+ ∩ (sin “ {0})) ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦𝐵 ∈ (ℝ+ ∩ (sin “ {0}))) → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ≤ 𝐵)
755, 14, 73, 74syl3anc 1323 . . . . . . . . . . . 12 (𝜑 → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ≤ 𝐵)
7630, 44, 17, 70, 75letrd 10139 . . . . . . . . . . 11 (𝜑 → 2 ≤ 𝐵)
7715, 32pm3.2i 471 . . . . . . . . . . . . 13 (2 ∈ ℝ ∧ 0 < 2)
7877a1i 11 . . . . . . . . . . . 12 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
79 lemul2 10821 . . . . . . . . . . . 12 ((2 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (2 ≤ 𝐵 ↔ (2 · 2) ≤ (2 · 𝐵)))
8030, 17, 78, 79syl3anc 1323 . . . . . . . . . . 11 (𝜑 → (2 ≤ 𝐵 ↔ (2 · 2) ≤ (2 · 𝐵)))
8176, 80mpbid 222 . . . . . . . . . 10 (𝜑 → (2 · 2) ≤ (2 · 𝐵))
8229, 81syl5eqbrr 4654 . . . . . . . . 9 (𝜑 → 4 ≤ (2 · 𝐵))
8322, 25, 19, 28, 82ltletrd 10142 . . . . . . . 8 (𝜑𝐴 < (2 · 𝐵))
8422, 19posdifd 10559 . . . . . . . 8 (𝜑 → (𝐴 < (2 · 𝐵) ↔ 0 < ((2 · 𝐵) − 𝐴)))
8583, 84mpbid 222 . . . . . . 7 (𝜑 → 0 < ((2 · 𝐵) − 𝐴))
8623, 85elrpd 11813 . . . . . 6 (𝜑 → ((2 · 𝐵) − 𝐴) ∈ ℝ+)
8719recnd 10013 . . . . . . . 8 (𝜑 → (2 · 𝐵) ∈ ℂ)
8822recnd 10013 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
89 sinsub 14818 . . . . . . . 8 (((2 · 𝐵) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (sin‘((2 · 𝐵) − 𝐴)) = (((sin‘(2 · 𝐵)) · (cos‘𝐴)) − ((cos‘(2 · 𝐵)) · (sin‘𝐴))))
9087, 88, 89syl2anc 692 . . . . . . 7 (𝜑 → (sin‘((2 · 𝐵) − 𝐴)) = (((sin‘(2 · 𝐵)) · (cos‘𝐴)) − ((cos‘(2 · 𝐵)) · (sin‘𝐴))))
9117recnd 10013 . . . . . . . . . . . . 13 (𝜑𝐵 ∈ ℂ)
92 sin2t 14827 . . . . . . . . . . . . 13 (𝐵 ∈ ℂ → (sin‘(2 · 𝐵)) = (2 · ((sin‘𝐵) · (cos‘𝐵))))
9391, 92syl 17 . . . . . . . . . . . 12 (𝜑 → (sin‘(2 · 𝐵)) = (2 · ((sin‘𝐵) · (cos‘𝐵))))
9471oveq1d 6620 . . . . . . . . . . . . . . 15 (𝜑 → ((sin‘𝐵) · (cos‘𝐵)) = (0 · (cos‘𝐵)))
9591coscld 14781 . . . . . . . . . . . . . . . 16 (𝜑 → (cos‘𝐵) ∈ ℂ)
9695mul02d 10179 . . . . . . . . . . . . . . 15 (𝜑 → (0 · (cos‘𝐵)) = 0)
9794, 96eqtrd 2660 . . . . . . . . . . . . . 14 (𝜑 → ((sin‘𝐵) · (cos‘𝐵)) = 0)
9897oveq2d 6621 . . . . . . . . . . . . 13 (𝜑 → (2 · ((sin‘𝐵) · (cos‘𝐵))) = (2 · 0))
99 2t0e0 11128 . . . . . . . . . . . . 13 (2 · 0) = 0
10098, 99syl6eq 2676 . . . . . . . . . . . 12 (𝜑 → (2 · ((sin‘𝐵) · (cos‘𝐵))) = 0)
10193, 100eqtrd 2660 . . . . . . . . . . 11 (𝜑 → (sin‘(2 · 𝐵)) = 0)
102101oveq1d 6620 . . . . . . . . . 10 (𝜑 → ((sin‘(2 · 𝐵)) · (cos‘𝐴)) = (0 · (cos‘𝐴)))
10388coscld 14781 . . . . . . . . . . 11 (𝜑 → (cos‘𝐴) ∈ ℂ)
104103mul02d 10179 . . . . . . . . . 10 (𝜑 → (0 · (cos‘𝐴)) = 0)
105102, 104eqtrd 2660 . . . . . . . . 9 (𝜑 → ((sin‘(2 · 𝐵)) · (cos‘𝐴)) = 0)
10637oveq2d 6621 . . . . . . . . . 10 (𝜑 → ((cos‘(2 · 𝐵)) · (sin‘𝐴)) = ((cos‘(2 · 𝐵)) · 0))
10787coscld 14781 . . . . . . . . . . 11 (𝜑 → (cos‘(2 · 𝐵)) ∈ ℂ)
108107mul01d 10180 . . . . . . . . . 10 (𝜑 → ((cos‘(2 · 𝐵)) · 0) = 0)
109106, 108eqtrd 2660 . . . . . . . . 9 (𝜑 → ((cos‘(2 · 𝐵)) · (sin‘𝐴)) = 0)
110105, 109oveq12d 6623 . . . . . . . 8 (𝜑 → (((sin‘(2 · 𝐵)) · (cos‘𝐴)) − ((cos‘(2 · 𝐵)) · (sin‘𝐴))) = (0 − 0))
111 0m0e0 11075 . . . . . . . 8 (0 − 0) = 0
112110, 111syl6eq 2676 . . . . . . 7 (𝜑 → (((sin‘(2 · 𝐵)) · (cos‘𝐴)) − ((cos‘(2 · 𝐵)) · (sin‘𝐴))) = 0)
11390, 112eqtrd 2660 . . . . . 6 (𝜑 → (sin‘((2 · 𝐵) − 𝐴)) = 0)
114 pilem1 24104 . . . . . 6 (((2 · 𝐵) − 𝐴) ∈ (ℝ+ ∩ (sin “ {0})) ↔ (((2 · 𝐵) − 𝐴) ∈ ℝ+ ∧ (sin‘((2 · 𝐵) − 𝐴)) = 0))
11586, 113, 114sylanbrc 697 . . . . 5 (𝜑 → ((2 · 𝐵) − 𝐴) ∈ (ℝ+ ∩ (sin “ {0})))
116 infrelb 10953 . . . . 5 (((ℝ+ ∩ (sin “ {0})) ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (ℝ+ ∩ (sin “ {0}))𝑥𝑦 ∧ ((2 · 𝐵) − 𝐴) ∈ (ℝ+ ∩ (sin “ {0}))) → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ≤ ((2 · 𝐵) − 𝐴))
1175, 14, 115, 116syl3anc 1323 . . . 4 (𝜑 → inf((ℝ+ ∩ (sin “ {0})), ℝ, < ) ≤ ((2 · 𝐵) − 𝐴))
1181, 117syl5eqbr 4653 . . 3 (𝜑 → π ≤ ((2 · 𝐵) − 𝐴))
1191, 44syl5eqel 2708 . . . 4 (𝜑 → π ∈ ℝ)
120 leaddsub 10449 . . . 4 ((π ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (2 · 𝐵) ∈ ℝ) → ((π + 𝐴) ≤ (2 · 𝐵) ↔ π ≤ ((2 · 𝐵) − 𝐴)))
121119, 22, 19, 120syl3anc 1323 . . 3 (𝜑 → ((π + 𝐴) ≤ (2 · 𝐵) ↔ π ≤ ((2 · 𝐵) − 𝐴)))
122118, 121mpbird 247 . 2 (𝜑 → (π + 𝐴) ≤ (2 · 𝐵))
123119, 22readdcld 10014 . . 3 (𝜑 → (π + 𝐴) ∈ ℝ)
124 ledivmul 10844 . . 3 (((π + 𝐴) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((π + 𝐴) / 2) ≤ 𝐵 ↔ (π + 𝐴) ≤ (2 · 𝐵)))
125123, 17, 78, 124syl3anc 1323 . 2 (𝜑 → (((π + 𝐴) / 2) ≤ 𝐵 ↔ (π + 𝐴) ≤ (2 · 𝐵)))
126122, 125mpbird 247 1 (𝜑 → ((π + 𝐴) / 2) ≤ 𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1992   ≠ wne 2796  ∀wral 2912  ∃wrex 2913   ∩ cin 3559   ⊆ wss 3560  ∅c0 3896  {csn 4153   class class class wbr 4618  ◡ccnv 5078   “ cima 5082  ‘cfv 5850  (class class class)co 6605  infcinf 8292  ℂcc 9879  ℝcr 9880  0cc0 9881   + caddc 9884   · cmul 9886  ℝ*cxr 10018   < clt 10019   ≤ cle 10020   − cmin 10211   / cdiv 10629  2c2 11015  4c4 11017  ℝ+crp 11776  (,)cioo 12114  (,]cioc 12115  sincsin 14714  cosccos 14715  πcpi 14717 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959  ax-addf 9960  ax-mulf 9961 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-pm 7806  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-oi 8360  df-card 8710  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-4 11026  df-5 11027  df-6 11028  df-7 11029  df-8 11030  df-n0 11238  df-z 11323  df-uz 11632  df-rp 11777  df-ioo 12118  df-ioc 12119  df-ico 12120  df-fz 12266  df-fzo 12404  df-fl 12530  df-seq 12739  df-exp 12798  df-fac 12998  df-bc 13027  df-hash 13055  df-shft 13736  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-limsup 14131  df-clim 14148  df-rlim 14149  df-sum 14346  df-ef 14718  df-sin 14720  df-cos 14721  df-pi 14723 This theorem is referenced by:  pilem3  24106
 Copyright terms: Public domain W3C validator