Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-hgprmladderOLD Structured version   Visualization version   GIF version

Axiom ax-hgprmladderOLD 40235
Description: Obsolete version of ax-hgprmladder 40228 as of 9-Sep-2021. (Contributed by AV, 3-Aug-2020.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hgprmladderOLD 𝑑 ∈ (ℤ‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = 13 ∧ (𝑓𝑑) = (89 · (10↑29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))))

Detailed syntax breakdown of Axiom ax-hgprmladderOLD
StepHypRef Expression
1 cc0 9815 . . . . . . 7 class 0
2 vf . . . . . . . 8 setvar 𝑓
32cv 1474 . . . . . . 7 class 𝑓
41, 3cfv 5804 . . . . . 6 class (𝑓‘0)
5 c7 10952 . . . . . 6 class 7
64, 5wceq 1475 . . . . 5 wff (𝑓‘0) = 7
7 c1 9816 . . . . . . 7 class 1
87, 3cfv 5804 . . . . . 6 class (𝑓‘1)
9 c3 10948 . . . . . . 7 class 3
107, 9cdc 11369 . . . . . 6 class 13
118, 10wceq 1475 . . . . 5 wff (𝑓‘1) = 13
12 vd . . . . . . . 8 setvar 𝑑
1312cv 1474 . . . . . . 7 class 𝑑
1413, 3cfv 5804 . . . . . 6 class (𝑓𝑑)
15 c8 10953 . . . . . . . 8 class 8
16 c9 10954 . . . . . . . 8 class 9
1715, 16cdc 11369 . . . . . . 7 class 89
18 c10 10955 . . . . . . . 8 class 10
19 c2 10947 . . . . . . . . 9 class 2
2019, 16cdc 11369 . . . . . . . 8 class 29
21 cexp 12722 . . . . . . . 8 class
2218, 20, 21co 6549 . . . . . . 7 class (10↑29)
23 cmul 9820 . . . . . . 7 class ·
2417, 22, 23co 6549 . . . . . 6 class (89 · (10↑29))
2514, 24wceq 1475 . . . . 5 wff (𝑓𝑑) = (89 · (10↑29))
266, 11, 25w3a 1031 . . . 4 wff ((𝑓‘0) = 7 ∧ (𝑓‘1) = 13 ∧ (𝑓𝑑) = (89 · (10↑29)))
27 vi . . . . . . . . 9 setvar 𝑖
2827cv 1474 . . . . . . . 8 class 𝑖
2928, 3cfv 5804 . . . . . . 7 class (𝑓𝑖)
30 cprime 15223 . . . . . . . 8 class
3119csn 4125 . . . . . . . 8 class {2}
3230, 31cdif 3537 . . . . . . 7 class (ℙ ∖ {2})
3329, 32wcel 1977 . . . . . 6 wff (𝑓𝑖) ∈ (ℙ ∖ {2})
34 caddc 9818 . . . . . . . . . 10 class +
3528, 7, 34co 6549 . . . . . . . . 9 class (𝑖 + 1)
3635, 3cfv 5804 . . . . . . . 8 class (𝑓‘(𝑖 + 1))
37 cmin 10145 . . . . . . . 8 class
3836, 29, 37co 6549 . . . . . . 7 class ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))
39 c4 10949 . . . . . . . . 9 class 4
407, 15cdc 11369 . . . . . . . . . 10 class 18
4118, 40, 21co 6549 . . . . . . . . 9 class (10↑18)
4239, 41, 23co 6549 . . . . . . . 8 class (4 · (10↑18))
4342, 39, 37co 6549 . . . . . . 7 class ((4 · (10↑18)) − 4)
44 clt 9953 . . . . . . 7 class <
4538, 43, 44wbr 4583 . . . . . 6 wff ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4)
4639, 38, 44wbr 4583 . . . . . 6 wff 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))
4733, 45, 46w3a 1031 . . . . 5 wff ((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)))
48 cfzo 12334 . . . . . 6 class ..^
491, 13, 48co 6549 . . . . 5 class (0..^𝑑)
5047, 27, 49wral 2896 . . . 4 wff 𝑖 ∈ (0..^𝑑)((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)))
5126, 50wa 383 . . 3 wff (((𝑓‘0) = 7 ∧ (𝑓‘1) = 13 ∧ (𝑓𝑑) = (89 · (10↑29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))))
52 ciccp 39951 . . . 4 class RePart
5313, 52cfv 5804 . . 3 class (RePart‘𝑑)
5451, 2, 53wrex 2897 . 2 wff 𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = 13 ∧ (𝑓𝑑) = (89 · (10↑29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))))
55 cuz 11563 . . 3 class
569, 55cfv 5804 . 2 class (ℤ‘3)
5754, 12, 56wrex 2897 1 wff 𝑑 ∈ (ℤ‘3)∃𝑓 ∈ (RePart‘𝑑)(((𝑓‘0) = 7 ∧ (𝑓‘1) = 13 ∧ (𝑓𝑑) = (89 · (10↑29))) ∧ ∀𝑖 ∈ (0..^𝑑)((𝑓𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝑓‘(𝑖 + 1)) − (𝑓𝑖)) < ((4 · (10↑18)) − 4) ∧ 4 < ((𝑓‘(𝑖 + 1)) − (𝑓𝑖))))
Colors of variables: wff setvar class
This axiom is referenced by:  tgblthelfgottOLD  40236
  Copyright terms: Public domain W3C validator